PROOF.bend

bendtorch@1.3.0.0 · 1,076 lines · 114 definitions

1# The proofs of LAWS.bend. Every proof is plain Bend: no @unsafe, no ?TODO, no axioms. The arithmetic lemmas come
2# from bend-ml-nat-lemmas; the division lemmas behind gqa_head are llama.bend's (MIT, same author).
3
4import Base
5import bendtorch@1.3.0.0/main.bend as T
6import bendtorch@1.3.0.0/spec.bend as Spec
7import bendtorch@1.3.0.0/tensor.bend as TT
8import bendtorch@1.3.0.0/LAWS.bend as Laws
9import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL
10import bend-ml-tensor-array@0.1.18.0/main.bend as TA
11
12# =====================================================================================================
13# Dot products
14# =====================================================================================================
15
16# dot(a + b, v) == dot(a, v) + dot(b, v): induction on the three vectors; at each entry (x + y)·z splits into x·z + y·z
17# (distributivity) and add4 regroups the four terms
18def dot_vadd(a: List<&2, Nat>, b: List<&2, Nat>, v: List<&2, Nat>) -> {Spec.dotn(Spec.vadd(a, b), v) == Nat.add(Spec.dotn(a, v), Spec.dotn(b, v)) : Nat}:
19  match a b v:
20    case Nil{} _ _:
21      {==}
22    case Con{+x, +xt} Nil{} +v:
23      Equal.sym(Nat, Nat.add(Spec.dotn(Con{x, xt}, v), 0n), Spec.dotn(Con{x, xt}, v), NL.add_zero(Spec.dotn(Con{x, xt}, v)))
24    case Con{x, xt} Con{y, yt} Nil{}:
25      {==}
26    case Con{+x, +xt} Con{+y, +yt} Con{+z, +zt}:
27      +xz = Nat.mul(x, z)
28      +yz = Nat.mul(y, z)
29      +pa = Spec.dotn(xt, zt)
30      +pb = Spec.dotn(yt, zt)
31      Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(x, y), z), Spec.dotn(Spec.vadd(xt, yt), zt)), Nat.add(Nat.mul(Nat.add(x, y), z), Nat.add(pa, pb)), Nat.add(Nat.add(xz, pa), Nat.add(yz, pb)),
32        Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(Nat.add(x, y), z), s), Spec.dotn(Spec.vadd(xt, yt), zt), Nat.add(pa, pb), dot_vadd(xt, yt, zt)),
33        Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(x, y), z), Nat.add(pa, pb)), Nat.add(Nat.add(xz, yz), Nat.add(pa, pb)), Nat.add(Nat.add(xz, pa), Nat.add(yz, pb)),
34          Equal.cong(Nat, Nat, s => Nat.add(s, Nat.add(pa, pb)), Nat.mul(Nat.add(x, y), z), Nat.add(xz, yz), Equal.sym(Nat, Nat.add(xz, yz), Nat.mul(Nat.add(x, y), z), NL.mul_dist(x, y, z))),
35          NL.add4(xz, yz, pa, pb)))
36
37# dot(k·r, v) == k · dot(r, v): at each entry (k·x)·z == k·(x·z) (associativity), then k factors out of the sum
38def dot_scale(+k: Nat, r: List<&2, Nat>, v: List<&2, Nat>) -> {Spec.dotn(Spec.vscale(k, r), v) == Nat.mul(k, Spec.dotn(r, v)) : Nat}:
39  match r v:
40    case Nil{} _:
41      Equal.sym(Nat, Nat.mul(k, 0n), 0n, NL.mul_zero(k))
42    case Con{x, xt} Nil{}:
43      Equal.sym(Nat, Nat.mul(k, 0n), 0n, NL.mul_zero(k))
44    case Con{+x, +xt} Con{+z, +zt}:
45      +d = Spec.dotn(xt, zt)
46      Equal.trans(Nat, Nat.add(Nat.mul(Nat.mul(k, x), z), Spec.dotn(Spec.vscale(k, xt), zt)), Nat.add(Nat.mul(Nat.mul(k, x), z), Nat.mul(k, d)), Nat.mul(k, Nat.add(Nat.mul(x, z), d)),
47        Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(Nat.mul(k, x), z), s), Spec.dotn(Spec.vscale(k, xt), zt), Nat.mul(k, d), dot_scale(k, xt, zt)),
48        Equal.trans(Nat, Nat.add(Nat.mul(Nat.mul(k, x), z), Nat.mul(k, d)), Nat.add(Nat.mul(k, Nat.mul(x, z)), Nat.mul(k, d)), Nat.mul(k, Nat.add(Nat.mul(x, z), d)),
49          Equal.cong(Nat, Nat, s => Nat.add(s, Nat.mul(k, d)), Nat.mul(Nat.mul(k, x), z), Nat.mul(k, Nat.mul(x, z)), Equal.sym(Nat, Nat.mul(k, Nat.mul(x, z)), Nat.mul(Nat.mul(k, x), z), NL.mul_assoc(k, x, z))),
50          Equal.sym(Nat, Nat.mul(k, Nat.add(Nat.mul(x, z), d)), Nat.add(Nat.mul(k, Nat.mul(x, z)), Nat.mul(k, d)), NL.mul_dist_l(k, Nat.mul(x, z), d))))
51
52# dot(a, b) == dot(b, a)
53def dot_comm(a: List<&2, Nat>, b: List<&2, Nat>) -> {Spec.dotn(a, b) == Spec.dotn(b, a) : Nat}:
54  match a b:
55    case Nil{} Nil{}:
56      {==}
57    case Nil{} Con{y, yt}:
58      {==}
59    case Con{x, xt} Nil{}:
60      {==}
61    case Con{+x, +xt} Con{+y, +yt}:
62      Equal.trans(Nat, Nat.add(Nat.mul(x, y), Spec.dotn(xt, yt)), Nat.add(Nat.mul(y, x), Spec.dotn(xt, yt)), Nat.add(Nat.mul(y, x), Spec.dotn(yt, xt)),
63        Equal.cong(Nat, Nat, s => Nat.add(s, Spec.dotn(xt, yt)), Nat.mul(x, y), Nat.mul(y, x), NL.mul_comm(x, y)),
64        Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(y, x), s), Spec.dotn(xt, yt), Spec.dotn(yt, xt), dot_comm(xt, yt)))
65
66# =====================================================================================================
67# The linear laws
68# =====================================================================================================
69
70# PROOF (adjoint): induction on the rows of W and the entries of dy. Row r with weight g_i contributes g_i·(r·x) on the
71# left and (g_i·r)·x on the right (dot_scale); the right side's sum of weighted rows splits by dot_vadd.
72def Laws.adjoint(w, g, v):
73  match w g:
74    case Nil{} Nil{}:
75      {==}
76    case Nil{} Con{gi, gt}:
77      {==}
78    case Con{r, rt} Nil{}:
79      {==}
80    case Con{+r, +rt} Con{+gi, +gt}:
81      +a = Spec.dotn(Spec.vscale(gi, r), v)
82      +m = Spec.mtv(rt, gt)
83      Equal.trans(Nat, Nat.add(Nat.mul(gi, Spec.dotn(r, v)), Spec.dotn(gt, Spec.mv(rt, v))), Nat.add(Nat.mul(gi, Spec.dotn(r, v)), Spec.dotn(m, v)), Spec.dotn(Spec.vadd(Spec.vscale(gi, r), m), v),
84        Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(gi, Spec.dotn(r, v)), s), Spec.dotn(gt, Spec.mv(rt, v)), Spec.dotn(m, v), Laws.adjoint(rt, gt, v)),
85        Equal.trans(Nat, Nat.add(Nat.mul(gi, Spec.dotn(r, v)), Spec.dotn(m, v)), Nat.add(a, Spec.dotn(m, v)), Spec.dotn(Spec.vadd(Spec.vscale(gi, r), m), v),
86          Equal.cong(Nat, Nat, s => Nat.add(s, Spec.dotn(m, v)), Nat.mul(gi, Spec.dotn(r, v)), a, Equal.sym(Nat, a, Nat.mul(gi, Spec.dotn(r, v)), dot_scale(gi, r, v))),
87          Equal.sym(Nat, Spec.dotn(Spec.vadd(Spec.vscale(gi, r), m), v), Nat.add(a, Spec.dotn(m, v)), dot_vadd(Spec.vscale(gi, r), m, v))))
88
89# PROOF (weight_adjoint): row by row, g_i·(r·x) == (g_i·x)·r, by dot_comm and dot_scale.
90def Laws.weight_adjoint(w, g, v):
91  match w g:
92    case Nil{} Nil{}:
93      {==}
94    case Nil{} Con{gi, gt}:
95      {==}
96    case Con{r, rt} Nil{}:
97      {==}
98    case Con{+r, +rt} Con{+gi, +gt}:
99      +f = Spec.frob(Spec.outer(gt, v), rt)
100      Equal.trans(Nat, Nat.add(Nat.mul(gi, Spec.dotn(r, v)), Spec.dotn(gt, Spec.mv(rt, v))), Nat.add(Nat.mul(gi, Spec.dotn(r, v)), f), Nat.add(Spec.dotn(Spec.vscale(gi, v), r), f),
101        Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(gi, Spec.dotn(r, v)), s), Spec.dotn(gt, Spec.mv(rt, v)), f, Laws.weight_adjoint(rt, gt, v)),
102        Equal.cong(Nat, Nat, s => Nat.add(s, f), Nat.mul(gi, Spec.dotn(r, v)), Spec.dotn(Spec.vscale(gi, v), r),
103          Equal.trans(Nat, Nat.mul(gi, Spec.dotn(r, v)), Nat.mul(gi, Spec.dotn(v, r)), Spec.dotn(Spec.vscale(gi, v), r),
104            Equal.cong(Nat, Nat, s => Nat.mul(gi, s), Spec.dotn(r, v), Spec.dotn(v, r), dot_comm(r, v)),
105            Equal.sym(Nat, Spec.dotn(Spec.vscale(gi, v), r), Nat.mul(gi, Spec.dotn(v, r)), dot_scale(gi, v, r)))))
106
107# PROOF (adjoint_seq): adjoint once for W2 (with W1·x as the input), then once for W1.
108def Laws.adjoint_seq(w1, w2, g, v):
109  Equal.trans(Nat, Spec.dotn(g, Spec.mv(w2, Spec.mv(w1, v))), Spec.dotn(Spec.mtv(w2, g), Spec.mv(w1, v)), Spec.dotn(Spec.mtv(w1, Spec.mtv(w2, g)), v), Laws.adjoint(w2, g, Spec.mv(w1, v)), Laws.adjoint(w1, Spec.mtv(w2, g), v))
110
111# =====================================================================================================
112# Causal attention
113# =====================================================================================================
114
115# PROOF (seq_chain): Seq's forward pass computes W2·(W1·x) and saves x and W1·x; its backward pass computes
116# W1ᵀ·(W2ᵀ·dy). Every step of the combinator reduces, so this is adjoint_seq.
117def Laws.seq_chain(w1, w2, x, dy, g1, g2):
118  Laws.adjoint_seq(w1, w2, dy, x)
119
120# PROOF (fork_sum): Fork's backward pass is W1ᵀ·dy1 + W2ᵀ·dy2 (vadd, the add it was given); the dot of a sum is the sum
121# of the dots (dot_vadd), and each is its layer's adjoint law.
122def Laws.fork_sum(w1, w2, x, dy1, dy2, g1, g2):
123  Equal.trans(Nat, Nat.add(Spec.dotn(dy1, Spec.mv(w1, x)), Spec.dotn(dy2, Spec.mv(w2, x))), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x), Spec.dotn(Spec.mtv(w2, dy2), x)), Spec.dotn(Spec.vadd(Spec.mtv(w1, dy1), Spec.mtv(w2, dy2)), x),
124    Equal.trans(Nat, Nat.add(Spec.dotn(dy1, Spec.mv(w1, x)), Spec.dotn(dy2, Spec.mv(w2, x))), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x), Spec.dotn(dy2, Spec.mv(w2, x))), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x), Spec.dotn(Spec.mtv(w2, dy2), x)),
125      Equal.cong(Nat, Nat, z => Nat.add(z, Spec.dotn(dy2, Spec.mv(w2, x))), Spec.dotn(dy1, Spec.mv(w1, x)), Spec.dotn(Spec.mtv(w1, dy1), x), Laws.adjoint(w1, dy1, x)),
126      Equal.cong(Nat, Nat, z => Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x), z), Spec.dotn(dy2, Spec.mv(w2, x)), Spec.dotn(Spec.mtv(w2, dy2), x), Laws.adjoint(w2, dy2, x))),
127    Equal.sym(Nat, Spec.dotn(Spec.vadd(Spec.mtv(w1, dy1), Spec.mtv(w2, dy2)), x), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x), Spec.dotn(Spec.mtv(w2, dy2), x)), dot_vadd(Spec.mtv(w1, dy1), Spec.mtv(w2, dy2), x)))
128
129# PROOF (both_sum): Both runs each layer on its own side, so both sides are pairs of linear passes; each half of the sum
130# is its layer's adjoint law.
131def Laws.both_sum(w1, w2, x1, x2, dy1, dy2, g1, g2):
132  Equal.trans(Nat, Nat.add(Spec.dotn(dy1, Spec.mv(w1, x1)), Spec.dotn(dy2, Spec.mv(w2, x2))), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x1), Spec.dotn(dy2, Spec.mv(w2, x2))), Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x1), Spec.dotn(Spec.mtv(w2, dy2), x2)),
133    Equal.cong(Nat, Nat, z => Nat.add(z, Spec.dotn(dy2, Spec.mv(w2, x2))), Spec.dotn(dy1, Spec.mv(w1, x1)), Spec.dotn(Spec.mtv(w1, dy1), x1), Laws.adjoint(w1, dy1, x1)),
134    Equal.cong(Nat, Nat, z => Nat.add(Spec.dotn(Spec.mtv(w1, dy1), x1), z), Spec.dotn(dy2, Spec.mv(w2, x2)), Spec.dotn(Spec.mtv(w2, dy2), x2), Laws.adjoint(w2, dy2, x2)))
135
136# PROOF (residual): the forward pass gives x + W·x and the backward pass dy + Wᵀ·dy (Id hands dy back, the linear layer
137# Wᵀ·dy, Fork adds them). Then dy·(x + W·x) = x·dy + (W·x)·dy (dot_comm, dot_vadd) = dy·x + dy·(W·x) (dot_comm twice)
138# = dy·x + (Wᵀ·dy)·x (adjoint) = (dy + Wᵀ·dy)·x (dot_vadd).
139def Laws.residual(w, x, dy, g):
140  +wx = Spec.mv(w, x)
141  +wd = Spec.mtv(w, dy)
142  Equal.trans(Nat, Spec.dotn(dy, Spec.vadd(x, wx)), Spec.dotn(Spec.vadd(x, wx), dy), Spec.dotn(Spec.vadd(dy, wd), x),
143    dot_comm(dy, Spec.vadd(x, wx)),
144    Equal.trans(Nat, Spec.dotn(Spec.vadd(x, wx), dy), Nat.add(Spec.dotn(x, dy), Spec.dotn(wx, dy)), Spec.dotn(Spec.vadd(dy, wd), x),
145      dot_vadd(x, wx, dy),
146      Equal.trans(Nat, Nat.add(Spec.dotn(x, dy), Spec.dotn(wx, dy)), Nat.add(Spec.dotn(dy, x), Spec.dotn(wx, dy)), Spec.dotn(Spec.vadd(dy, wd), x),
147        Equal.cong(Nat, Nat, z => Nat.add(z, Spec.dotn(wx, dy)), Spec.dotn(x, dy), Spec.dotn(dy, x), dot_comm(x, dy)),
148        Equal.trans(Nat, Nat.add(Spec.dotn(dy, x), Spec.dotn(wx, dy)), Nat.add(Spec.dotn(dy, x), Spec.dotn(wd, x)), Spec.dotn(Spec.vadd(dy, wd), x),
149          Equal.cong(Nat, Nat, z => Nat.add(Spec.dotn(dy, x), z), Spec.dotn(wx, dy), Spec.dotn(wd, x),
150            Equal.trans(Nat, Spec.dotn(wx, dy), Spec.dotn(dy, wx), Spec.dotn(wd, x), dot_comm(wx, dy), Laws.adjoint(w, dy, x))),
151          Equal.sym(Nat, Spec.dotn(Spec.vadd(dy, wd), x), Nat.add(Spec.dotn(dy, x), Spec.dotn(wd, x)), dot_vadd(dy, wd, x))))))
152
153def disc(b: Bool) -> Type:
154  match b:
155    case True{}:
156      Unit
157    case False{}:
158      Empty
159
160# False == True is impossible: rewriting the goal Empty = disc(False) with it gives disc(True) = Unit
161def false_true(e: {False{} == True{} : Bool}) -> Empty:
162  %Equal.sym(Bool, False{}, True{}, e) : disc(_)
163  Unit{}
164
165# xs reversed onto acc has the length of both
166def len_rcat(+xs: List<&2, F32>, +acc: List<&2, F32>) -> {List.length(&2, F32, T.rcat(xs, acc)) == Nat.add(List.length(&2, F32, xs), List.length(&2, F32, acc)) : Nat}:
167  match xs:
168    case Nil{}:
169      {==}
170    case Con{+x, +t}:
171      Equal.trans(Nat, List.length(&2, F32, T.rcat(t, x <> acc)), Nat.add(List.length(&2, F32, t), 1n+List.length(&2, F32, acc)), 1n+Nat.add(List.length(&2, F32, t), List.length(&2, F32, acc)), len_rcat(t, x <> acc), Equal.sym(Nat, 1n+Nat.add(List.length(&2, F32, t), List.length(&2, F32, acc)), Nat.add(List.length(&2, F32, t), 1n+List.length(&2, F32, acc)), NL.add_succ(List.length(&2, F32, t), List.length(&2, F32, acc))))
172
173# drow's row has the current dot, the m after it, and acc: 1 + m + |acc| numbers
174def len_drow(m: Nat, +hd: Nat, +ia: U32, +ib: U32, +bs: U32, +acc: List<&2, F32>, r: T.D2) -> {List.length(&2, F32, T.dr_row(T.drow(m, hd, ia, ib, bs, acc, r))) == Nat.add(1n+m, List.length(&2, F32, acc)) : Nat}:
175  match m r:
176    case 0n T.D2{a, b, +s}:
177      Equal.trans(Nat, List.length(&2, F32, T.rcat(s <> acc, Nil{})), Nat.add(1n+List.length(&2, F32, acc), 0n), 1n+List.length(&2, F32, acc), len_rcat(s <> acc, Nil{}), NL.add_zero(1n+List.length(&2, F32, acc)))
178    case 1n++p T.D2{a, b, +s}:
179      Equal.trans(Nat, List.length(&2, F32, T.dr_row(T.drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b)))), Nat.add(1n+p, 1n+List.length(&2, F32, acc)), 2n+Nat.add(p, List.length(&2, F32, acc)), len_drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b)), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(p, 1n+List.length(&2, F32, acc)), 1n+Nat.add(p, List.length(&2, F32, acc)), Equal.sym(Nat, 1n+Nat.add(p, List.length(&2, F32, acc)), Nat.add(p, 1n+List.length(&2, F32, acc)), NL.add_succ(p, List.length(&2, F32, acc)))))
180
181# PROOF (causal_keys): qrow is drow(i, ..) from an empty accumulator, so its row has 1 + i + 0 numbers (len_drow).
182def Laws.causal_keys(i, hd, qs, qc, ks, kc, q, k):
183  Equal.trans(Nat, List.length(&2, F32, T.dr_row(T.qrow(i, hd, qs, qc, ks, kc, q, k))), Nat.add(1n+i, 0n), 1n+i, len_drow(i, hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, ks, Nil{}, T.dot0(hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, 1, 1, q, k)), NL.add_zero(1n+i))
184
185# n - 0 is n
186def sub0(+n: Nat) -> {Nat.sub(n, 0n) == n : Nat}:
187  match n:
188    case 0n:
189      {==}
190    case 1n+p:
191      {==}
192
193# the division loop of a softmax counts the 1 + k numbers it divides onto c (pr_of hands the count on as the row's)
194def cnt_div(q: Array<F32>, k: Array<F32>, kk: Nat, +idx: U32, +s: F32, +c: Nat, r: Array<F32> & F32) -> {T.pr_n(T.pr_of(q, k, T.pdiv(kk, idx, s, c, r))) == Nat.add(1n+kk, c) : Nat}:
195  match kk r:
196    case 0n Tuple{a, +x}:
197      {==}
198    case 1n++j Tuple{a, +x}:
199      Equal.trans(Nat, T.pr_n(T.pr_of(q, k, T.pdiv(j, (idx + 1 : U32), s, 1n+c, Array.get(F32, Array.set(F32, a, idx, (x / s : F32)), (idx + 1 : U32))))), Nat.add(1n+j, 1n+c), 2n+Nat.add(j, c), cnt_div(q, k, j, (idx + 1 : U32), s, 1n+c, Array.get(F32, Array.set(F32, a, idx, (x / s : F32)), (idx + 1 : U32))), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(j, 1n+c), 1n+Nat.add(j, c), Equal.sym(Nat, 1n+Nat.add(j, c), Nat.add(j, 1n+c), NL.add_succ(j, c))))
200
201# the whole softmax over 1 + kk numbers reports 1 + kk, whatever max and exp found (they are matched, not computed)
202def cnt_psm3(q: Array<F32>, k: Array<F32>, +kk: Nat, +off: U32, r: T.AS) -> {T.pr_n(T.pr_of(q, k, T.psm3(kk, off, r))) == 1n+kk : Nat}:
203  match r:
204    case T.AS{a, +s}:
205      Equal.trans(Nat, T.pr_n(T.pr_of(q, k, T.pdiv(kk, off, s, 0n, Array.get(F32, a, off)))), Nat.add(1n+kk, 0n), 1n+kk, cnt_div(q, k, kk, off, s, 0n, Array.get(F32, a, off)), NL.add_zero(1n+kk))
206
207def cnt_psm2(q: Array<F32>, k: Array<F32>, +kk: Nat, +off: U32, r: T.AS) -> {T.pr_n(T.pr_of(q, k, T.psm2(kk, off, r))) == 1n+kk : Nat}:
208  match r:
209    case T.AS{a, +m}:
210      cnt_psm3(q, k, kk, off, T.pexp(kk, off, m, 0.0, Array.get(F32, a, off)))
211
212# pw writes xs and counts them from n; the softmax prow3 runs on them reports 1 + (|xs| + n - 1)
213def cnt_pw(+xs: List<&2, F32>, +idx: U32, +sc: F32, +n: Nat, +off: U32, q: Array<F32>, k: Array<F32>, p: Array<F32>) -> {T.pr_n(T.prow3(off, q, k, T.pw(xs, idx, sc, n, p))) == 1n+Nat.sub(Nat.add(List.length(&2, F32, xs), n), 1n) : Nat}:
214  match xs:
215    case Nil{}:
216      cnt_psm2(q, k, Nat.sub(n, 1n), off, T.pmax0(Nat.sub(n, 1n), off, Array.get(F32, p, off)))
217    case Con{+x, +t}:
218      Equal.trans(Nat, T.pr_n(T.prow3(off, q, k, T.pw(t, (idx + 1 : U32), sc, 1n+n, Array.set(F32, p, idx, (x * sc : F32))))), 1n+Nat.sub(Nat.add(List.length(&2, F32, t), 1n+n), 1n), 1n+Nat.sub(1n+Nat.add(List.length(&2, F32, t), n), 1n), cnt_pw(t, (idx + 1 : U32), sc, 1n+n, off, q, k, Array.set(F32, p, idx, (x * sc : F32))), Equal.cong(Nat, Nat, z => 1n+Nat.sub(z, 1n), Nat.add(List.length(&2, F32, t), 1n+n), 1n+Nat.add(List.length(&2, F32, t), n), Equal.sym(Nat, 1n+Nat.add(List.length(&2, F32, t), n), Nat.add(List.length(&2, F32, t), 1n+n), NL.add_succ(List.length(&2, F32, t), n))))
219
220# the count prow2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_pw
221def cnt_drow(m: Nat, +hd: Nat, +ia: U32, +ib: U32, +bs: U32, +acc: List<&2, F32>, r: T.D2, +sc: F32, +off: U32, pa: Array<F32>) -> {T.pr_n(T.prow2(sc, off, pa, T.drow(m, hd, ia, ib, bs, acc, r))) == Nat.add(1n+m, List.length(&2, F32, acc)) : Nat}:
222  match m r:
223    case 0n T.D2{a, b, +s}:
224      +rw = T.rcat(s <> acc, Nil{})
225      +la = List.length(&2, F32, acc)
226      Equal.trans(Nat, T.pr_n(T.prow3(off, a, b, T.pw(rw, off, sc, 0n, pa))), 1n+Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), 1n+la, cnt_pw(rw, off, sc, 0n, off, a, b, pa),
227        Equal.cong(Nat, Nat, z => 1n+z, Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), la,
228          Equal.trans(Nat, Nat.sub(Nat.add(List.length(&2, F32, rw), 0n), 1n), Nat.sub(1n+la, 1n), la,
229            Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), Nat.add(List.length(&2, F32, rw), 0n), 1n+la,
230              Equal.trans(Nat, Nat.add(List.length(&2, F32, rw), 0n), List.length(&2, F32, rw), 1n+la, NL.add_zero(List.length(&2, F32, rw)),
231                Equal.trans(Nat, List.length(&2, F32, rw), Nat.add(1n+la, 0n), 1n+la, len_rcat(s <> acc, Nil{}), NL.add_zero(1n+la)))),
232            sub0(la))))
233    case 1n++p T.D2{a, b, +s}:
234      Equal.trans(Nat, T.pr_n(T.prow2(sc, off, pa, T.drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b)))), Nat.add(1n+p, 1n+List.length(&2, F32, acc)), 2n+Nat.add(p, List.length(&2, F32, acc)), cnt_drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b), sc, off, pa), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(p, 1n+List.length(&2, F32, acc)), 1n+Nat.add(p, List.length(&2, F32, acc)), Equal.sym(Nat, 1n+Nat.add(p, List.length(&2, F32, acc)), Nat.add(p, 1n+List.length(&2, F32, acc)), NL.add_succ(p, List.length(&2, F32, acc)))))
235
236# PROOF (causal): prow runs prow2 on qrow's row, drow(i, ..) from an empty accumulator, so the count it hands the
237# softmax is 1 + i + 0 (cnt_drow).
238def Laws.causal(i, t, hd, sc, qs, qc, ks, kc, q, k, p):
239  Equal.trans(Nat, T.pr_n(T.prow(i, t, hd, sc, qs, qc, ks, kc, q, k, p)), Nat.add(1n+i, 0n), 1n+i, cnt_drow(i, hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, ks, Nil{}, T.dot0(hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, 1, 1, q, k), sc, (U32.from_nat(i) * U32.from_nat(t) : U32), p), NL.add_zero(1n+i))
240
241# gw writes xs and counts them from n: gr3 hands on |xs| + n (as cnt_pw for the forward pass)
242def cnt_gw(+xs: List<&2, F32>, +idx: U32, +n: Nat, +sc: F32, +off: U32, d: Array<F32>, v: Array<F32>, p: Array<F32>, g: Array<F32>) -> {T.gr_n(T.gr3(sc, off, d, v, p, T.gw(xs, idx, n, g))) == Nat.add(List.length(&2, F32, xs), n) : Nat}:
243  match xs:
244    case Nil{}:
245      {==}
246    case Con{+x, +t}:
247      Equal.trans(Nat, T.gr_n(T.gr3(sc, off, d, v, p, T.gw(t, (idx + 1 : U32), 1n+n, Array.set(F32, g, idx, x)))), Nat.add(List.length(&2, F32, t), 1n+n), 1n+Nat.add(List.length(&2, F32, t), n), cnt_gw(t, (idx + 1 : U32), 1n+n, sc, off, d, v, p, Array.set(F32, g, idx, x)), Equal.sym(Nat, 1n+Nat.add(List.length(&2, F32, t), n), Nat.add(List.length(&2, F32, t), 1n+n), NL.add_succ(List.length(&2, F32, t), n)))
248
249# the count gr2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_gw (cnt_drow's twin)
250def cnt_gdrow(m: Nat, +hd: Nat, +ia: U32, +ib: U32, +bs: U32, +acc: List<&2, F32>, r: T.D2, +sc: F32, +off: U32, pa: Array<F32>, ga: Array<F32>) -> {T.gr_n(T.gr2(sc, off, pa, ga, T.drow(m, hd, ia, ib, bs, acc, r))) == Nat.add(1n+m, List.length(&2, F32, acc)) : Nat}:
251  match m r:
252    case 0n T.D2{a, b, +s}:
253      +rw = T.rcat(s <> acc, Nil{})
254      Equal.trans(Nat, T.gr_n(T.gr3(sc, off, a, b, pa, T.gw(rw, off, 0n, ga))), Nat.add(List.length(&2, F32, rw), 0n), 1n+List.length(&2, F32, acc), cnt_gw(rw, off, 0n, sc, off, a, b, pa, ga),
255        Equal.trans(Nat, Nat.add(List.length(&2, F32, rw), 0n), List.length(&2, F32, rw), 1n+List.length(&2, F32, acc), NL.add_zero(List.length(&2, F32, rw)),
256          Equal.trans(Nat, List.length(&2, F32, rw), Nat.add(1n+List.length(&2, F32, acc), 0n), 1n+List.length(&2, F32, acc), len_rcat(s <> acc, Nil{}), NL.add_zero(1n+List.length(&2, F32, acc)))))
257    case 1n++p T.D2{a, b, +s}:
258      Equal.trans(Nat, T.gr_n(T.gr2(sc, off, pa, ga, T.drow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b)))), Nat.add(1n+p, 1n+List.length(&2, F32, acc)), 2n+Nat.add(p, List.length(&2, F32, acc)), cnt_gdrow(p, hd, ia, (ib + bs : U32), bs, s <> acc, T.dot0(hd, ia, (ib + bs : U32), 1, 1, a, b), sc, off, pa, ga), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(p, 1n+List.length(&2, F32, acc)), 1n+Nat.add(p, List.length(&2, F32, acc)), Equal.sym(Nat, 1n+Nat.add(p, List.length(&2, F32, acc)), Nat.add(p, 1n+List.length(&2, F32, acc)), NL.add_succ(p, List.length(&2, F32, acc)))))
259
260# PROOF (causal_grad): grow runs gr2 on drow(i, ..) from an empty accumulator, so the count is 1 + i + 0 (cnt_gdrow).
261def Laws.causal_grad(i, t, hd, sc, ds, dc, vs, vc, d, v, p, g):
262  Equal.trans(Nat, T.gr_n(T.grow(i, t, hd, sc, ds, dc, vs, vc, d, v, p, g)), Nat.add(1n+i, 0n), 1n+i, cnt_gdrow(i, hd, ((U32.from_nat(i) * ds : U32) + dc : U32), vc, vs, Nil{}, T.dot0(hd, ((U32.from_nat(i) * ds : U32) + dc : U32), vc, 1, 1, d, v), sc, (U32.from_nat(i) * U32.from_nat(t) : U32), p, g), NL.add_zero(1n+i))
263
264# PROOF (full_keys, full, full_grad): the causal proofs with m in place of i, because a full row reads every key
265# 0..m; the row's count is then 1 + m from the same drow lemmas.
266def Laws.full_keys(i, m, hd, qs, qc, ks, kc, q, k):
267  Equal.trans(Nat, List.length(&2, F32, T.dr_row(T.frow(i, m, hd, qs, qc, ks, kc, q, k))), Nat.add(1n+m, 0n), 1n+m, len_drow(m, hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, ks, Nil{}, T.dot0(hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, 1, 1, q, k)), NL.add_zero(1n+m))
268
269def Laws.full(i, m, hd, sc, qs, qc, ks, kc, q, k, pa):
270  Equal.trans(Nat, T.pr_n(T.fprow(i, m, hd, sc, qs, qc, ks, kc, q, k, pa)), Nat.add(1n+m, 0n), 1n+m, cnt_drow(m, hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, ks, Nil{}, T.dot0(hd, ((U32.from_nat(i) * qs : U32) + qc : U32), kc, 1, 1, q, k), sc, (U32.from_nat(i) * U32.from_nat(1n+m) : U32), pa), NL.add_zero(1n+m))
271
272def Laws.full_grad(i, m, hd, sc, ds, dc, vs, vc, d, v, pa, ga):
273  Equal.trans(Nat, T.gr_n(T.fgrow(i, m, hd, sc, ds, dc, vs, vc, d, v, pa, ga)), Nat.add(1n+m, 0n), 1n+m, cnt_gdrow(m, hd, ((U32.from_nat(i) * ds : U32) + dc : U32), vc, vs, Nil{}, T.dot0(hd, ((U32.from_nat(i) * ds : U32) + dc : U32), vc, 1, 1, d, v), sc, (U32.from_nat(i) * U32.from_nat(1n+m) : U32), pa, ga), NL.add_zero(1n+m))
274
275# =====================================================================================================
276# Attention's trees of sequences: parallel = sequential
277# =====================================================================================================
278
279# a ++ b == a2 ++ b2 from a == a2 and b == b2
280def app2(-A: Type, -a: List<&1, A>, -a2: List<&1, A>, -b: List<&1, A>, -b2: List<&1, A>, ea: {a == a2 : List<&1, A>}, eb: {b == b2 : List<&1, A>}) -> {List.append(&1, A, a, b) == List.append(&1, A, a2, b2) : List<&1, A>}:
281  Equal.trans(List<&1, A>, List.append(&1, A, a, b), List.append(&1, A, a2, b), List.append(&1, A, a2, b2), Equal.cong(List<&1, A>, List<&1, A>, z => List.append(&1, A, z, b), a, a2, ea), Equal.cong(List<&1, A>, List<&1, A>, z => List.append(&1, A, a2, z), b, b2, eb))
282
283# ---- the sequential map the tree is compared with: f(x) = fs_o(fheads(h, 0, dm, x)) for each x, in order ----
284
285def fmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.FS>) -> List<&1, Array<F32>>:
286  match xs:
287    case Nil{}:
288      Nil{}
289    case Con{x, t}:
290      T.fs_o(T.fheads(h, 0n, dm, x)) <> fmap(h, dm, t)
291
292# ---- fleaf (the code's loop with an accumulator) is the map pushed onto the accumulator ----
293
294type L1R<-h: Nat, -dm: T.Dm, -xs: List<&1, T.FS>, -acc: List<&1, Array<F32>>> is Type:
295  L1R{ys: List<&1, T.FS>, same: {ys == xs : List<&1, T.FS>}, fact: {T.fleaf(xs, h, dm, acc) == List.reverse.go(&1, Array<F32>, acc, fmap(h, dm, xs)) : List<&1, Array<F32>>}}
296
297def l1_con(x: T.FS, -t: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array<F32>>, r: L1R<h, dm, t, T.fs_o(T.fheads(h, 0n, dm, x)) <> acc>) -> L1R<h, dm, x <> t, acc>:
298  match r:
299    case L1R{ys, same, fact}:
300      L1R{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), fact}
301
302def l1(xs: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array<F32>>) -> L1R<h, dm, xs, acc>:
303  match xs:
304    case Nil{}:
305      L1R{Nil{}, {==}, {==}}
306    case Con{x, t}:
307      l1_con(x, t, h, dm, acc, l1(t, h, dm, T.fs_o(T.fheads(h, 0n, dm, x)) <> acc))
308
309# ---- the map of two lists appended is the two maps appended ----
310
311type MAR<-h: Nat, -dm: T.Dm, -a: List<&1, T.FS>, -b: List<&1, T.FS>> is Type:
312  MAR{ys: List<&1, T.FS>, same: {ys == a : List<&1, T.FS>}, fact: {fmap(h, dm, List.append(&1, T.FS, a, b)) == List.append(&1, Array<F32>, fmap(h, dm, a), fmap(h, dm, b)) : List<&1, Array<F32>>}}
313
314def ma_con(x: T.FS, -t: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>, r: MAR<h, dm, t, b>) -> MAR<h, dm, x <> t, b>:
315  match r:
316    case MAR{ys, same, fact}:
317      MAR{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), Equal.cong(List<&1, Array<F32>>, List<&1, Array<F32>>, z => T.fs_o(T.fheads(h, 0n, dm, x)) <> z, fmap(h, dm, List.append(&1, T.FS, t, b)), List.append(&1, Array<F32>, fmap(h, dm, t), fmap(h, dm, b)), fact)}
318
319def map_app(a: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>) -> MAR<h, dm, a, b>:
320  match a:
321    case Nil{}:
322      MAR{Nil{}, {==}, {==}}
323    case Con{x, t}:
324      ma_con(x, t, h, dm, b, map_app(t, h, dm, b))
325
326# ---- a reversed onto b, then c appended: a reversed onto b ++ c ----
327
328type GAR<-a: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>> is Type:
329  GAR{ys: List<&1, T.FS>, same: {ys == a : List<&1, T.FS>}, fact: {List.append(&1, T.FS, List.reverse.go(&1, T.FS, a, b), c) == List.reverse.go(&1, T.FS, a, List.append(&1, T.FS, b, c)) : List<&1, T.FS>}}
330
331def ga_con(x: T.FS, -t: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>, r: GAR<t, x <> b, c>) -> GAR<x <> t, b, c>:
332  match r:
333    case GAR{ys, same, fact}:
334      GAR{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), fact}
335
336def go_app(a: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>) -> GAR<a, b, c>:
337  match a:
338    case Nil{}:
339      GAR{Nil{}, {==}, {==}}
340    case Con{x, t}:
341      ga_con(x, t, b, c, go_app(t, x <> b, c))
342
343# ---- cut gives two halves that, appended, are acc reversed onto xs ----
344
345type CGR<-k: Nat, -xs: List<&1, T.FS>, -acc: List<&1, T.FS>> is Type:
346  CGR{hh: T.Halves<T.FS>, same: {hh == T.cut(T.FS, k, xs, acc) : T.Halves<T.FS>}, cat: {T.hcat(T.FS, hh) == List.reverse.go(&1, T.FS, acc, xs) : List<&1, T.FS>}}
347
348def cg_base(-k: Nat, xs: List<&1, T.FS>, -acc: List<&1, T.FS>, e: {T.cut(T.FS, k, xs, acc) == T.Halves{List.reverse(&1, T.FS, acc), xs} : T.Halves<T.FS>}, r: GAR<acc, Nil{}, xs>) -> CGR<k, xs, acc>:
349  match r:
350    case GAR{ys, +same, fact}:
351      CGR{T.Halves{List.reverse(&1, T.FS, ys), xs},
352        Equal.trans(T.Halves<T.FS>, T.Halves{List.reverse(&1, T.FS, ys), xs}, T.Halves{List.reverse(&1, T.FS, acc), xs}, T.cut(T.FS, k, xs, acc), Equal.cong(List<&1, T.FS>, T.Halves<T.FS>, z => T.Halves{List.reverse(&1, T.FS, z), xs}, ys, acc, same), Equal.sym(T.Halves<T.FS>, T.cut(T.FS, k, xs, acc), T.Halves{List.reverse(&1, T.FS, acc), xs}, e)),
353        Equal.trans(List<&1, T.FS>, List.append(&1, T.FS, List.reverse.go(&1, T.FS, ys, Nil{}), xs), List.append(&1, T.FS, List.reverse.go(&1, T.FS, acc, Nil{}), xs), List.reverse.go(&1, T.FS, acc, xs), Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => List.append(&1, T.FS, List.reverse.go(&1, T.FS, z, Nil{}), xs), ys, acc, same), fact)}
354
355def cg_con(-m: Nat, -x: T.FS, -t: List<&1, T.FS>, -acc: List<&1, T.FS>, r: CGR<m, t, x <> acc>) -> CGR<1n+m, x <> t, acc>:
356  match r:
357    case CGR{hh, same, cat}:
358      CGR{hh, same, cat}
359
360def cg(k: Nat, xs: List<&1, T.FS>, acc: List<&1, T.FS>) -> CGR<k, xs, acc>:
361  match k xs:
362    case 1n+m Con{x, t}:
363      cg_con(m, x, t, acc, cg(m, t, x <> acc))
364    case 0n ys:
365      cg_base(0n, ys, acc, {==}, go_app(acc, Nil{}, ys))
366    case 1n+m Nil{}:
367      cg_base(1n+m, Nil{}, acc, {==}, go_app(acc, Nil{}, Nil{}))
368
369# ---- the tree: fpar at depth d on two halves is the map of the halves appended ----
370
371type MR<-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, -h: Nat, -dm: T.Dm> is Type:
372  MR{ys: List<&1, T.FS>, same: {ys == T.hcat(T.FS, gs) : List<&1, T.FS>}, fact: {T.fpar(d, gs, n, h, dm) == fmap(h, dm, T.hcat(T.FS, gs)) : List<&1, Array<F32>>}}
373
374# depth 0: the two leaves' loops, appended
375def m0c(-l: List<&1, T.FS>, -r: List<&1, T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, -l1y: List<&1, T.FS>, +sl: {l1y == l : List<&1, T.FS>}, fl: {T.fleaf(l, h, dm, Nil{}) == fmap(h, dm, l) : List<&1, Array<F32>>}, r1: List<&1, T.FS>, sr: {r1 == r : List<&1, T.FS>}, fr: {T.fleaf(r, h, dm, Nil{}) == fmap(h, dm, r) : List<&1, Array<F32>>}, c: MAR<h, dm, l1y, r>) -> MR<0n, T.Halves{l, r}, n, h, dm>:
376  match c:
377    case MAR{l2, s2, fa}:
378      MR{List.append(&1, T.FS, l2, r1), app2(T.FS, l2, l, r1, r, Equal.trans(List<&1, T.FS>, l2, l1y, l, s2, sl), sr),
379        Equal.trans(List<&1, Array<F32>>, List.append(&1, Array<F32>, T.fleaf(l, h, dm, Nil{}), T.fleaf(r, h, dm, Nil{})), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), fmap(h, dm, List.append(&1, T.FS, l, r)), app2(Array<F32>, T.fleaf(l, h, dm, Nil{}), fmap(h, dm, l), T.fleaf(r, h, dm, Nil{}), fmap(h, dm, r), fl, fr),
380          Equal.sym(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, l, r)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)),
381            Equal.trans(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, l, r)), fmap(h, dm, List.append(&1, T.FS, l1y, r)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, List.append(&1, T.FS, z, r)), l, l1y, Equal.sym(List<&1, T.FS>, l1y, l, sl)),
382              Equal.trans(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, l1y, r)), List.append(&1, Array<F32>, fmap(h, dm, l1y), fmap(h, dm, r)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), fa, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => List.append(&1, Array<F32>, fmap(h, dm, z), fmap(h, dm, r)), l1y, l, sl)))))}
383
384def m0b(-l: List<&1, T.FS>, -r: List<&1, T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, l1y: List<&1, T.FS>, +sl: {l1y == l : List<&1, T.FS>}, fl: {T.fleaf(l, h, dm, Nil{}) == fmap(h, dm, l) : List<&1, Array<F32>>}, b: L1R<h, dm, r, Nil{}>) -> MR<0n, T.Halves{l, r}, n, h, dm>:
385  match b:
386    case L1R{r1, sr, fr}:
387      m0c(l, r, n, h, dm, l1y, sl, fl, r1, sr, fr, map_app(l1y, h, dm, r))
388
389def m0a(-l: List<&1, T.FS>, r: List<&1, T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, a: L1R<h, dm, l, Nil{}>) -> MR<0n, T.Halves{l, r}, n, h, dm>:
390  match a:
391    case L1R{l1y, sl, fl}:
392      m0b(l, r, n, h, dm, l1y, sl, fl, l1(r, h, dm, Nil{}))
393
394# depth 1 + e: each half cut in two and its tree (the closures run main at depth e), then the two maps appended
395def m1c(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.FS>, s1: {hh1 == T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.FS>}, +cat1: {T.hcat(T.FS, hh1) == l : List<&1, T.FS>}, -hh2: T.Halves<T.FS>, s2: {hh2 == T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.FS>}, +cat2: {T.hcat(T.FS, hh2) == r : List<&1, T.FS>}, -y1: List<&1, T.FS>, sy1: {y1 == T.hcat(T.FS, hh1) : List<&1, T.FS>}, f1: {T.fpar(e, hh1, TA.half(n), h, dm) == fmap(h, dm, T.hcat(T.FS, hh1)) : List<&1, Array<F32>>}, y2: List<&1, T.FS>, sy2: {y2 == T.hcat(T.FS, hh2) : List<&1, T.FS>}, f2: {T.fpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm) == fmap(h, dm, T.hcat(T.FS, hh2)) : List<&1, Array<F32>>}, ma: MAR<h, dm, y1, y2>) -> MR<1n+e, T.Halves{l, r}, n, h, dm>:
396  match ma:
397    case MAR{y1b, sb, fa}:
398      +ly1 = Equal.trans(List<&1, T.FS>, y1, T.hcat(T.FS, hh1), l, sy1, cat1)
399      +ly2 = Equal.trans(List<&1, T.FS>, y2, T.hcat(T.FS, hh2), r, sy2, cat2)
400      +q1 = Equal.trans(List<&1, Array<F32>>, T.fpar(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.fpar(e, hh1, TA.half(n), h, dm), fmap(h, dm, l), Equal.cong(T.Halves<T.FS>, List<&1, Array<F32>>, z => T.fpar(e, z, TA.half(n), h, dm), T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), hh1, Equal.sym(T.Halves<T.FS>, hh1, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), s1)), Equal.trans(List<&1, Array<F32>>, T.fpar(e, hh1, TA.half(n), h, dm), fmap(h, dm, T.hcat(T.FS, hh1)), fmap(h, dm, l), f1, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), T.hcat(T.FS, hh1), l, cat1)))
401      +q2 = Equal.trans(List<&1, Array<F32>>, T.fpar(e, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), T.fpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm), fmap(h, dm, r), Equal.cong(T.Halves<T.FS>, List<&1, Array<F32>>, z => T.fpar(e, z, Nat.sub(n, TA.half(n)), h, dm), T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), hh2, Equal.sym(T.Halves<T.FS>, hh2, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), s2)), Equal.trans(List<&1, Array<F32>>, T.fpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm), fmap(h, dm, T.hcat(T.FS, hh2)), fmap(h, dm, r), f2, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), T.hcat(T.FS, hh2), r, cat2)))
402      +bb = Equal.trans(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, l, r)), fmap(h, dm, List.append(&1, T.FS, y1, y2)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), List.append(&1, T.FS, l, r), List.append(&1, T.FS, y1, y2), app2(T.FS, l, y1, r, y2, Equal.sym(List<&1, T.FS>, y1, l, ly1), Equal.sym(List<&1, T.FS>, y2, r, ly2))), Equal.trans(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, y1, y2)), List.append(&1, Array<F32>, fmap(h, dm, y1), fmap(h, dm, y2)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), fa, app2(Array<F32>, fmap(h, dm, y1), fmap(h, dm, l), fmap(h, dm, y2), fmap(h, dm, r), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), y1, l, ly1), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), y2, r, ly2))))
403      MR{List.append(&1, T.FS, y1b, y2), app2(T.FS, y1b, l, y2, r, Equal.trans(List<&1, T.FS>, y1b, y1, l, sb, ly1), ly2),
404        Equal.trans(List<&1, Array<F32>>, List.append(&1, Array<F32>, T.fpar(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.fpar(e, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), fmap(h, dm, List.append(&1, T.FS, l, r)), app2(Array<F32>, T.fpar(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), fmap(h, dm, l), T.fpar(e, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), fmap(h, dm, r), q1, q2), Equal.sym(List<&1, Array<F32>>, fmap(h, dm, List.append(&1, T.FS, l, r)), List.append(&1, Array<F32>, fmap(h, dm, l), fmap(h, dm, r)), bb))}
405
406def m1b(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.FS>, s1: {hh1 == T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.FS>}, cat1: {T.hcat(T.FS, hh1) == l : List<&1, T.FS>}, -hh2: T.Halves<T.FS>, s2: {hh2 == T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.FS>}, cat2: {T.hcat(T.FS, hh2) == r : List<&1, T.FS>}, r1: MR<e, hh1, TA.half(n), h, dm>, r2: MR<e, hh2, Nat.sub(n, TA.half(n)), h, dm>) -> MR<1n+e, T.Halves{l, r}, n, h, dm>:
407  match r1 r2:
408    case MR{y1, sy1, f1} MR{y2, sy2, f2}:
409      m1c(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, y1, sy1, f1, y2, sy2, f2, map_app(y1, h, dm, y2))
410
411def m1a(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, c1: CGR<TA.half(TA.half(n)), l, Nil{}>, c2: CGR<TA.half(Nat.sub(n, TA.half(n))), r, Nil{}>, k1: @g: T.Halves<T.FS> -> MR<e, g, TA.half(n), h, dm>, k2: @g: T.Halves<T.FS> -> MR<e, g, Nat.sub(n, TA.half(n)), h, dm>) -> MR<1n+e, T.Halves{l, r}, n, h, dm>:
412  match c1 c2:
413    case CGR{hh1, s1, cat1} CGR{hh2, s2, cat2}:
414      m1b(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, k1(hh1), k2(hh2))
415
416def tree(d: Nat, gs: T.Halves<T.FS>, +n: Nat, +h: Nat, +dm: T.Dm) -> MR<d, gs, n, h, dm>:
417  match d gs:
418    case 0n T.Halves{l, r}:
419      m0a(l, r, n, h, dm, l1(l, h, dm, Nil{}))
420    case 1n++e T.Halves{l, r}:
421      m1a(e, l, r, n, h, dm, cg(TA.half(TA.half(n)), l, Nil{}), cg(TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), g1 => tree(e, g1, TA.half(n), h, dm), g2 => tree(e, g2, Nat.sub(n, TA.half(n)), h, dm))
422
423# the law: the tree gives what fleaf, the loop over the sequences one after another, gives
424def par_fin(-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, -ys: List<&1, T.FS>, +sy: {ys == T.hcat(T.FS, gs) : List<&1, T.FS>}, f: {T.fpar(d, gs, n, h, dm) == fmap(h, dm, T.hcat(T.FS, gs)) : List<&1, Array<F32>>}, r: L1R<h, dm, ys, Nil{}>) -> {T.fpar(d, gs, n, h, dm) == T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array<F32>>}:
425  match r:
426    case L1R{ys2, s2, fl}:
427      Equal.trans(List<&1, Array<F32>>, T.fpar(d, gs, n, h, dm), fmap(h, dm, T.hcat(T.FS, gs)), T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}), f,
428        Equal.sym(List<&1, Array<F32>>, T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}), fmap(h, dm, T.hcat(T.FS, gs)),
429          Equal.trans(List<&1, Array<F32>>, T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}), T.fleaf(ys, h, dm, Nil{}), fmap(h, dm, T.hcat(T.FS, gs)), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => T.fleaf(z, h, dm, Nil{}), T.hcat(T.FS, gs), ys, Equal.sym(List<&1, T.FS>, ys, T.hcat(T.FS, gs), sy)),
430            Equal.trans(List<&1, Array<F32>>, T.fleaf(ys, h, dm, Nil{}), fmap(h, dm, ys), fmap(h, dm, T.hcat(T.FS, gs)), fl, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => fmap(h, dm, z), ys, T.hcat(T.FS, gs), sy)))))
431
432def par_mid(-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, r: MR<d, gs, n, h, dm>) -> {T.fpar(d, gs, n, h, dm) == T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array<F32>>}:
433  match r:
434    case MR{ys, sy, f}:
435      par_fin(d, gs, n, h, dm, ys, sy, f, l1(ys, h, dm, Nil{}))
436
437def ffmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.FS>) -> List<&1, Array<F32>>:
438  match xs:
439    case Nil{}:
440      Nil{}
441    case Con{x, t}:
442      T.fs_o(T.fheads_full(h, 0n, dm, x)) <> ffmap(h, dm, t)
443
444# ---- fleaf (the code's loop with an accumulator) is the map pushed onto the accumulator ----
445
446type L1RF<-h: Nat, -dm: T.Dm, -xs: List<&1, T.FS>, -acc: List<&1, Array<F32>>> is Type:
447  L1RF{ys: List<&1, T.FS>, same: {ys == xs : List<&1, T.FS>}, fact: {T.fleaf_full(xs, h, dm, acc) == List.reverse.go(&1, Array<F32>, acc, ffmap(h, dm, xs)) : List<&1, Array<F32>>}}
448
449def lf_con(x: T.FS, -t: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array<F32>>, r: L1RF<h, dm, t, T.fs_o(T.fheads_full(h, 0n, dm, x)) <> acc>) -> L1RF<h, dm, x <> t, acc>:
450  match r:
451    case L1RF{ys, same, fact}:
452      L1RF{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), fact}
453
454def lf1(xs: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array<F32>>) -> L1RF<h, dm, xs, acc>:
455  match xs:
456    case Nil{}:
457      L1RF{Nil{}, {==}, {==}}
458    case Con{x, t}:
459      lf_con(x, t, h, dm, acc, lf1(t, h, dm, T.fs_o(T.fheads_full(h, 0n, dm, x)) <> acc))
460
461# ---- the map of two lists appended is the two maps appended ----
462
463type MARF<-h: Nat, -dm: T.Dm, -a: List<&1, T.FS>, -b: List<&1, T.FS>> is Type:
464  MARF{ys: List<&1, T.FS>, same: {ys == a : List<&1, T.FS>}, fact: {ffmap(h, dm, List.append(&1, T.FS, a, b)) == List.append(&1, Array<F32>, ffmap(h, dm, a), ffmap(h, dm, b)) : List<&1, Array<F32>>}}
465
466def ma_conf(x: T.FS, -t: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>, r: MARF<h, dm, t, b>) -> MARF<h, dm, x <> t, b>:
467  match r:
468    case MARF{ys, same, fact}:
469      MARF{x <> ys, Equal.cong(List<&1, T.FS>, List<&1, T.FS>, z => x <> z, ys, t, same), Equal.cong(List<&1, Array<F32>>, List<&1, Array<F32>>, z => T.fs_o(T.fheads_full(h, 0n, dm, x)) <> z, ffmap(h, dm, List.append(&1, T.FS, t, b)), List.append(&1, Array<F32>, ffmap(h, dm, t), ffmap(h, dm, b)), fact)}
470
471def map_appf(a: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>) -> MARF<h, dm, a, b>:
472  match a:
473    case Nil{}:
474      MARF{Nil{}, {==}, {==}}
475    case Con{x, t}:
476      ma_conf(x, t, h, dm, b, map_appf(t, h, dm, b))
477
478# ---- a reversed onto b, then c appended: a reversed onto b ++ c ----
479
480type MRF<-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, -h: Nat, -dm: T.Dm> is Type:
481  MRF{ys: List<&1, T.FS>, same: {ys == T.hcat(T.FS, gs) : List<&1, T.FS>}, fact: {T.fpar_full(d, gs, n, h, dm) == ffmap(h, dm, T.hcat(T.FS, gs)) : List<&1, Array<F32>>}}
482
483# depth 0: the two leaves' loops, appended
484def fm0c(-l: List<&1, T.FS>, -r: List<&1, T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, -l1y: List<&1, T.FS>, +sl: {l1y == l : List<&1, T.FS>}, fl: {T.fleaf_full(l, h, dm, Nil{}) == ffmap(h, dm, l) : List<&1, Array<F32>>}, r1: List<&1, T.FS>, sr: {r1 == r : List<&1, T.FS>}, fr: {T.fleaf_full(r, h, dm, Nil{}) == ffmap(h, dm, r) : List<&1, Array<F32>>}, c: MARF<h, dm, l1y, r>) -> MRF<0n, T.Halves{l, r}, n, h, dm>:
485  match c:
486    case MARF{l2, s2, fa}:
487      MRF{List.append(&1, T.FS, l2, r1), app2(T.FS, l2, l, r1, r, Equal.trans(List<&1, T.FS>, l2, l1y, l, s2, sl), sr),
488        Equal.trans(List<&1, Array<F32>>, List.append(&1, Array<F32>, T.fleaf_full(l, h, dm, Nil{}), T.fleaf_full(r, h, dm, Nil{})), List.append(&1, Array<F32>, ffmap(h, dm, l), ffmap(h, dm, r)), ffmap(h, dm, List.append(&1, T.FS, l, r)), app2(Array<F32>, T.fleaf_full(l, h, dm, Nil{}), ffmap(h, dm, l), T.fleaf_full(r, h, dm, Nil{}), ffmap(h, dm, r), fl, fr),
489          Equal.sym(List<&1, Array<F32>>, ffmap(h, dm, List.append(&1, T.FS, l, r)), List.append(&1, Array<F32>, ffmap(h, dm, l), ffmap(h, dm, r)),
490            Equal.trans(List<&1, Array<F32>>, ffmap(h, dm, List.append(&1, T.FS, l, r)), ffmap(h, dm, List.append(&1, T.FS, l1y, r)), List.append(&1, Array<F32>, ffmap(h, dm, l), ffmap(h, dm, r)), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => ffmap(h, dm, List.append(&1, T.FS, z, r)), l, l1y, Equal.sym(List<&1, T.FS>, l1y, l, sl)),
491              Equal.trans(List<&1, Array<F32>>, ffmap(h, dm, List.append(&1, T.FS, l1y, r)), List.append(&1, Array<F32>, ffmap(h, dm, l1y), ffmap(h, dm, r)), List.append(&1, Array<F32>, ffmap(h, dm, l), ffmap(h, dm, r)), fa, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => List.append(&1, Array<F32>, ffmap(h, dm, z), ffmap(h, dm, r)), l1y, l, sl)))))}
492
493def fm0b(-l: List<&1, T.FS>, -r: List<&1, T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, l1y: List<&1, T.FS>, +sl: {l1y == l : List<&1, T.FS>}, fl: {T.fleaf_full(l, h, dm, Nil{}) == ffmap(h, dm, l) : List<&1, Array<F32>>}, b: L1RF<h, dm, r, Nil{}>) -> MRF<0n, T.Halves{l, r}, n, h, dm>:
494  match b:
495    case L1RF{r1, sr, fr}:
496      fm0c(l, r, n, h, dm, l1y, sl, fl, r1, sr, fr, map_appf(l1y, h, dm, r))
497
498def fm0a(-l: List<&1, T.FS>, r: List<&1, T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, a: L1RF<h, dm, l, Nil{}>) -> MRF<0n, T.Halves{l, r}, n, h, dm>:
499  match a:
500    case L1RF{l1y, sl, fl}:
501      fm0b(l, r, n, h, dm, l1y, sl, fl, lf1(r, h, dm, Nil{}))
502
503# depth 1 + e: each half cut in two and its treef (the closures run main at depth e), then the two maps appended
504def fm1c(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.FS>, s1: {hh1 == T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.FS>}, +cat1: {T.hcat(T.FS, hh1) == l : List<&1, T.FS>}, -hh2: T.Halves<T.FS>, s2: {hh2 == T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.FS>}, +cat2: {T.hcat(T.FS, hh2) == r : List<&1, T.FS>}, -y1: List<&1, T.FS>, sy1: {y1 == T.hcat(T.FS, hh1) : List<&1, T.FS>}, f1: {T.fpar_full(e, hh1, TA.half(n), h, dm) == ffmap(h, dm, T.hcat(T.FS, hh1)) : List<&1, Array<F32>>}, y2: List<&1, T.FS>, sy2: {y2 == T.hcat(T.FS, hh2) : List<&1, T.FS>}, f2: {T.fpar_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm) == ffmap(h, dm, T.hcat(T.FS, hh2)) : List<&1, Array<F32>>}, ma: MARF<h, dm, y1, y2>) -> MRF<1n+e, T.Halves{l, r}, n, h, dm>:
505  match ma:
506    case MARF{y1b, sb, fa}:
507      +ly1 = Equal.trans(List<&1, T.FS>, y1, T.hcat(T.FS, hh1), l, sy1, cat1)
508      +ly2 = Equal.trans(List<&1, T.FS>, y2, T.hcat(T.FS, hh2), r, sy2, cat2)
509      +q1 = Equal.trans(List<&1, Array<F32>>, T.fpar_full(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.fpar_full(e, hh1, TA.half(n), h, dm), ffmap(h, dm, l), Equal.cong(T.Halves<T.FS>, List<&1, Array<F32>>, z => T.fpar_full(e, z, TA.half(n), h, dm), T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), hh1, Equal.sym(T.Halves<T.FS>, hh1, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), s1)), Equal.trans(List<&1, Array<F32>>, T.fpar_full(e, hh1, TA.half(n), h, dm), ffmap(h, dm, T.hcat(T.FS, hh1)), ffmap(h, dm, l), f1, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => ffmap(h, dm, z), T.hcat(T.FS, hh1), l, cat1)))
510      +q2 = Equal.trans(List<&1, Array<F32>>, T.fpar_full(e, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), T.fpar_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm), ffmap(h, dm, r), Equal.cong(T.Halves<T.FS>, List<&1, Array<F32>>, z => T.fpar_full(e, z, Nat.sub(n, TA.half(n)), h, dm), T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), hh2, Equal.sym(T.Halves<T.FS>, hh2, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), s2)), Equal.trans(List<&1, Array<F32>>, T.fpar_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm), ffmap(h, dm, T.hcat(T.FS, hh2)), ffmap(h, dm, r), f2, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => ffmap(h, dm, z), T.hcat(T.FS, hh2), r, cat2)))
511      +bb = Equal.trans(List<&1, Array<F32>>, ffmap(h, dm, List.append(&1, T.FS, l, r)), ffmap(h, dm, List.append(&1, T.FS, y1, y2)), List.append(&1, Array<F32>, ffmap(h, dm, l), ffmap(h, dm, r)), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => ffmap(h, dm, z), List.append(&1, T.FS, l, r), List.append(&1, T.FS, y1, y2), app2(T.FS, l, y1, r, y2, Equal.sym(List<&1, T.FS>, y1, l, ly1), Equal.sym(List<&1, T.FS>, y2, r, ly2))), Equal.trans(List<&1, Array<F32>>, ffmap(h, dm, List.append(&1, T.FS, y1, y2)), List.append(&1, Array<F32>, ffmap(h, dm, y1), ffmap(h, dm, y2)), List.append(&1, Array<F32>, ffmap(h, dm, l), ffmap(h, dm, r)), fa, app2(Array<F32>, ffmap(h, dm, y1), ffmap(h, dm, l), ffmap(h, dm, y2), ffmap(h, dm, r), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => ffmap(h, dm, z), y1, l, ly1), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => ffmap(h, dm, z), y2, r, ly2))))
512      MRF{List.append(&1, T.FS, y1b, y2), app2(T.FS, y1b, l, y2, r, Equal.trans(List<&1, T.FS>, y1b, y1, l, sb, ly1), ly2),
513        Equal.trans(List<&1, Array<F32>>, List.append(&1, Array<F32>, T.fpar_full(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.fpar_full(e, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm)), List.append(&1, Array<F32>, ffmap(h, dm, l), ffmap(h, dm, r)), ffmap(h, dm, List.append(&1, T.FS, l, r)), app2(Array<F32>, T.fpar_full(e, T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), ffmap(h, dm, l), T.fpar_full(e, T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), ffmap(h, dm, r), q1, q2), Equal.sym(List<&1, Array<F32>>, ffmap(h, dm, List.append(&1, T.FS, l, r)), List.append(&1, Array<F32>, ffmap(h, dm, l), ffmap(h, dm, r)), bb))}
514
515def fm1b(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.FS>, s1: {hh1 == T.cut(T.FS, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.FS>}, cat1: {T.hcat(T.FS, hh1) == l : List<&1, T.FS>}, -hh2: T.Halves<T.FS>, s2: {hh2 == T.cut(T.FS, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.FS>}, cat2: {T.hcat(T.FS, hh2) == r : List<&1, T.FS>}, r1: MRF<e, hh1, TA.half(n), h, dm>, r2: MRF<e, hh2, Nat.sub(n, TA.half(n)), h, dm>) -> MRF<1n+e, T.Halves{l, r}, n, h, dm>:
516  match r1 r2:
517    case MRF{y1, sy1, f1} MRF{y2, sy2, f2}:
518      fm1c(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, y1, sy1, f1, y2, sy2, f2, map_appf(y1, h, dm, y2))
519
520def fm1a(-e: Nat, -l: List<&1, T.FS>, -r: List<&1, T.FS>, +n: Nat, +h: Nat, +dm: T.Dm, c1: CGR<TA.half(TA.half(n)), l, Nil{}>, c2: CGR<TA.half(Nat.sub(n, TA.half(n))), r, Nil{}>, k1: @g: T.Halves<T.FS> -> MRF<e, g, TA.half(n), h, dm>, k2: @g: T.Halves<T.FS> -> MRF<e, g, Nat.sub(n, TA.half(n)), h, dm>) -> MRF<1n+e, T.Halves{l, r}, n, h, dm>:
521  match c1 c2:
522    case CGR{hh1, s1, cat1} CGR{hh2, s2, cat2}:
523      fm1b(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, k1(hh1), k2(hh2))
524
525def treef(d: Nat, gs: T.Halves<T.FS>, +n: Nat, +h: Nat, +dm: T.Dm) -> MRF<d, gs, n, h, dm>:
526  match d gs:
527    case 0n T.Halves{l, r}:
528      fm0a(l, r, n, h, dm, lf1(l, h, dm, Nil{}))
529    case 1n++e T.Halves{l, r}:
530      fm1a(e, l, r, n, h, dm, cg(TA.half(TA.half(n)), l, Nil{}), cg(TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), g1 => treef(e, g1, TA.half(n), h, dm), g2 => treef(e, g2, Nat.sub(n, TA.half(n)), h, dm))
531
532# the law: the treef gives what fleaf, the loop over the sequences one after another, gives
533def par_fin_f(-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, -ys: List<&1, T.FS>, +sy: {ys == T.hcat(T.FS, gs) : List<&1, T.FS>}, f: {T.fpar_full(d, gs, n, h, dm) == ffmap(h, dm, T.hcat(T.FS, gs)) : List<&1, Array<F32>>}, r: L1RF<h, dm, ys, Nil{}>) -> {T.fpar_full(d, gs, n, h, dm) == T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array<F32>>}:
534  match r:
535    case L1RF{ys2, s2, fl}:
536      Equal.trans(List<&1, Array<F32>>, T.fpar_full(d, gs, n, h, dm), ffmap(h, dm, T.hcat(T.FS, gs)), T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}), f,
537        Equal.sym(List<&1, Array<F32>>, T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}), ffmap(h, dm, T.hcat(T.FS, gs)),
538          Equal.trans(List<&1, Array<F32>>, T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}), T.fleaf_full(ys, h, dm, Nil{}), ffmap(h, dm, T.hcat(T.FS, gs)), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => T.fleaf_full(z, h, dm, Nil{}), T.hcat(T.FS, gs), ys, Equal.sym(List<&1, T.FS>, ys, T.hcat(T.FS, gs), sy)),
539            Equal.trans(List<&1, Array<F32>>, T.fleaf_full(ys, h, dm, Nil{}), ffmap(h, dm, ys), ffmap(h, dm, T.hcat(T.FS, gs)), fl, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => ffmap(h, dm, z), ys, T.hcat(T.FS, gs), sy)))))
540
541def par_mid_f(-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, r: MRF<d, gs, n, h, dm>) -> {T.fpar_full(d, gs, n, h, dm) == T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array<F32>>}:
542  match r:
543    case MRF{ys, sy, f}:
544      par_fin_f(d, gs, n, h, dm, ys, sy, f, lf1(ys, h, dm, Nil{}))
545
546# PROOF (attn_par_fwd_full): attn_par_fwd's proof for the full-visible leaf; the depth induction, cut and append
547# lemmas are the same, and cg (which is about cut and hcat, not about a leaf) is shared with it.
548def Laws.attn_par_fwd_full(d, gs, n, h, dm):
549  par_mid_f(d, gs, n, h, dm, treef(d, gs, n, h, dm))
550
551# PROOF (attn_par_fwd): by induction on the depth, each fact handing its list back (the lists hold arrays, so each is
552# used once): a leaf pair is fleaf twice, and fleaf is the map pushed onto its accumulator (l1); the map of two lists
553# appended is the two maps appended (map_app); cut's halves, appended, are the list it cut (cg); a deeper tree is two
554# trees on cut's halves (the closures).
555def Laws.attn_par_fwd(d, gs, n, h, dm):
556  par_mid(d, gs, n, h, dm, tree(d, gs, n, h, dm))
557
558# ---- the sequential map the b_tree is compared with: f(x) = fs_o(fheads(h, 0, dm, x)) for each x, in order ----
559
560def b_fmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.BG>) -> List<&1, T.DB>:
561  match xs:
562    case Nil{}:
563      Nil{}
564    case Con{x, t}:
565      T.db_of(T.bgroups(h, 0n, dm, x)) <> b_fmap(h, dm, t)
566
567# ---- fleaf (the code's loop with an accumulator) is the map pushed onto the accumulator ----
568
569type b_L1R<-h: Nat, -dm: T.Dm, -xs: List<&1, T.BG>, -acc: List<&1, T.DB>> is Type:
570  b_L1R{ys: List<&1, T.BG>, same: {ys == xs : List<&1, T.BG>}, fact: {T.bleaf(xs, h, dm, acc) == List.reverse.go(&1, T.DB, acc, b_fmap(h, dm, xs)) : List<&1, T.DB>}}
571
572def b_l1_con(x: T.BG, -t: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>, r: b_L1R<h, dm, t, T.db_of(T.bgroups(h, 0n, dm, x)) <> acc>) -> b_L1R<h, dm, x <> t, acc>:
573  match r:
574    case b_L1R{ys, same, fact}:
575      b_L1R{x <> ys, Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => x <> z, ys, t, same), fact}
576
577def b_l1(xs: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>) -> b_L1R<h, dm, xs, acc>:
578  match xs:
579    case Nil{}:
580      b_L1R{Nil{}, {==}, {==}}
581    case Con{x, t}:
582      b_l1_con(x, t, h, dm, acc, b_l1(t, h, dm, T.db_of(T.bgroups(h, 0n, dm, x)) <> acc))
583
584# ---- the map of two lists appended is the two maps appended ----
585
586type b_MAR<-h: Nat, -dm: T.Dm, -a: List<&1, T.BG>, -b: List<&1, T.BG>> is Type:
587  b_MAR{ys: List<&1, T.BG>, same: {ys == a : List<&1, T.BG>}, fact: {b_fmap(h, dm, List.append(&1, T.BG, a, b)) == List.append(&1, T.DB, b_fmap(h, dm, a), b_fmap(h, dm, b)) : List<&1, T.DB>}}
588
589def b_ma_con(x: T.BG, -t: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>, r: b_MAR<h, dm, t, b>) -> b_MAR<h, dm, x <> t, b>:
590  match r:
591    case b_MAR{ys, same, fact}:
592      b_MAR{x <> ys, Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => x <> z, ys, t, same), Equal.cong(List<&1, T.DB>, List<&1, T.DB>, z => T.db_of(T.bgroups(h, 0n, dm, x)) <> z, b_fmap(h, dm, List.append(&1, T.BG, t, b)), List.append(&1, T.DB, b_fmap(h, dm, t), b_fmap(h, dm, b)), fact)}
593
594def b_map_app(a: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>) -> b_MAR<h, dm, a, b>:
595  match a:
596    case Nil{}:
597      b_MAR{Nil{}, {==}, {==}}
598    case Con{x, t}:
599      b_ma_con(x, t, h, dm, b, b_map_app(t, h, dm, b))
600
601# ---- a reversed onto b, then c appended: a reversed onto b ++ c ----
602
603type b_GAR<-a: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>> is Type:
604  b_GAR{ys: List<&1, T.BG>, same: {ys == a : List<&1, T.BG>}, fact: {List.append(&1, T.BG, List.reverse.go(&1, T.BG, a, b), c) == List.reverse.go(&1, T.BG, a, List.append(&1, T.BG, b, c)) : List<&1, T.BG>}}
605
606def b_ga_con(x: T.BG, -t: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>, r: b_GAR<t, x <> b, c>) -> b_GAR<x <> t, b, c>:
607  match r:
608    case b_GAR{ys, same, fact}:
609      b_GAR{x <> ys, Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => x <> z, ys, t, same), fact}
610
611def b_go_app(a: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>) -> b_GAR<a, b, c>:
612  match a:
613    case Nil{}:
614      b_GAR{Nil{}, {==}, {==}}
615    case Con{x, t}:
616      b_ga_con(x, t, b, c, b_go_app(t, x <> b, c))
617
618# ---- cut gives two halves that, appended, are acc reversed onto xs ----
619
620type b_CGR<-k: Nat, -xs: List<&1, T.BG>, -acc: List<&1, T.BG>> is Type:
621  b_CGR{hh: T.Halves<T.BG>, same: {hh == T.cut(T.BG, k, xs, acc) : T.Halves<T.BG>}, cat: {T.hcat(T.BG, hh) == List.reverse.go(&1, T.BG, acc, xs) : List<&1, T.BG>}}
622
623def b_cg_base(-k: Nat, xs: List<&1, T.BG>, -acc: List<&1, T.BG>, e: {T.cut(T.BG, k, xs, acc) == T.Halves{List.reverse(&1, T.BG, acc), xs} : T.Halves<T.BG>}, r: b_GAR<acc, Nil{}, xs>) -> b_CGR<k, xs, acc>:
624  match r:
625    case b_GAR{ys, +same, fact}:
626      b_CGR{T.Halves{List.reverse(&1, T.BG, ys), xs},
627        Equal.trans(T.Halves<T.BG>, T.Halves{List.reverse(&1, T.BG, ys), xs}, T.Halves{List.reverse(&1, T.BG, acc), xs}, T.cut(T.BG, k, xs, acc), Equal.cong(List<&1, T.BG>, T.Halves<T.BG>, z => T.Halves{List.reverse(&1, T.BG, z), xs}, ys, acc, same), Equal.sym(T.Halves<T.BG>, T.cut(T.BG, k, xs, acc), T.Halves{List.reverse(&1, T.BG, acc), xs}, e)),
628        Equal.trans(List<&1, T.BG>, List.append(&1, T.BG, List.reverse.go(&1, T.BG, ys, Nil{}), xs), List.append(&1, T.BG, List.reverse.go(&1, T.BG, acc, Nil{}), xs), List.reverse.go(&1, T.BG, acc, xs), Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => List.append(&1, T.BG, List.reverse.go(&1, T.BG, z, Nil{}), xs), ys, acc, same), fact)}
629
630def b_cg_con(-m: Nat, -x: T.BG, -t: List<&1, T.BG>, -acc: List<&1, T.BG>, r: b_CGR<m, t, x <> acc>) -> b_CGR<1n+m, x <> t, acc>:
631  match r:
632    case b_CGR{hh, same, cat}:
633      b_CGR{hh, same, cat}
634
635def b_cg(k: Nat, xs: List<&1, T.BG>, acc: List<&1, T.BG>) -> b_CGR<k, xs, acc>:
636  match k xs:
637    case 1n+m Con{x, t}:
638      b_cg_con(m, x, t, acc, b_cg(m, t, x <> acc))
639    case 0n ys:
640      b_cg_base(0n, ys, acc, {==}, b_go_app(acc, Nil{}, ys))
641    case 1n+m Nil{}:
642      b_cg_base(1n+m, Nil{}, acc, {==}, b_go_app(acc, Nil{}, Nil{}))
643
644# ---- the b_tree: fpar at depth d on two halves is the map of the halves appended ----
645
646type b_MR<-d: Nat, -gs: T.Halves<T.BG>, -n: Nat, -h: Nat, -dm: T.Dm> is Type:
647  b_MR{ys: List<&1, T.BG>, same: {ys == T.hcat(T.BG, gs) : List<&1, T.BG>}, fact: {T.bpar(d, gs, n, h, dm) == b_fmap(h, dm, T.hcat(T.BG, gs)) : List<&1, T.DB>}}
648
649# depth 0: the two leaves' loops, appended
650def b_m0c(-l: List<&1, T.BG>, -r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, -l1y: List<&1, T.BG>, +sl: {l1y == l : List<&1, T.BG>}, fl: {T.bleaf(l, h, dm, Nil{}) == b_fmap(h, dm, l) : List<&1, T.DB>}, r1: List<&1, T.BG>, sr: {r1 == r : List<&1, T.BG>}, fr: {T.bleaf(r, h, dm, Nil{}) == b_fmap(h, dm, r) : List<&1, T.DB>}, c: b_MAR<h, dm, l1y, r>) -> b_MR<0n, T.Halves{l, r}, n, h, dm>:
651  match c:
652    case b_MAR{l2, s2, fa}:
653      b_MR{List.append(&1, T.BG, l2, r1), app2(T.BG, l2, l, r1, r, Equal.trans(List<&1, T.BG>, l2, l1y, l, s2, sl), sr),
654        Equal.trans(List<&1, T.DB>, List.append(&1, T.DB, T.bleaf(l, h, dm, Nil{}), T.bleaf(r, h, dm, Nil{})), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), b_fmap(h, dm, List.append(&1, T.BG, l, r)), app2(T.DB, T.bleaf(l, h, dm, Nil{}), b_fmap(h, dm, l), T.bleaf(r, h, dm, Nil{}), b_fmap(h, dm, r), fl, fr),
655          Equal.sym(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, l, r)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)),
656            Equal.trans(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, l, r)), b_fmap(h, dm, List.append(&1, T.BG, l1y, r)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, List.append(&1, T.BG, z, r)), l, l1y, Equal.sym(List<&1, T.BG>, l1y, l, sl)),
657              Equal.trans(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, l1y, r)), List.append(&1, T.DB, b_fmap(h, dm, l1y), b_fmap(h, dm, r)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), fa, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => List.append(&1, T.DB, b_fmap(h, dm, z), b_fmap(h, dm, r)), l1y, l, sl)))))}
658
659def b_m0b(-l: List<&1, T.BG>, -r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, l1y: List<&1, T.BG>, +sl: {l1y == l : List<&1, T.BG>}, fl: {T.bleaf(l, h, dm, Nil{}) == b_fmap(h, dm, l) : List<&1, T.DB>}, b: b_L1R<h, dm, r, Nil{}>) -> b_MR<0n, T.Halves{l, r}, n, h, dm>:
660  match b:
661    case b_L1R{r1, sr, fr}:
662      b_m0c(l, r, n, h, dm, l1y, sl, fl, r1, sr, fr, b_map_app(l1y, h, dm, r))
663
664def b_m0a(-l: List<&1, T.BG>, r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, a: b_L1R<h, dm, l, Nil{}>) -> b_MR<0n, T.Halves{l, r}, n, h, dm>:
665  match a:
666    case b_L1R{l1y, sl, fl}:
667      b_m0b(l, r, n, h, dm, l1y, sl, fl, b_l1(r, h, dm, Nil{}))
668
669# depth 1 + e: each half cut in two and its b_tree (the closures run main at depth e), then the two maps appended
670def b_m1c(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.BG>, s1: {hh1 == T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.BG>}, +cat1: {T.hcat(T.BG, hh1) == l : List<&1, T.BG>}, -hh2: T.Halves<T.BG>, s2: {hh2 == T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.BG>}, +cat2: {T.hcat(T.BG, hh2) == r : List<&1, T.BG>}, -y1: List<&1, T.BG>, sy1: {y1 == T.hcat(T.BG, hh1) : List<&1, T.BG>}, f1: {T.bpar(e, hh1, TA.half(n), h, dm) == b_fmap(h, dm, T.hcat(T.BG, hh1)) : List<&1, T.DB>}, y2: List<&1, T.BG>, sy2: {y2 == T.hcat(T.BG, hh2) : List<&1, T.BG>}, f2: {T.bpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm) == b_fmap(h, dm, T.hcat(T.BG, hh2)) : List<&1, T.DB>}, ma: b_MAR<h, dm, y1, y2>) -> b_MR<1n+e, T.Halves{l, r}, n, h, dm>:
671  match ma:
672    case b_MAR{y1b, sb, fa}:
673      +ly1 = Equal.trans(List<&1, T.BG>, y1, T.hcat(T.BG, hh1), l, sy1, cat1)
674      +ly2 = Equal.trans(List<&1, T.BG>, y2, T.hcat(T.BG, hh2), r, sy2, cat2)
675      +q1 = Equal.trans(List<&1, T.DB>, T.bpar(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.bpar(e, hh1, TA.half(n), h, dm), b_fmap(h, dm, l), Equal.cong(T.Halves<T.BG>, List<&1, T.DB>, z => T.bpar(e, z, TA.half(n), h, dm), T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), hh1, Equal.sym(T.Halves<T.BG>, hh1, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), s1)), Equal.trans(List<&1, T.DB>, T.bpar(e, hh1, TA.half(n), h, dm), b_fmap(h, dm, T.hcat(T.BG, hh1)), b_fmap(h, dm, l), f1, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), T.hcat(T.BG, hh1), l, cat1)))
676      +q2 = Equal.trans(List<&1, T.DB>, T.bpar(e, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), T.bpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm), b_fmap(h, dm, r), Equal.cong(T.Halves<T.BG>, List<&1, T.DB>, z => T.bpar(e, z, Nat.sub(n, TA.half(n)), h, dm), T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), hh2, Equal.sym(T.Halves<T.BG>, hh2, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), s2)), Equal.trans(List<&1, T.DB>, T.bpar(e, hh2, Nat.sub(n, TA.half(n)), h, dm), b_fmap(h, dm, T.hcat(T.BG, hh2)), b_fmap(h, dm, r), f2, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), T.hcat(T.BG, hh2), r, cat2)))
677      +bb = Equal.trans(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, l, r)), b_fmap(h, dm, List.append(&1, T.BG, y1, y2)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), List.append(&1, T.BG, l, r), List.append(&1, T.BG, y1, y2), app2(T.BG, l, y1, r, y2, Equal.sym(List<&1, T.BG>, y1, l, ly1), Equal.sym(List<&1, T.BG>, y2, r, ly2))), Equal.trans(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, y1, y2)), List.append(&1, T.DB, b_fmap(h, dm, y1), b_fmap(h, dm, y2)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), fa, app2(T.DB, b_fmap(h, dm, y1), b_fmap(h, dm, l), b_fmap(h, dm, y2), b_fmap(h, dm, r), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), y1, l, ly1), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), y2, r, ly2))))
678      b_MR{List.append(&1, T.BG, y1b, y2), app2(T.BG, y1b, l, y2, r, Equal.trans(List<&1, T.BG>, y1b, y1, l, sb, ly1), ly2),
679        Equal.trans(List<&1, T.DB>, List.append(&1, T.DB, T.bpar(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.bpar(e, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), b_fmap(h, dm, List.append(&1, T.BG, l, r)), app2(T.DB, T.bpar(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), b_fmap(h, dm, l), T.bpar(e, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), b_fmap(h, dm, r), q1, q2), Equal.sym(List<&1, T.DB>, b_fmap(h, dm, List.append(&1, T.BG, l, r)), List.append(&1, T.DB, b_fmap(h, dm, l), b_fmap(h, dm, r)), bb))}
680
681def b_m1b(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.BG>, s1: {hh1 == T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.BG>}, cat1: {T.hcat(T.BG, hh1) == l : List<&1, T.BG>}, -hh2: T.Halves<T.BG>, s2: {hh2 == T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.BG>}, cat2: {T.hcat(T.BG, hh2) == r : List<&1, T.BG>}, r1: b_MR<e, hh1, TA.half(n), h, dm>, r2: b_MR<e, hh2, Nat.sub(n, TA.half(n)), h, dm>) -> b_MR<1n+e, T.Halves{l, r}, n, h, dm>:
682  match r1 r2:
683    case b_MR{y1, sy1, f1} b_MR{y2, sy2, f2}:
684      b_m1c(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, y1, sy1, f1, y2, sy2, f2, b_map_app(y1, h, dm, y2))
685
686def b_m1a(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, c1: b_CGR<TA.half(TA.half(n)), l, Nil{}>, c2: b_CGR<TA.half(Nat.sub(n, TA.half(n))), r, Nil{}>, k1: @g: T.Halves<T.BG> -> b_MR<e, g, TA.half(n), h, dm>, k2: @g: T.Halves<T.BG> -> b_MR<e, g, Nat.sub(n, TA.half(n)), h, dm>) -> b_MR<1n+e, T.Halves{l, r}, n, h, dm>:
687  match c1 c2:
688    case b_CGR{hh1, s1, cat1} b_CGR{hh2, s2, cat2}:
689      b_m1b(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, k1(hh1), k2(hh2))
690
691def b_tree(d: Nat, gs: T.Halves<T.BG>, +n: Nat, +h: Nat, +dm: T.Dm) -> b_MR<d, gs, n, h, dm>:
692  match d gs:
693    case 0n T.Halves{l, r}:
694      b_m0a(l, r, n, h, dm, b_l1(l, h, dm, Nil{}))
695    case 1n++e T.Halves{l, r}:
696      b_m1a(e, l, r, n, h, dm, b_cg(TA.half(TA.half(n)), l, Nil{}), b_cg(TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), g1 => b_tree(e, g1, TA.half(n), h, dm), g2 => b_tree(e, g2, Nat.sub(n, TA.half(n)), h, dm))
697
698# the law: the b_tree gives what fleaf, the loop over the sequences one after another, gives
699def b_par_fin(-d: Nat, -gs: T.Halves<T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, -ys: List<&1, T.BG>, +sy: {ys == T.hcat(T.BG, gs) : List<&1, T.BG>}, f: {T.bpar(d, gs, n, h, dm) == b_fmap(h, dm, T.hcat(T.BG, gs)) : List<&1, T.DB>}, r: b_L1R<h, dm, ys, Nil{}>) -> {T.bpar(d, gs, n, h, dm) == T.bleaf(T.hcat(T.BG, gs), h, dm, Nil{}) : List<&1, T.DB>}:
700  match r:
701    case b_L1R{ys2, s2, fl}:
702      Equal.trans(List<&1, T.DB>, T.bpar(d, gs, n, h, dm), b_fmap(h, dm, T.hcat(T.BG, gs)), T.bleaf(T.hcat(T.BG, gs), h, dm, Nil{}), f,
703        Equal.sym(List<&1, T.DB>, T.bleaf(T.hcat(T.BG, gs), h, dm, Nil{}), b_fmap(h, dm, T.hcat(T.BG, gs)),
704          Equal.trans(List<&1, T.DB>, T.bleaf(T.hcat(T.BG, gs), h, dm, Nil{}), T.bleaf(ys, h, dm, Nil{}), b_fmap(h, dm, T.hcat(T.BG, gs)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => T.bleaf(z, h, dm, Nil{}), T.hcat(T.BG, gs), ys, Equal.sym(List<&1, T.BG>, ys, T.hcat(T.BG, gs), sy)),
705            Equal.trans(List<&1, T.DB>, T.bleaf(ys, h, dm, Nil{}), b_fmap(h, dm, ys), b_fmap(h, dm, T.hcat(T.BG, gs)), fl, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_fmap(h, dm, z), ys, T.hcat(T.BG, gs), sy)))))
706
707def b_par_mid(-d: Nat, -gs: T.Halves<T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, r: b_MR<d, gs, n, h, dm>) -> {T.bpar(d, gs, n, h, dm) == T.bleaf(T.hcat(T.BG, gs), h, dm, Nil{}) : List<&1, T.DB>}:
708  match r:
709    case b_MR{ys, sy, f}:
710      b_par_fin(d, gs, n, h, dm, ys, sy, f, b_l1(ys, h, dm, Nil{}))
711
712def b_ffmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.BG>) -> List<&1, T.DB>:
713  match xs:
714    case Nil{}:
715      Nil{}
716    case Con{x, t}:
717      T.db_of(T.bgroups_full(h, 0n, dm, x)) <> b_ffmap(h, dm, t)
718
719# ---- fleaf (the code's loop with an accumulator) is the map pushed onto the accumulator ----
720
721type b_L1RF<-h: Nat, -dm: T.Dm, -xs: List<&1, T.BG>, -acc: List<&1, T.DB>> is Type:
722  b_L1RF{ys: List<&1, T.BG>, same: {ys == xs : List<&1, T.BG>}, fact: {T.bleaf_full(xs, h, dm, acc) == List.reverse.go(&1, T.DB, acc, b_ffmap(h, dm, xs)) : List<&1, T.DB>}}
723
724def b_lf_con(x: T.BG, -t: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>, r: b_L1RF<h, dm, t, T.db_of(T.bgroups_full(h, 0n, dm, x)) <> acc>) -> b_L1RF<h, dm, x <> t, acc>:
725  match r:
726    case b_L1RF{ys, same, fact}:
727      b_L1RF{x <> ys, Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => x <> z, ys, t, same), fact}
728
729def b_lf1(xs: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>) -> b_L1RF<h, dm, xs, acc>:
730  match xs:
731    case Nil{}:
732      b_L1RF{Nil{}, {==}, {==}}
733    case Con{x, t}:
734      b_lf_con(x, t, h, dm, acc, b_lf1(t, h, dm, T.db_of(T.bgroups_full(h, 0n, dm, x)) <> acc))
735
736# ---- the map of two lists appended is the two maps appended ----
737
738type b_MARF<-h: Nat, -dm: T.Dm, -a: List<&1, T.BG>, -b: List<&1, T.BG>> is Type:
739  b_MARF{ys: List<&1, T.BG>, same: {ys == a : List<&1, T.BG>}, fact: {b_ffmap(h, dm, List.append(&1, T.BG, a, b)) == List.append(&1, T.DB, b_ffmap(h, dm, a), b_ffmap(h, dm, b)) : List<&1, T.DB>}}
740
741def b_ma_conf(x: T.BG, -t: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>, r: b_MARF<h, dm, t, b>) -> b_MARF<h, dm, x <> t, b>:
742  match r:
743    case b_MARF{ys, same, fact}:
744      b_MARF{x <> ys, Equal.cong(List<&1, T.BG>, List<&1, T.BG>, z => x <> z, ys, t, same), Equal.cong(List<&1, T.DB>, List<&1, T.DB>, z => T.db_of(T.bgroups_full(h, 0n, dm, x)) <> z, b_ffmap(h, dm, List.append(&1, T.BG, t, b)), List.append(&1, T.DB, b_ffmap(h, dm, t), b_ffmap(h, dm, b)), fact)}
745
746def b_map_appf(a: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>) -> b_MARF<h, dm, a, b>:
747  match a:
748    case Nil{}:
749      b_MARF{Nil{}, {==}, {==}}
750    case Con{x, t}:
751      b_ma_conf(x, t, h, dm, b, b_map_appf(t, h, dm, b))
752
753# ---- a reversed onto b, then c appended: a reversed onto b ++ c ----
754
755type b_MRF<-d: Nat, -gs: T.Halves<T.BG>, -n: Nat, -h: Nat, -dm: T.Dm> is Type:
756  b_MRF{ys: List<&1, T.BG>, same: {ys == T.hcat(T.BG, gs) : List<&1, T.BG>}, fact: {T.bpar_full(d, gs, n, h, dm) == b_ffmap(h, dm, T.hcat(T.BG, gs)) : List<&1, T.DB>}}
757
758# depth 0: the two leaves' loops, appended
759def b_fm0c(-l: List<&1, T.BG>, -r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, -l1y: List<&1, T.BG>, +sl: {l1y == l : List<&1, T.BG>}, fl: {T.bleaf_full(l, h, dm, Nil{}) == b_ffmap(h, dm, l) : List<&1, T.DB>}, r1: List<&1, T.BG>, sr: {r1 == r : List<&1, T.BG>}, fr: {T.bleaf_full(r, h, dm, Nil{}) == b_ffmap(h, dm, r) : List<&1, T.DB>}, c: b_MARF<h, dm, l1y, r>) -> b_MRF<0n, T.Halves{l, r}, n, h, dm>:
760  match c:
761    case b_MARF{l2, s2, fa}:
762      b_MRF{List.append(&1, T.BG, l2, r1), app2(T.BG, l2, l, r1, r, Equal.trans(List<&1, T.BG>, l2, l1y, l, s2, sl), sr),
763        Equal.trans(List<&1, T.DB>, List.append(&1, T.DB, T.bleaf_full(l, h, dm, Nil{}), T.bleaf_full(r, h, dm, Nil{})), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), b_ffmap(h, dm, List.append(&1, T.BG, l, r)), app2(T.DB, T.bleaf_full(l, h, dm, Nil{}), b_ffmap(h, dm, l), T.bleaf_full(r, h, dm, Nil{}), b_ffmap(h, dm, r), fl, fr),
764          Equal.sym(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l, r)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)),
765            Equal.trans(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l, r)), b_ffmap(h, dm, List.append(&1, T.BG, l1y, r)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, List.append(&1, T.BG, z, r)), l, l1y, Equal.sym(List<&1, T.BG>, l1y, l, sl)),
766              Equal.trans(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l1y, r)), List.append(&1, T.DB, b_ffmap(h, dm, l1y), b_ffmap(h, dm, r)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), fa, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => List.append(&1, T.DB, b_ffmap(h, dm, z), b_ffmap(h, dm, r)), l1y, l, sl)))))}
767
768def b_fm0b(-l: List<&1, T.BG>, -r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, l1y: List<&1, T.BG>, +sl: {l1y == l : List<&1, T.BG>}, fl: {T.bleaf_full(l, h, dm, Nil{}) == b_ffmap(h, dm, l) : List<&1, T.DB>}, b: b_L1RF<h, dm, r, Nil{}>) -> b_MRF<0n, T.Halves{l, r}, n, h, dm>:
769  match b:
770    case b_L1RF{r1, sr, fr}:
771      b_fm0c(l, r, n, h, dm, l1y, sl, fl, r1, sr, fr, b_map_appf(l1y, h, dm, r))
772
773def b_fm0a(-l: List<&1, T.BG>, r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, a: b_L1RF<h, dm, l, Nil{}>) -> b_MRF<0n, T.Halves{l, r}, n, h, dm>:
774  match a:
775    case b_L1RF{l1y, sl, fl}:
776      b_fm0b(l, r, n, h, dm, l1y, sl, fl, b_lf1(r, h, dm, Nil{}))
777
778# depth 1 + e: each half cut in two and its b_treef (the closures run main at depth e), then the two maps appended
779def b_fm1c(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.BG>, s1: {hh1 == T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.BG>}, +cat1: {T.hcat(T.BG, hh1) == l : List<&1, T.BG>}, -hh2: T.Halves<T.BG>, s2: {hh2 == T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.BG>}, +cat2: {T.hcat(T.BG, hh2) == r : List<&1, T.BG>}, -y1: List<&1, T.BG>, sy1: {y1 == T.hcat(T.BG, hh1) : List<&1, T.BG>}, f1: {T.bpar_full(e, hh1, TA.half(n), h, dm) == b_ffmap(h, dm, T.hcat(T.BG, hh1)) : List<&1, T.DB>}, y2: List<&1, T.BG>, sy2: {y2 == T.hcat(T.BG, hh2) : List<&1, T.BG>}, f2: {T.bpar_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm) == b_ffmap(h, dm, T.hcat(T.BG, hh2)) : List<&1, T.DB>}, ma: b_MARF<h, dm, y1, y2>) -> b_MRF<1n+e, T.Halves{l, r}, n, h, dm>:
780  match ma:
781    case b_MARF{y1b, sb, fa}:
782      +ly1 = Equal.trans(List<&1, T.BG>, y1, T.hcat(T.BG, hh1), l, sy1, cat1)
783      +ly2 = Equal.trans(List<&1, T.BG>, y2, T.hcat(T.BG, hh2), r, sy2, cat2)
784      +q1 = Equal.trans(List<&1, T.DB>, T.bpar_full(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.bpar_full(e, hh1, TA.half(n), h, dm), b_ffmap(h, dm, l), Equal.cong(T.Halves<T.BG>, List<&1, T.DB>, z => T.bpar_full(e, z, TA.half(n), h, dm), T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), hh1, Equal.sym(T.Halves<T.BG>, hh1, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), s1)), Equal.trans(List<&1, T.DB>, T.bpar_full(e, hh1, TA.half(n), h, dm), b_ffmap(h, dm, T.hcat(T.BG, hh1)), b_ffmap(h, dm, l), f1, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, z), T.hcat(T.BG, hh1), l, cat1)))
785      +q2 = Equal.trans(List<&1, T.DB>, T.bpar_full(e, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), T.bpar_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm), b_ffmap(h, dm, r), Equal.cong(T.Halves<T.BG>, List<&1, T.DB>, z => T.bpar_full(e, z, Nat.sub(n, TA.half(n)), h, dm), T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), hh2, Equal.sym(T.Halves<T.BG>, hh2, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), s2)), Equal.trans(List<&1, T.DB>, T.bpar_full(e, hh2, Nat.sub(n, TA.half(n)), h, dm), b_ffmap(h, dm, T.hcat(T.BG, hh2)), b_ffmap(h, dm, r), f2, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, z), T.hcat(T.BG, hh2), r, cat2)))
786      +bb = Equal.trans(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l, r)), b_ffmap(h, dm, List.append(&1, T.BG, y1, y2)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, z), List.append(&1, T.BG, l, r), List.append(&1, T.BG, y1, y2), app2(T.BG, l, y1, r, y2, Equal.sym(List<&1, T.BG>, y1, l, ly1), Equal.sym(List<&1, T.BG>, y2, r, ly2))), Equal.trans(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, y1, y2)), List.append(&1, T.DB, b_ffmap(h, dm, y1), b_ffmap(h, dm, y2)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), fa, app2(T.DB, b_ffmap(h, dm, y1), b_ffmap(h, dm, l), b_ffmap(h, dm, y2), b_ffmap(h, dm, r), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, z), y1, l, ly1), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, z), y2, r, ly2))))
787      b_MRF{List.append(&1, T.BG, y1b, y2), app2(T.BG, y1b, l, y2, r, Equal.trans(List<&1, T.BG>, y1b, y1, l, sb, ly1), ly2),
788        Equal.trans(List<&1, T.DB>, List.append(&1, T.DB, T.bpar_full(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), T.bpar_full(e, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), b_ffmap(h, dm, List.append(&1, T.BG, l, r)), app2(T.DB, T.bpar_full(e, T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}), TA.half(n), h, dm), b_ffmap(h, dm, l), T.bpar_full(e, T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), Nat.sub(n, TA.half(n)), h, dm), b_ffmap(h, dm, r), q1, q2), Equal.sym(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l, r)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), bb))}
789
790def b_fm1b(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves<T.BG>, s1: {hh1 == T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}) : T.Halves<T.BG>}, cat1: {T.hcat(T.BG, hh1) == l : List<&1, T.BG>}, -hh2: T.Halves<T.BG>, s2: {hh2 == T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves<T.BG>}, cat2: {T.hcat(T.BG, hh2) == r : List<&1, T.BG>}, r1: b_MRF<e, hh1, TA.half(n), h, dm>, r2: b_MRF<e, hh2, Nat.sub(n, TA.half(n)), h, dm>) -> b_MRF<1n+e, T.Halves{l, r}, n, h, dm>:
791  match r1 r2:
792    case b_MRF{y1, sy1, f1} b_MRF{y2, sy2, f2}:
793      b_fm1c(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, y1, sy1, f1, y2, sy2, f2, b_map_appf(y1, h, dm, y2))
794
795def b_fm1a(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, c1: b_CGR<TA.half(TA.half(n)), l, Nil{}>, c2: b_CGR<TA.half(Nat.sub(n, TA.half(n))), r, Nil{}>, k1: @g: T.Halves<T.BG> -> b_MRF<e, g, TA.half(n), h, dm>, k2: @g: T.Halves<T.BG> -> b_MRF<e, g, Nat.sub(n, TA.half(n)), h, dm>) -> b_MRF<1n+e, T.Halves{l, r}, n, h, dm>:
796  match c1 c2:
797    case b_CGR{hh1, s1, cat1} b_CGR{hh2, s2, cat2}:
798      b_fm1b(e, l, r, n, h, dm, hh1, s1, cat1, hh2, s2, cat2, k1(hh1), k2(hh2))
799
800def b_treef(d: Nat, gs: T.Halves<T.BG>, +n: Nat, +h: Nat, +dm: T.Dm) -> b_MRF<d, gs, n, h, dm>:
801  match d gs:
802    case 0n T.Halves{l, r}:
803      b_fm0a(l, r, n, h, dm, b_lf1(l, h, dm, Nil{}))
804    case 1n++e T.Halves{l, r}:
805      b_fm1a(e, l, r, n, h, dm, b_cg(TA.half(TA.half(n)), l, Nil{}), b_cg(TA.half(Nat.sub(n, TA.half(n))), r, Nil{}), g1 => b_treef(e, g1, TA.half(n), h, dm), g2 => b_treef(e, g2, Nat.sub(n, TA.half(n)), h, dm))
806
807# the law: the b_treef gives what fleaf, the loop over the sequences one after another, gives
808def b_par_fin_f(-d: Nat, -gs: T.Halves<T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, -ys: List<&1, T.BG>, +sy: {ys == T.hcat(T.BG, gs) : List<&1, T.BG>}, f: {T.bpar_full(d, gs, n, h, dm) == b_ffmap(h, dm, T.hcat(T.BG, gs)) : List<&1, T.DB>}, r: b_L1RF<h, dm, ys, Nil{}>) -> {T.bpar_full(d, gs, n, h, dm) == T.bleaf_full(T.hcat(T.BG, gs), h, dm, Nil{}) : List<&1, T.DB>}:
809  match r:
810    case b_L1RF{ys2, s2, fl}:
811      Equal.trans(List<&1, T.DB>, T.bpar_full(d, gs, n, h, dm), b_ffmap(h, dm, T.hcat(T.BG, gs)), T.bleaf_full(T.hcat(T.BG, gs), h, dm, Nil{}), f,
812        Equal.sym(List<&1, T.DB>, T.bleaf_full(T.hcat(T.BG, gs), h, dm, Nil{}), b_ffmap(h, dm, T.hcat(T.BG, gs)),
813          Equal.trans(List<&1, T.DB>, T.bleaf_full(T.hcat(T.BG, gs), h, dm, Nil{}), T.bleaf_full(ys, h, dm, Nil{}), b_ffmap(h, dm, T.hcat(T.BG, gs)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => T.bleaf_full(z, h, dm, Nil{}), T.hcat(T.BG, gs), ys, Equal.sym(List<&1, T.BG>, ys, T.hcat(T.BG, gs), sy)),
814            Equal.trans(List<&1, T.DB>, T.bleaf_full(ys, h, dm, Nil{}), b_ffmap(h, dm, ys), b_ffmap(h, dm, T.hcat(T.BG, gs)), fl, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, z), ys, T.hcat(T.BG, gs), sy)))))
815
816def b_par_mid_f(-d: Nat, -gs: T.Halves<T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, r: b_MRF<d, gs, n, h, dm>) -> {T.bpar_full(d, gs, n, h, dm) == T.bleaf_full(T.hcat(T.BG, gs), h, dm, Nil{}) : List<&1, T.DB>}:
817  match r:
818    case b_MRF{ys, sy, f}:
819      b_par_fin_f(d, gs, n, h, dm, ys, sy, f, b_lf1(ys, h, dm, Nil{}))
820
821# PROOF (attn_par_bwd_full): attn_par_bwd's proof for the full-visible leaf; b_cg (cut and hcat, no leaf) is shared.
822def Laws.attn_par_bwd_full(d, gs, n, h, dm):
823  b_par_mid_f(d, gs, n, h, dm, b_treef(d, gs, n, h, dm))
824
825# PROOF (attn_par_bwd): attn_par_fwd's proof, for BG and bleaf.
826def Laws.attn_par_bwd(d, gs, n, h, dm):
827  b_par_mid(d, gs, n, h, dm, b_tree(d, gs, n, h, dm))
828
829# =====================================================================================================
830# Grouped-query heads (llama.bend's proof)
831# =====================================================================================================
832
833# one block of 1 + m numbers adds 1 to the quotient (Nat.divmod.go counts down the remainder from m)
834def div_block(+m: Nat, -n: Nat, -d: Nat, -r: Nat) -> {Nat.divmod.go(Nat.add(1n+m, n), m, d, r) == Nat.divmod.go(n, Nat.add(m, r), 1n+d, 0n) : Nat & Nat}:
835  match m:
836    case 0n:
837      {==}
838    case 1n+p:
839      %Equal.sym(Nat, 1n+Nat.add(p, r), Nat.add(p, 1n+r), NL.add_succ(p, r)) : {Nat.divmod.go(Nat.add(1n+p, n), p, d, 1n+r) == Nat.divmod.go(n, _, 1n+d, 0n) : Nat & Nat}
840      div_block(p, n, d, 1n+r)
841
842# j whole blocks of 1 + s numbers add j to the quotient
843def div_blocks(+j: Nat, +s: Nat, +n: Nat, +d: Nat) -> {Nat.divmod.go(Nat.add(Nat.mul(j, 1n+s), n), s, d, 0n) == Nat.divmod.go(n, s, Nat.add(j, d), 0n) : Nat & Nat}:
844  match j:
845    case 0n:
846      {==}
847    case 1n+jp:
848      %NL.add_assoc(1n+s, Nat.mul(jp, 1n+s), n) : {Nat.divmod.go(_, s, d, 0n) == Nat.divmod.go(n, s, Nat.add(1n+jp, d), 0n) : Nat & Nat}
849      %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(1n+s, Nat.add(Nat.mul(jp, 1n+s), n)), s, d, 0n), Nat.divmod.go(Nat.add(Nat.mul(jp, 1n+s), n), Nat.add(s, 0n), 1n+d, 0n), div_block(s, Nat.add(Nat.mul(jp, 1n+s), n), d, 0n)) : {_ == Nat.divmod.go(n, s, Nat.add(1n+jp, d), 0n) : Nat & Nat}
850      %Equal.sym(Nat, Nat.add(s, 0n), s, NL.add_zero(s)) : {Nat.divmod.go(Nat.add(Nat.mul(jp, 1n+s), n), _, 1n+d, 0n) == Nat.divmod.go(n, s, Nat.add(1n+jp, d), 0n) : Nat & Nat}
851      %Equal.sym(Nat, 1n+Nat.add(jp, d), Nat.add(jp, 1n+d), NL.add_succ(jp, d)) : {Nat.divmod.go(Nat.add(Nat.mul(jp, 1n+s), n), s, 1n+d, 0n) == Nat.divmod.go(n, s, _, 0n) : Nat & Nat}
852      div_blocks(jp, s, n, 1n+d)
853
854# fewer than 1 + s numbers after the last whole block leave the quotient alone
855def div_rest(+i: Nat, -k: Nat, -d: Nat, -r: Nat) -> {Pair.fst(Nat, Nat, Nat.divmod.go(i, Nat.add(i, k), d, r)) == d : Nat}:
856  match i:
857    case 0n:
858      {==}
859    case 1n+p:
860      div_rest(p, k, d, 1n+r)
861
862# PROOF (gqa_head): Nat.div counts how many whole blocks of g numbers fit. j·g is j whole blocks (div_blocks), and
863# i < g numbers after them do not complete another one (div_rest).
864def Laws.gqa_head(j, i, k):
865  %Equal.sym(Nat & Nat, Nat.divmod.go(Nat.add(Nat.mul(j, 1n+Nat.add(i, k)), i), Nat.add(i, k), 0n, 0n), Nat.divmod.go(i, Nat.add(i, k), Nat.add(j, 0n), 0n), div_blocks(j, Nat.add(i, k), i, 0n)) : {Pair.fst(Nat, Nat, _) == j : Nat}
866  %NL.add_zero(j) : {Pair.fst(Nat, Nat, Nat.divmod.go(i, Nat.add(i, k), Nat.add(j, 0n), 0n)) == _ : Nat}
867  div_rest(i, k, Nat.add(j, 0n), 0n)
868
869# PROOF (kv_of_group): kv_of is Nat.div, so this is gqa_head.
870def Laws.kv_of_group(j, i, k):
871  Laws.gqa_head(j, i, k)
872
873# PROOF (kv_cols): head_cols' key column is kv_of(head, g)·hd; kv_of of a head of group j is j (kv_of_group).
874def Laws.kv_cols(t, hd, w, kvw, sc, j, i, k):
875  Equal.cong(Nat, U32, n => U32.from_nat(Nat.mul(n, hd)), T.kv_of(Nat.add(Nat.mul(j, 1n+Nat.add(i, k)), i), 1n+Nat.add(i, k)), j, Laws.kv_of_group(j, i, k))
876
877# =====================================================================================================
878# Tensors: shapes
879# =====================================================================================================
880
881# a || b == b || a, and a && b == b && a: every case computes
882def or_comm(+a: Bool, +b: Bool) -> {Bool.or(a, b) == Bool.or(b, a) : Bool}:
883  match a b:
884    case True{} True{}:
885      {==}
886    case True{} False{}:
887      {==}
888    case False{} True{}:
889      {==}
890    case False{} False{}:
891      {==}
892
893def and_comm(+a: Bool, +b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}:
894  match a b:
895    case True{} True{}:
896      {==}
897    case True{} False{}:
898      {==}
899    case False{} True{}:
900      {==}
901    case False{} False{}:
902      {==}
903
904# equal operands give equal conjunctions and disjunctions
905def and_cong(+p: Bool, +p2: Bool, +q: Bool, +q2: Bool, e: {p == p2 : Bool}, f: {q == q2 : Bool}) -> {Bool.and(p, q) == Bool.and(p2, q2) : Bool}:
906  Equal.trans(Bool, Bool.and(p, q), Bool.and(p2, q), Bool.and(p2, q2), Equal.cong(Bool, Bool, x => Bool.and(x, q), p, p2, e), Equal.cong(Bool, Bool, x => Bool.and(p2, x), q, q2, f))
907
908def or_cong(+p: Bool, +p2: Bool, +q: Bool, +q2: Bool, e: {p == p2 : Bool}, f: {q == q2 : Bool}) -> {Bool.or(p, q) == Bool.or(p2, q2) : Bool}:
909  Equal.trans(Bool, Bool.or(p, q), Bool.or(p2, q), Bool.or(p2, q2), Equal.cong(Bool, Bool, x => Bool.or(x, q), p, p2, e), Equal.cong(Bool, Bool, x => Bool.or(p2, x), q, q2, f))
910
911# one axis: bc_dim is written as pair(x, y) || pair(y, x), so swapping x and y only swaps the two sides of the ||
912def bc_dim_sym(+x: Nat, +y: Nat, +z: Nat) -> {TT.bc_dim(x, y, z) == TT.bc_dim(y, x, z) : Bool}:
913  or_comm(TT.bc_pair(x, y, z), TT.bc_pair(y, x, z))
914
915# axis by axis: the same on each axis (bc_dim_sym), and by induction on the rest; shapes of different ranks are False
916# either way round
917def 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}:
918  match a b o:
919    case Nil{} Nil{} Nil{}:
920      {==}
921    case Nil{} Nil{} Con{z, ro}:
922      {==}
923    case Nil{} Con{y, rb} Nil{}:
924      {==}
925    case Nil{} Con{y, rb} Con{z, ro}:
926      {==}
927    case Con{x, ra} Nil{} Nil{}:
928      {==}
929    case Con{x, ra} Nil{} Con{z, ro}:
930      {==}
931    case Con{x, ra} Con{y, rb} Nil{}:
932      {==}
933    case Con{+x, +ra} Con{+y, +rb} Con{+z, +ro}:
934      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))
935
936# the ranks: the same two comparisons and the same two equalities, in the other order
937def bc_rank_sym(+la: Nat, +lb: Nat, +lo: Nat) -> {TT.bc_rank(la, lb, lo) == TT.bc_rank(lb, la, lo) : Bool}:
938  and_cong(Bool.and(Nat.is_le(la, lo), Nat.is_le(lb, lo)), Bool.and(Nat.is_le(lb, lo), Nat.is_le(la, lo)), Bool.or(Nat.is_eq(la, lo), Nat.is_eq(lb, lo)), Bool.or(Nat.is_eq(lb, lo), Nat.is_eq(la, lo)),
939    and_comm(Nat.is_le(la, lo), Nat.is_le(lb, lo)), or_comm(Nat.is_eq(la, lo), Nat.is_eq(lb, lo)))
940
941def Laws.bc_sym(a, b, o):
942  and_cong(TT.bc_rank(List.length(&2, Nat, a), List.length(&2, Nat, b), List.length(&2, Nat, o)), TT.bc_rank(List.length(&2, Nat, b), List.length(&2, Nat, a), List.length(&2, Nat, o)),
943    TT.bc_eq(TT.pad(a, List.length(&2, Nat, o)), TT.pad(b, List.length(&2, Nat, o)), o), TT.bc_eq(TT.pad(b, List.length(&2, Nat, o)), TT.pad(a, List.length(&2, Nat, o)), o),
944    bc_rank_sym(List.length(&2, Nat, a), List.length(&2, Nat, b), List.length(&2, Nat, o)), bc_eq_sym(TT.pad(a, List.length(&2, Nat, o)), TT.pad(b, List.length(&2, Nat, o)), o))
945
946# h * (a * r) == a * (h * r): associativity, then commutativity of the first two factors, then associativity back
947def mul_swap(+h: Nat, +a: Nat, +r: Nat) -> {Nat.mul(h, Nat.mul(a, r)) == Nat.mul(a, Nat.mul(h, r)) : Nat}:
948  Equal.trans(Nat, Nat.mul(h, Nat.mul(a, r)), Nat.mul(Nat.mul(h, a), r), Nat.mul(a, Nat.mul(h, r)), NL.mul_assoc(h, a, r),
949    Equal.trans(Nat, Nat.mul(Nat.mul(h, a), r), Nat.mul(Nat.mul(a, h), r), Nat.mul(a, Nat.mul(h, r)),
950      Equal.cong(Nat, Nat, x => Nat.mul(x, r), Nat.mul(h, a), Nat.mul(a, h), NL.mul_comm(h, a)),
951      Equal.sym(Nat, Nat.mul(a, Nat.mul(h, r)), Nat.mul(Nat.mul(a, h), r), NL.mul_assoc(a, h, r))))
952
953# by induction on the shape and the axis: axis 0 computes; past it, the first size h stays in front on both sides, and
954# mul_swap moves it past size(k)
955def Laws.sum_numel(s, k):
956  match s k:
957    case Nil{} _:
958      {==}
959    case Con{h, t} 0n:
960      {==}
961    case Con{+h, +t} 1n+p:
962      Equal.trans(Nat, Nat.mul(h, NL.product(t)), Nat.mul(h, Nat.mul(TT.at1(t, p), NL.product(TT.remove(t, p)))), Nat.mul(TT.at1(t, p), Nat.mul(h, NL.product(TT.remove(t, p)))),
963        Equal.cong(Nat, Nat, x => Nat.mul(h, x), NL.product(t), Nat.mul(TT.at1(t, p), NL.product(TT.remove(t, p))), Laws.sum_numel(t, p)),
964        mul_swap(h, TT.at1(t, p), NL.product(TT.remove(t, p))))
965
966# =====================================================================================================
967# Tensors: narrow, cat, of_mat, permute
968# =====================================================================================================
969
970# by induction: axis 0 is replaced and then taken out; past it, the first size stays in front on both sides
971def Laws.narrow_rest(s, d, l):
972  match s d:
973    case Nil{} _:
974      {==}
975    case Con{h, t} 0n:
976      {==}
977    case Con{+h, +t} 1n+p:
978      # bend-lint: disable-next bend-lint-rules/performance/unused_result -- the binder of Equal.cong's motive, used in its body not-expected-because: a law, never run
979      Equal.cong(List<&2, Nat>, List<&2, Nat>, x => h <> x, TT.remove(TT.setd(t, p, l), p), TT.remove(t, p), Laws.narrow_rest(t, p, l))
980
981# a shape with no axis d contradicts the premise (d < rank is False); axis 0 is l; past it, the induction
982def Laws.narrow_axis(s, d, l, e):
983  match s d:
984    case Nil{} 0n:
985      Empty.absurd({TT.at1(TT.setd([], 0n, l), 0n) == l : Nat}, false_true(Equal.sym(Bool, True{}, False{}, e)))
986    case Nil{} 1n+p:
987      Empty.absurd({TT.at1(TT.setd([], 1n+p, l), 1n+p) == l : Nat}, false_true(Equal.sym(Bool, True{}, False{}, e)))
988    case Con{h, t} 0n:
989      {==}
990    case Con{h, +t} 1n+p:
991      Laws.narrow_axis(t, p, l, e)
992
993# axis 0: (x + y)·n == x·n + y·n (distributivity); past it, the induction and k·(a + b) == k·a + k·b
994def Laws.cat_numel(s, d, x, y, e):
995  match s d:
996    case Nil{} 0n:
997      Empty.absurd({TT.numel(TT.setd([], 0n, Nat.add(x, y))) == Nat.add(TT.numel(TT.setd([], 0n, x)), TT.numel(TT.setd([], 0n, y))) : Nat}, false_true(Equal.sym(Bool, True{}, False{}, e)))
998    case Nil{} 1n+p:
999      Empty.absurd({TT.numel(TT.setd([], 1n+p, Nat.add(x, y))) == Nat.add(TT.numel(TT.setd([], 1n+p, x)), TT.numel(TT.setd([], 1n+p, y))) : Nat}, false_true(Equal.sym(Bool, True{}, False{}, e)))
1000    case Con{h, +t} 0n:
1001      Equal.sym(Nat, Nat.add(Nat.mul(x, NL.product(t)), Nat.mul(y, NL.product(t))), Nat.mul(Nat.add(x, y), NL.product(t)), NL.mul_dist(x, y, NL.product(t)))
1002    case Con{+h, +t} 1n+p:
1003      Equal.trans(Nat, Nat.mul(h, NL.product(TT.setd(t, p, Nat.add(x, y)))), Nat.mul(h, Nat.add(NL.product(TT.setd(t, p, x)), NL.product(TT.setd(t, p, y)))), Nat.add(Nat.mul(h, NL.product(TT.setd(t, p, x))), Nat.mul(h, NL.product(TT.setd(t, p, y)))),
1004        Equal.cong(Nat, Nat, v => Nat.mul(h, v), NL.product(TT.setd(t, p, Nat.add(x, y))), Nat.add(NL.product(TT.setd(t, p, x)), NL.product(TT.setd(t, p, y))), Laws.cat_numel(t, p, x, y, e)),
1005        NL.mul_dist_l(h, NL.product(TT.setd(t, p, x)), NL.product(TT.setd(t, p, y))))
1006
1007# r·(c·1) == r·c: c·1 == c
1008def Laws.mat_numel(r, c):
1009  Equal.cong(Nat, Nat, v => Nat.mul(r, v), Nat.mul(c, 1n), c, NL.mul_one_r(c))
1010
1011# one axis of the result per entry of p
1012def Laws.permute_rank(s, p):
1013  match p:
1014    case Nil{}:
1015      {==}
1016    case Con{k, r}:
1017      Equal.cong(Nat, Nat, v => 1n+v, TT.rank(TT.permuted(s, r)), List.length(&2, Nat, r), Laws.permute_rank(s, r))
1018
1019# =====================================================================================================
1020# The order of a row's additions (block_sum)
1021# =====================================================================================================
1022
1023# one pass over 2k blocks of 2^p cells gives the k blocks of 2^(p+1) cells: the pass adds blocks 2j and 2j+1, the two
1024# halves bal puts under one node. Induction on k; add_succ turns k + (k + 1) into 2 + (k + k), and add_assoc moves the
1025# next pair's start from (lo + 2^p) + 2^p to lo + 2^(p+1)
1026def pass_pair(+p: Nat, +k: Nat, +lo: Nat) -> {Spec.spass(Spec.blocks(p, Nat.add(k, k), lo)) == Spec.blocks(1n+p, k, lo) : List<&2, Spec.Sum>}:
1027  match k:
1028    case 0n:
1029      {==}
1030    case 1n+j:
1031      +a = Spec.pw(p)
1032      +nx = Nat.add(Nat.add(lo, a), a)
1033      %NL.add_succ(j, j) : {Spec.spass(Spec.blocks(p, 1n+_, lo)) == Spec.blocks(1n+p, 1n+j, lo) : List<&2, Spec.Sum>}
1034      %Equal.sym(Nat, Nat.add(lo, Nat.add(a, a)), nx, NL.add_assoc(lo, a, a)) : {Spec.spass(Spec.blocks(p, 1n+1n+Nat.add(j, j), lo)) == Spec.SAdd{Spec.bal(p, lo), Spec.bal(p, Nat.add(lo, a))} <> Spec.blocks(1n+p, j, _) : List<&2, Spec.Sum>}
1035      %pass_pair(p, j, nx) : {Spec.spass(Spec.blocks(p, 1n+1n+Nat.add(j, j), lo)) == Spec.SAdd{Spec.bal(p, lo), Spec.bal(p, Nat.add(lo, a))} <> _ : List<&2, Spec.Sum>}
1036      {==}
1037
1038# 2^(p+1) · k cells are 2^p · 2k: (a + a)·k == a·k + a·k == a·(k + k)
1039def cnt2(+p: Nat, +k: Nat) -> {Nat.mul(Spec.pw(1n+p), k) == Nat.mul(Spec.pw(p), Nat.add(k, k)) : Nat}:
1040  +a = Spec.pw(p)
1041  Equal.trans(Nat, Nat.mul(Nat.add(a, a), k), Nat.add(Nat.mul(a, k), Nat.mul(a, k)), Nat.mul(a, Nat.add(k, k)),
1042    Equal.sym(Nat, Nat.add(Nat.mul(a, k), Nat.mul(a, k)), Nat.mul(Nat.add(a, a), k), NL.mul_dist(a, a, k)),
1043    Equal.sym(Nat, Nat.mul(a, Nat.add(k, k)), Nat.add(Nat.mul(a, k), Nat.mul(a, k)), NL.mul_dist_l(a, k, k)))
1044
1045# the first p passes over a row of 2^p · k cells leave its k blocks, each summed as bal sums it. Induction on p: p
1046# passes over 2^(p+1)·k cells (= 2^p·2k, cnt2) leave 2k blocks of 2^p, and one more pass pairs them (pass_pair)
1047def blocks_passes(+p: Nat, +k: Nat, +lo: Nat) -> {Spec.passes(p, Spec.blocks(0n, Nat.mul(Spec.pw(p), k), lo)) == Spec.blocks(p, k, lo) : List<&2, Spec.Sum>}:
1048  match p:
1049    case 0n:
1050      %NL.mul_one_l(k) : {Spec.blocks(0n, Nat.mul(1n, k), lo) == Spec.blocks(0n, _, lo) : List<&2, Spec.Sum>}
1051      {==}
1052    case 1n+q:
1053      +kk = Nat.add(k, k)
1054      %Equal.sym(Nat, Nat.mul(Spec.pw(1n+q), k), Nat.mul(Spec.pw(q), kk), cnt2(q, k)) : {Spec.spass(Spec.passes(q, Spec.blocks(0n, _, lo))) == Spec.blocks(1n+q, k, lo) : List<&2, Spec.Sum>}
1055      %Equal.sym(List<&2, Spec.Sum>, Spec.passes(q, Spec.blocks(0n, Nat.mul(Spec.pw(q), kk), lo)), Spec.blocks(q, kk, lo), blocks_passes(q, kk, lo)) : {Spec.spass(_) == Spec.blocks(1n+q, k, lo) : List<&2, Spec.Sum>}
1056      pass_pair(q, k, lo)
1057
1058# r + p passes are p passes, then r more
1059def passes_add(r: Nat, +p: Nat, +xs: List<&2, Spec.Sum>) -> {Spec.passes(Nat.add(r, p), xs) == Spec.passes(r, Spec.passes(p, xs)) : List<&2, Spec.Sum>}:
1060  match r:
1061    case 0n:
1062      {==}
1063    case 1n+q:
1064      # bend-lint: disable-next bend-lint-rules/performance/unused_result -- the binder of Equal.cong's motive, used in its body not-expected-because: a law, never run
1065      Equal.cong(List<&2, Spec.Sum>, List<&2, Spec.Sum>, z => Spec.spass(z), Spec.passes(Nat.add(q, p), xs), Spec.passes(q, Spec.passes(p, xs)), passes_add(q, p, xs))
1066
1067# block_sum: r + p passes over the row are r passes over what its first p passes leave (passes_add), which is its k
1068# blocks summed as bal sums them (blocks_passes)
1069def Laws.block_sum(p, k, r):
1070  +row = Spec.blocks(0n, Nat.mul(Spec.pw(p), k), 0n)
1071  Equal.trans(List<&2, Spec.Sum>, Spec.passes(Nat.add(r, p), row), Spec.passes(r, Spec.passes(p, row)), Spec.passes(r, Spec.blocks(p, k, 0n)),
1072    passes_add(r, p, row),
1073    Equal.cong(List<&2, Spec.Sum>, List<&2, Spec.Sum>, z => Spec.passes(r, z), Spec.passes(p, row), Spec.blocks(p, k, 0n), blocks_passes(p, k, 0n)))
1074
1075def main() -> Unit:
1076  Unit{}