PROOF.bc_eq_sym: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/PROOF.bend as PROOF
Lines 915-934 of bendtorch@1.3.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/PROOF.bend&start_line=915&end_line=934

import Base
import bendtorch@1.3.0.0/tensor.bend as TT

# axis by axis: the same on each axis (bc_dim_sym), and by induction on the rest; shapes of different ranks are False
# either way round
def bc_eq_sym(a: List<&2, Nat>, b: List<&2, Nat>, o: List<&2, Nat>) -> {TT.bc_eq(a, b, o) == TT.bc_eq(b, a, o) : Bool}:
  match a b o:
    case Nil{} Nil{} Nil{}:
      {==}
    case Nil{} Nil{} Con{z, ro}:
      {==}
    case Nil{} Con{y, rb} Nil{}:
      {==}
    case Nil{} Con{y, rb} Con{z, ro}:
      {==}
    case Con{x, ra} Nil{} Nil{}:
      {==}
    case Con{x, ra} Nil{} Con{z, ro}:
      {==}
    case Con{x, ra} Con{y, rb} Nil{}:
      {==}
    case Con{+x, +ra} Con{+y, +rb} Con{+z, +ro}:
      and_cong(TT.bc_dim(x, y, z), TT.bc_dim(y, x, z), TT.bc_eq(ra, rb, ro), TT.bc_eq(rb, ra, ro), bc_dim_sym(x, y, z), bc_eq_sym(ra, rb, ro))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=and_cong
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=bc_dim_sym
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=bc_dim
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=bc_eq