def axis_unique

bendtorch-core@0.1.0.0 · src/shape/unique_proofs.bend:73

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

73def axis_unique(-left: Nat, -right: Nat, -output: Nat, -other: Nat, +first: Shape.Axis<left, right, output>, +second: Shape.Axis<left, right, other>) -> {output == other : Nat}:
74  match first second:
75    case Shape.AxisEqual{l1, r1} Shape.AxisEqual{l2, r2}:
76      Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))
77    case Shape.AxisEqual{l1, r1} Shape.AxisLeftOne{o2, r2}:
78      Equal.trans(Nat, output, right, other, r1, Equal.sym(Nat, other, right, r2))
79    case Shape.AxisEqual{l1, r1} Shape.AxisRightOne{l2, o2}:
80      Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))
81    case Shape.AxisLeftOne{o1, r1} Shape.AxisEqual{l2, r2}:
82      Equal.trans(Nat, output, right, other, r1, Equal.sym(Nat, other, right, r2))
83    case Shape.AxisLeftOne{o1, r1} Shape.AxisLeftOne{o2, r2}:
84      Equal.trans(Nat, output, right, other, r1, Equal.sym(Nat, other, right, r2))
85    case Shape.AxisLeftOne{o1, r1} Shape.AxisRightOne{l2, o2}:
86      Equal.trans(Nat, output, 1n, other, Equal.trans(Nat, output, right, 1n, r1, Equal.sym(Nat, 1n, right, o2)), Equal.trans(Nat, 1n, left, other, o1, Equal.sym(Nat, other, left, l2)))
87    case Shape.AxisRightOne{l1, o1} Shape.AxisEqual{l2, r2}:
88      Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))
89    case Shape.AxisRightOne{l1, o1} Shape.AxisLeftOne{o2, r2}:
90      Equal.trans(Nat, output, 1n, other, Equal.trans(Nat, output, left, 1n, l1, Equal.sym(Nat, 1n, left, o2)), Equal.trans(Nat, 1n, right, other, o1, Equal.sym(Nat, other, right, r2)))
91    case Shape.AxisRightOne{l1, o1} Shape.AxisRightOne{l2, o2}:
92      Equal.trans(Nat, output, left, other, l1, Equal.sym(Nat, other, left, l2))