def aligned_unique

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

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

94def aligned_unique(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +other: List<&2, Nat>, +first: Shape.Aligned(left, right, output), +second: Shape.Aligned(left, right, other)) -> {output == other : List<&2, Nat>}:
95  match left right output:
96    case Nil{} Nil{} Nil{}:
97      match other:
98        case Nil{}:
99          {==}
100        case oh <> ot:
101          match second:
102    case +lh <> +lt +rh <> +rt +oh <> +ot:
103      match other:
104        case Nil{}:
105          match second:
106        case +qh <> +qt:
107          Shape.AStep{+a1, +t1} = first
108          Shape.AStep{+a2, +t2} = second
109          %axis_unique(lh, rh, oh, qh, a1, a2) : {oh <> ot == _ <> qt : List<&2, Nat>}
110          %aligned_unique(lt, rt, ot, qt, t1, t2) : {oh <> ot == oh <> _ : List<&2, Nat>}
111          {==}
112    case Nil{} Nil{} oh <> ot:
113      match first:
114    case Nil{} rh <> rt Nil{}:
115      match first:
116    case lh <> lt Nil{} Nil{}:
117      match first:
118    case Nil{} rh <> rt oh <> ot:
119      match first:
120    case lh <> lt Nil{} oh <> ot:
121      match first:
122    case lh <> lt rh <> rt Nil{}:
123      match first: