bendtorch

Releases (6):
  1.3.0.0  0x36ea31ed290fa4b30d529f2a3ef7c48f  indexed  https://jend.leeeet.dev/files.txt?path=bendtorch@1.3.0.0
  1.2.0.0  0xea477ac4399d6f3f46b9d25d99c1900c  unindexed  https://jend.leeeet.dev/files.txt?path=bendtorch@1.2.0.0
  1.1.1.0  0xe1214263ebd97956a02f4f3ea7544c84  unindexed  https://jend.leeeet.dev/files.txt?path=bendtorch@1.1.1.0
  1.1.0.0  0x88d35bdf07184f57aa5174c6f06ab791  unindexed  https://jend.leeeet.dev/files.txt?path=bendtorch@1.1.0.0
  1.0.1.0  0xfc8448b10655d3efdb72c022131382f2  unindexed  https://jend.leeeet.dev/files.txt?path=bendtorch@1.0.1.0
  1.0.0.0  0x1ca1def0868294e0aed9920bf123e68a  unindexed  https://jend.leeeet.dev/files.txt?path=bendtorch@1.0.0.0

Definitions (1049, 1 to 100 shown):
  LAWS.adjoint (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=adjoint)
   # LAW (adjoint): the backward pass of a linear layer, dx = Wᵀ·dy, is the adjoint of its forward pass y = W·x: for any
   # W, dy and x, dy·(W·x) == (Wᵀ·dy)·x. This is what makes dx the gradient of the loss with respect to x.
   law adjoint:
     for w: List<&2, List<&2, Nat>>
     for g: List<&2, Nat>
     for +v: List<&2, Nat>
     {Spec.dotn(g, Spec.mv(w, v)) == Spec.dotn(Spec.mtv(w, g), v) : Nat}
  LAWS.weight_adjoint (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=weight_adjoint)
   # LAW (weight_adjoint): the weight gradient dW = dy ⊗ x is the adjoint in W: dy·(W·x) == <dy ⊗ x, W>.
   law weight_adjoint:
     for w: List<&2, List<&2, Nat>>
     for g: List<&2, Nat>
     for +v: List<&2, Nat>
     {Spec.dotn(g, Spec.mv(w, v)) == Spec.frob(Spec.outer(g, v), w) : Nat}
  LAWS.adjoint_seq (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=adjoint_seq)
   # LAW (adjoint_seq): Seq runs the second layer's backward pass, then the first's. For two linear layers that is
   # W1ᵀ·(W2ᵀ·dy), and it is the adjoint of the composed forward pass W2·(W1·x): the chain rule, for linear maps.
   law adjoint_seq:
     for +w1: List<&2, List<&2, Nat>>
     for +w2: List<&2, List<&2, Nat>>
     for +g: List<&2, Nat>
     for +v: List<&2, Nat>
     {Spec.dotn(g, Spec.mv(w2, Spec.mv(w1, v))) == Spec.dotn(Spec.mtv(w1, Spec.mtv(w2, g)), v) : Nat}
  LAWS.seq_chain (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=seq_chain)
   # LAW (seq_chain): T.Seq's own code, running two linear layers of the exact model one after the other, gives a backward
   # pass that is the adjoint of its forward pass: dy·y == dx·x, for the y the forward pass returns and the dx its backward
   # pass returns from the state the forward pass saved. adjoint_seq says it of the formulas; this says it of the
   # combinator that composes the layers: Seq feeds the second layer's input gradient to the first, the chain rule.
   law seq_chain:
     for +w1: List<&2, List<&2, Nat>>
     for +w2: List<&2, List<&2, Nat>>
     for +x: List<&2, Nat>
     for +dy: List<&2, Nat>
     for g1: List<&2, List<&2, Nat>>
     for g2: List<&2, List<&2, Nat>>
     {Spec.dotn(dy, Spec.fy(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, T.Layer.fwd(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, Spec.SeqL(), T.Two{w1, w2}, x))) == Spec.dotn(Spec.bdx(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, T.Layer.bwd(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, Spec.SeqL(), T.Two{w1, w2}, Spec.fsv(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, T.Layer.fwd(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, Spec.SeqL(), T.Two{w1, w2}, x)), dy, T.Two{g1, g2})), x) : Nat}
  LAWS.fork_sum (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=fork_sum)
   # LAW (fork_sum): T.Fork's own code, giving one input to two linear layers, gives as input gradient the sum of the two
   # layers' input gradients, and that sum is the adjoint of the pair of outputs: dy1·y1 + dy2·y2 == dx·x. A residual
   # block (Fork of the identity and a layer) and attention's q, k, v projections rely on it.
   law fork_sum:
     for +w1: List<&2, List<&2, Nat>>
     for +w2: List<&2, List<&2, Nat>>
     for +x: List<&2, Nat>
     for +dy1: List<&2, Nat>
     for +dy2: List<&2, Nat>
     for g1: List<&2, List<&2, Nat>>
     for g2: List<&2, List<&2, Nat>>
     {Spec.pdot(T.Two{dy1, dy2}, Spec.fy(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, T.Two<List<&2, Nat>, List<&2, Nat>>, T.Two<List<&2, Nat>, List<&2, Nat>>, T.Layer.fwd(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, T.Two<List<&2, Nat>, List<&2, Nat>>, Spec.ForkL(), T.Two{w1, w2}, x))) == Spec.dotn(Spec.bdx(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, T.Layer.bwd(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, T.Two<List<&2, Nat>, List<&2, Nat>>, Spec.ForkL(), T.Two{w1, w2}, Spec.fsv(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, T.Two<List<&2, Nat>, List<&2, Nat>>, T.Two<List<&2, Nat>, List<&2, Nat>>, T.Layer.fwd(T.Two<List<&2, List<&2, Nat>>, List<&2, List<&2, Nat>>>, List<&2, Nat>, T.Two<List<&2, Nat>, List<&2, Nat>>, T.Two<List<&2, Nat>, List<&2, Nat>>, Spec.ForkL(), T.Two{w1, w2}, x)), T.Two{dy1, dy2}, T.Two{g1, g2})), x) : Nat}
  LAWS.both_sum (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=both_sum)
   # LAW (both_sum): T.Both's own code, running two linear layers side by side on the two inputs of a pair, gives a backward
   # pass that is the adjoint of its forward pass: dy1·y1 + dy2·y2 == dx1·x1 + dx2·x2. Each layer gets its own input's
   # gradient and nothing crosses between the two sides. Attention applies RoPE to q and k this way (Both(RoPE, Both(RoPE,
   # Id))).
   law both_sum:
     for +w1: List<&2, List<&2, Nat>>
     for +w2: List<&2, List<&2, Nat>>
     for +x1: List<&2, Nat>
     for +x2: List<&2, Nat>
     for +dy1: List<&2, Nat>
     for +dy2: List<&2, Nat>
     …
  LAWS.residual (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=residual)
   # LAW (residual): T.Residual's own code (T.ResidualOf: Seq(Fork(Id, f), Add2)), with a linear layer as f, gives a
   # backward pass that is the adjoint of its forward pass: for y = x + W·x and its dx, dy·y == dx·x. The backward pass
   # hands dy to both branches and adds what comes back, dx = dy + Wᵀ·dy: the gradient goes through the skip connection
   # untouched and through the layer, the rule every block of the Llama models relies on twice. (Over matrices the join
   # is Add2; here it is its twin over vectors, a + b forward and dy to both backward.)
   law residual:
     for +w: List<&2, List<&2, Nat>>
     for +x: List<&2, Nat>
     for +dy: List<&2, Nat>
     for g: List<&2, List<&2, Nat>>
     {Spec.dotn(dy, Spec.fy(T.Two<T.Two<Unit, List<&2, List<&2, Nat>>>, Unit>, List<&2, Nat>, T.Two<T.Two<Unit, List<&2, Nat>>, Unit>, T.Layer.fwd(T.Two<T.Two<Unit, List<&2, List<&2, Nat>>>, Unit>, List<&2, Nat>, List<&2, Nat>, T.Two<T.Two<Unit, List<&2, Nat>>, Unit>, Spec.ResL(), T.Two{T.Two{Unit{}, w}, Unit{}}, x))) == Spec.dotn(Spec.bdx(T.Two<T.Two<Unit, List<&2, List<&2, Nat>>>, Unit>, List<&2, Nat>, T.Layer.bwd(T.Two<T.Two<Unit, List<&2, List<&2, Nat>>>, Unit>, List<&2, Nat>, List<&2, Nat>, T.Two<T.Two<Unit, List<&2, Nat>>, Unit>, Spec.ResL(), T.Two{T.Two{Unit{}, w}, Unit{}}, Spec.fsv(T.Two<T.Two<Unit, List<&2, List<&2, Nat>>>, Unit>, List<&2, Nat>, T.Two<T.Two<Unit, List<&2, Nat>>, Unit>, T.Layer.fwd(T.Two<T.Two<Unit, List<&2, List<&2, Nat>>>, Unit>, List<&2, Nat>, List<&2, Nat>, T.Two<T.Two<Unit, List<&2, Nat>>, Unit>, Spec.ResL(), T.Two{T.Two{Unit{}, w}, Unit{}}, x)), dy, T.Two{T.Two{Unit{}, g}, Unit{}})), x) : Nat}
  LAWS.causal_keys (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=causal_keys)
   # LAW (causal_keys): T.Attention reads keys only through T.qrow, and the scores it builds for the query at position i
   # come from keys 0..i, one per key: exactly i + 1 of them. So no key after position i is read, and T.causal_row (law
   # causal) gets the i + 1 scores its condition asks for: past them, the row of probabilities is zeros.
   law causal_keys:
     for +i: Nat
     for +hd: Nat
     for +qs: U32
     for +qc: U32
     for +ks: U32
     for +kc: U32
     for q: Array<F32>
     …
  LAWS.causal (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=causal)
   # LAW (causal): in T.Attention, row i of a head's probabilities is a softmax over exactly i + 1 positions. T.prow
   # writes the query's scores from the start of its row and runs the softmax over as many positions as it wrote; the count
   # is the one the softmax's own division loop reports (T.psmc), and this law says it is i + 1, the keys 0..i of
   # causal_keys. P starts as zeros and nothing else writes the row, so its other t - (i + 1) positions stay 0: no
   # probability lands on a later position.
   law causal:
     for +i: Nat
     for +t: Nat
     for +hd: Nat
     for +sc: F32
     for +qs: U32
     …
  LAWS.full_keys (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=full_keys)
   # LAW (full_keys): FullAttention's frow reads every key 0..m, so a row's scores are 1 + m long, not 1 + i.
   law full_keys:
     for +i: Nat
     for +m: Nat
     for +hd: Nat
     for +qs: U32
     for +qc: U32
     for +ks: U32
     for +kc: U32
     for q: Array<F32>
     for k: Array<F32>
     {List.length(&2, F32, T.dr_row(T.frow(i, m, hd, qs, qc, ks, kc, q, k))) == 1n+m : Nat}
  LAWS.full (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=full)
   # LAW (full): row i of a head's probabilities in FullAttention is a softmax over all t positions.
   law full:
     for +i: Nat
     for +m: Nat
     for +hd: Nat
     for +sc: F32
     for +qs: U32
     for +qc: U32
     for +ks: U32
     for +kc: U32
     for q: Array<F32>
     …
  LAWS.full_grad (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=full_grad)
   # LAW (full_grad): the backward's G row for row i sums over all t keys, not 1 + i.
   law full_grad:
     for +i: Nat
     for +m: Nat
     for +hd: Nat
     for +sc: F32
     for +ds: U32
     for +dc: U32
     for +vs: U32
     for +vc: U32
     for d: Array<F32>
     …
  LAWS.causal_grad (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=causal_grad)
   # LAW (causal_grad): in T.Attention's backward pass, row i of a head's G (the gradient of its scores) is computed over
   # exactly i + 1 positions. T.grow reads dP's row against values 0..i only (as qrow reads keys 0..i), writes it from the
   # start of its row and runs the softmax's backward pass over as many positions as it wrote; this law says that count is
   # i + 1. G starts as zeros and nothing else writes the row, so its other t - (i + 1) positions stay 0: no gradient
   # reaches a key or a value after the query's position.
   law causal_grad:
     for +i: Nat
     for +t: Nat
     for +hd: Nat
     for +sc: F32
     for +ds: U32
     …
  LAWS.attn_par_fwd (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=attn_par_fwd)
   # LAW (attn_par_fwd): T.Attention runs its sequences in a tree of parallel lets (T.fpar: the sequences cut in halves,
   # each half cut again, d levels deep, the leaves' outputs appended). Whatever the depth and however the sequences are
   # split between the two halves, the tree gives exactly what T.fleaf gives running them one after another, in order: the
   # parallel forward pass is the sequential one, and its output does not depend on d or on the thread count.
   law attn_par_fwd:
     for d: Nat
     for gs: T.Halves<T.FS>
     for +n: Nat
     for +h: Nat
     for +dm: T.Dm
     {T.fpar(d, gs, n, h, dm) == T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array<F32>>}
  LAWS.attn_par_fwd_full (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=attn_par_fwd_full)
   # LAW (attn_par_fwd_full): the same tree law for FullAttention's forward leaf: fpar_full at any depth gives exactly
   # what fleaf_full gives running the sequences one after another, so a full-attention forward does not depend on the
   # depth or the thread count either.
   law attn_par_fwd_full:
     for d: Nat
     for gs: T.Halves<T.FS>
     for +n: Nat
     for +h: Nat
     for +dm: T.Dm
     {T.fpar_full(d, gs, n, h, dm) == T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array<F32>>}
  LAWS.attn_par_bwd (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=attn_par_bwd)
   # LAW (attn_par_bwd): the same for the backward pass: T.bpar's tree gives each sequence's dQ, dK and dV exactly as
   # T.bleaf, one sequence after another.
   law attn_par_bwd:
     for d: Nat
     for gs: T.Halves<T.BG>
     for +n: Nat
     for +kv: Nat
     for +dm: T.Dm
     {T.bpar(d, gs, n, kv, dm) == T.bleaf(T.hcat(T.BG, gs), kv, dm, Nil{}) : List<&1, T.DB>}
  LAWS.attn_par_bwd_full (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=attn_par_bwd_full)
   # LAW (attn_par_bwd_full): the tree law for FullAttention's backward leaf, as attn_par_bwd is for Attention's.
   law attn_par_bwd_full:
     for d: Nat
     for gs: T.Halves<T.BG>
     for +n: Nat
     for +kv: Nat
     for +dm: T.Dm
     {T.bpar_full(d, gs, n, kv, dm) == T.bleaf_full(T.hcat(T.BG, gs), kv, dm, Nil{}) : List<&1, T.DB>}
  LAWS.kv_of_group (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=kv_of_group)
   # LAW (kv_of_group): T.kv_of, the function both passes of T.Attention use to pick the key/value head of query head hi,
   # gives j for every head of group j: query heads j·g + 0 .. j·g + g - 1 (g = 1 + i + k, i < g) all read key/value head j.
   law kv_of_group:
     for +j: Nat
     for +i: Nat
     for +k: Nat
     {T.kv_of(Nat.add(Nat.mul(j, 1n+Nat.add(i, k)), i), 1n+Nat.add(i, k)) == j : Nat}
  LAWS.gqa_head (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=gqa_head)
   # LAW (gqa_head): with g = 1 + i + k query heads per key/value head, query head j·g + i reads key/value head
   # (j·g + i) / g = j, the head of its own group: T.Attention's forward pass picks head hi / g, and its backward pass
   # sums the gradients of heads j·g + 0 .. j·g + g - 1 into key/value head j, so both see the same groups.
   law gqa_head:
     for +j: Nat
     for +i: Nat
     for +k: Nat
     {Nat.div(Nat.add(Nat.mul(j, 1n+Nat.add(i, k)), i), 1n+Nat.add(i, k)) == j : Nat}
  LAWS.kv_cols (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=kv_cols)
   # LAW (kv_cols): the attention code takes the columns each query head reads from T.head_cols, in both passes (the head
   # loops pass no head index further, so they cannot compute other columns). With g = 1 + i + k query heads per key/value
   # head, query head j·g + i reads the key and value columns of head j: j·hd onwards.
   law kv_cols:
     for +t: Nat
     for +hd: Nat
     for +w: Nat
     for +kvw: Nat
     for +sc: F32
     for +j: Nat
     for +i: Nat
     …
  LAWS.bc_sym (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=bc_sym)
   # LAW (bc_sym): broadcasting does not depend on the order of the operands: a and b broadcast to o exactly when b and a
   # do, so x + y and y + x (and x * y, y * x) accept the same shapes.
   law bc_sym:
     for +a: List<&2, Nat>
     for +b: List<&2, Nat>
     for +o: List<&2, Nat>
     {TT.bc_ok(a, b, o) == TT.bc_ok(b, a, o) : Bool}
  LAWS.sum_numel (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=sum_numel)
   # LAW (sum_numel): summing over axis k partitions the elements: a tensor of shape s has exactly size(k) times as many
   # numbers as its sum over axis k, for every shape and every k (past the last axis the size counts as 1).
   law sum_numel:
     for +s: List<&2, Nat>
     for +k: Nat
     {TT.numel(s) == Nat.mul(TT.at1(s, k), TT.numel(TT.remove(s, k))) : Nat}
  LAWS.narrow_rest (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=narrow_rest)
   # LAW (narrow_rest): narrow (and setting any axis' size) changes only its own axis: with axis d taken out, the shape is
   # what it was.
   law narrow_rest:
     for +s: List<&2, Nat>
     for +d: Nat
     for +l: Nat
     {TT.remove(TT.setd(s, d, l), d) == TT.remove(s, d) : List<&2, Nat>}
  LAWS.narrow_axis (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=narrow_axis)
   # LAW (narrow_axis): narrowing axis d of a tensor that has it gives that axis exactly the length asked for.
   law narrow_axis:
     for +s: List<&2, Nat>
     for +d: Nat
     for +l: Nat
     for e: {True{} == Nat.is_lt(d, TT.rank(s)) : Bool}
     {TT.at1(TT.setd(s, d, l), d) == l : Nat}
  LAWS.cat_numel (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=cat_numel)
   # LAW (cat_numel): concatenating along an axis the tensor has adds the counts: a tensor whose axis d is x + y long holds
   # as many numbers as the two with x and y.
   law cat_numel:
     for +s: List<&2, Nat>
     for +d: Nat
     for +x: Nat
     for +y: Nat
     for e: {True{} == Nat.is_lt(d, TT.rank(s)) : Bool}
     {TT.numel(TT.setd(s, d, Nat.add(x, y))) == Nat.add(TT.numel(TT.setd(s, d, x)), TT.numel(TT.setd(s, d, y))) : Nat}
  LAWS.mat_numel (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=mat_numel)
   # LAW (mat_numel): a Tensor<[r, c]> holds the r·c numbers of a Mat<r, c>, so of_mat and to_mat reuse the array as it is.
   law mat_numel:
     for +r: Nat
     for +c: Nat
     {TT.numel([r, c]) == Nat.mul(r, c) : Nat}
  LAWS.permute_rank (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=permute_rank)
   # LAW (permute_rank): permuting by p gives as many axes as p has, so a permutation of the axes keeps the rank.
   law permute_rank:
     for +s: List<&2, Nat>
     for p: List<&2, Nat>
     {TT.rank(TT.permuted(s, p)) == List.length(&2, Nat, p) : Nat}
  LAWS.block_sum (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/LAWS.bend&name=block_sum)
   # LAW (block_sum): summing a row in blocks gives the row's own sum, bit for bit. tree_sum adds a row's cells in pairs,
   # pass after pass. The GPU's loss kernels instead give each block of 2^p cells to one leaf, which sums it as a balanced
   # tree of pairs, and then run tree_sum's remaining passes over the block sums. When 2^p divides the row (a row of 2^p·k
   # cells), both build the same tree of additions (torch/spec.bend), for every p, k and number of passes r after the
   # first p: the same pairs added in the same order, so the same bits in F32. Any block size that divides the row gives
   # the row's sum, which is why the mutant that shrinks the cross-entropy's blocks to one cell survives.
   law block_sum:
     for +p: Nat
     for +k: Nat
     for +r: Nat
     {Spec.passes(Nat.add(r, p), Spec.blocks(0n, Nat.mul(Spec.pw(p), k), 0n)) == Spec.passes(r, Spec.blocks(p, k, 0n)) : List<&2, Spec.Sum>}
  PROOF.dot_vadd (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=dot_vadd)
   # 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
   # (distributivity) and add4 regroups the four terms
   def 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}:
  PROOF.dot_scale (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=dot_scale)
   # 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
   def 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}:
  PROOF.dot_comm (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=dot_comm)
   # dot(a, b) == dot(b, a)
   def dot_comm(a: List<&2, Nat>, b: List<&2, Nat>) -> {Spec.dotn(a, b) == Spec.dotn(b, a) : Nat}:
  PROOF.disc (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=disc)
   def disc(b: Bool) -> Type:
  PROOF.false_true (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=false_true)
   # False == True is impossible: rewriting the goal Empty = disc(False) with it gives disc(True) = Unit
   def false_true(e: {False{} == True{} : Bool}) -> Empty:
  PROOF.len_rcat (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=len_rcat)
   # xs reversed onto acc has the length of both
   def 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}:
  PROOF.len_drow (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=len_drow)
   # drow's row has the current dot, the m after it, and acc: 1 + m + |acc| numbers
   def 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}:
  PROOF.sub0 (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=sub0)
   # n - 0 is n
   def sub0(+n: Nat) -> {Nat.sub(n, 0n) == n : Nat}:
  PROOF.cnt_div (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cnt_div)
   # 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)
   def 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}:
  PROOF.cnt_psm3 (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cnt_psm3)
   # the whole softmax over 1 + kk numbers reports 1 + kk, whatever max and exp found (they are matched, not computed)
   def 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}:
  PROOF.cnt_psm2 (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cnt_psm2)
   def 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}:
  PROOF.cnt_pw (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cnt_pw)
   # pw writes xs and counts them from n; the softmax prow3 runs on them reports 1 + (|xs| + n - 1)
   def 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}:
  PROOF.cnt_drow (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cnt_drow)
   # the count prow2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_pw
   def 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}:
  PROOF.cnt_gw (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cnt_gw)
   # gw writes xs and counts them from n: gr3 hands on |xs| + n (as cnt_pw for the forward pass)
   def 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}:
  PROOF.cnt_gdrow (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cnt_gdrow)
   # the count gr2 hands on for drow's row: 1 + m + |acc|, as len_drow, through cnt_gw (cnt_drow's twin)
   def 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}:
  PROOF.app2 (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=app2)
   # a ++ b == a2 ++ b2 from a == a2 and b == b2
   def 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>}:
  PROOF.fmap (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=fmap)
   def fmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.FS>) -> List<&1, Array<F32>>:
  PROOF.L1R (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=L1R)
   type L1R<-h: Nat, -dm: T.Dm, -xs: List<&1, T.FS>, -acc: List<&1, Array<F32>>> is Type:
     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>>}}
  PROOF.l1_con (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=l1_con)
   def 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>:
  PROOF.l1 (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=l1)
   def l1(xs: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array<F32>>) -> L1R<h, dm, xs, acc>:
  PROOF.MAR (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=MAR)
   type MAR<-h: Nat, -dm: T.Dm, -a: List<&1, T.FS>, -b: List<&1, T.FS>> is Type:
     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>>}}
  PROOF.ma_con (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=ma_con)
   def 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>:
  PROOF.map_app (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=map_app)
   def map_app(a: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>) -> MAR<h, dm, a, b>:
  PROOF.GAR (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=GAR)
   type GAR<-a: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>> is Type:
     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>}}
  PROOF.ga_con (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=ga_con)
   def 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>:
  PROOF.go_app (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=go_app)
   def go_app(a: List<&1, T.FS>, -b: List<&1, T.FS>, -c: List<&1, T.FS>) -> GAR<a, b, c>:
  PROOF.CGR (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=CGR)
   type CGR<-k: Nat, -xs: List<&1, T.FS>, -acc: List<&1, T.FS>> is Type:
     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>}}
  PROOF.cg_base (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cg_base)
   def 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>:
  PROOF.cg_con (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cg_con)
   def 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>:
  PROOF.cg (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cg)
   def cg(k: Nat, xs: List<&1, T.FS>, acc: List<&1, T.FS>) -> CGR<k, xs, acc>:
  PROOF.MR (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=MR)
   type MR<-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, -h: Nat, -dm: T.Dm> is Type:
     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>>}}
  PROOF.m0c (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=m0c)
   # depth 0: the two leaves' loops, appended
   def 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>:
  PROOF.m0b (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=m0b)
   def 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>:
  PROOF.m0a (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=m0a)
   def 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>:
  PROOF.m1c (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=m1c)
   # depth 1 + e: each half cut in two and its tree (the closures run main at depth e), then the two maps appended
   def 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>:
  PROOF.m1b (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=m1b)
   def 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>:
  PROOF.m1a (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=m1a)
   def 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>:
  PROOF.tree (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=tree)
   def tree(d: Nat, gs: T.Halves<T.FS>, +n: Nat, +h: Nat, +dm: T.Dm) -> MR<d, gs, n, h, dm>:
  PROOF.par_fin (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=par_fin)
   # the law: the tree gives what fleaf, the loop over the sequences one after another, gives
   def 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>>}:
  PROOF.par_mid (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=par_mid)
   def 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>>}:
  PROOF.ffmap (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=ffmap)
   def ffmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.FS>) -> List<&1, Array<F32>>:
  PROOF.L1RF (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=L1RF)
   type L1RF<-h: Nat, -dm: T.Dm, -xs: List<&1, T.FS>, -acc: List<&1, Array<F32>>> is Type:
     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>>}}
  PROOF.lf_con (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=lf_con)
   def 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>:
  PROOF.lf1 (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=lf1)
   def lf1(xs: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -acc: List<&1, Array<F32>>) -> L1RF<h, dm, xs, acc>:
  PROOF.MARF (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=MARF)
   type MARF<-h: Nat, -dm: T.Dm, -a: List<&1, T.FS>, -b: List<&1, T.FS>> is Type:
     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>>}}
  PROOF.ma_conf (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=ma_conf)
   def 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>:
  PROOF.map_appf (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=map_appf)
   def map_appf(a: List<&1, T.FS>, +h: Nat, +dm: T.Dm, -b: List<&1, T.FS>) -> MARF<h, dm, a, b>:
  PROOF.MRF (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=MRF)
   type MRF<-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, -h: Nat, -dm: T.Dm> is Type:
     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>>}}
  PROOF.fm0c (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=fm0c)
   # depth 0: the two leaves' loops, appended
   def 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>:
  PROOF.fm0b (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=fm0b)
   def 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>:
  PROOF.fm0a (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=fm0a)
   def 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>:
  PROOF.fm1c (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=fm1c)
   # depth 1 + e: each half cut in two and its treef (the closures run main at depth e), then the two maps appended
   def 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>:
  PROOF.fm1b (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=fm1b)
   def 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>:
  PROOF.fm1a (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=fm1a)
   def 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>:
  PROOF.treef (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=treef)
   def treef(d: Nat, gs: T.Halves<T.FS>, +n: Nat, +h: Nat, +dm: T.Dm) -> MRF<d, gs, n, h, dm>:
  PROOF.par_fin_f (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=par_fin_f)
   # the law: the treef gives what fleaf, the loop over the sequences one after another, gives
   def 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>>}:
  PROOF.par_mid_f (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=par_mid_f)
   def 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>>}:
  PROOF.b_fmap (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_fmap)
   def b_fmap(+h: Nat, +dm: T.Dm, xs: List<&1, T.BG>) -> List<&1, T.DB>:
  PROOF.b_L1R (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_L1R)
   type b_L1R<-h: Nat, -dm: T.Dm, -xs: List<&1, T.BG>, -acc: List<&1, T.DB>> is Type:
     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>}}
  PROOF.b_l1_con (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_l1_con)
   def 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>:
  PROOF.b_l1 (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_l1)
   def b_l1(xs: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -acc: List<&1, T.DB>) -> b_L1R<h, dm, xs, acc>:
  PROOF.b_MAR (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_MAR)
   type b_MAR<-h: Nat, -dm: T.Dm, -a: List<&1, T.BG>, -b: List<&1, T.BG>> is Type:
     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>}}
  PROOF.b_ma_con (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_ma_con)
   def 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>:
  PROOF.b_map_app (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_map_app)
   def b_map_app(a: List<&1, T.BG>, +h: Nat, +dm: T.Dm, -b: List<&1, T.BG>) -> b_MAR<h, dm, a, b>:
  PROOF.b_GAR (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_GAR)
   type b_GAR<-a: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>> is Type:
     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>}}
  PROOF.b_ga_con (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_ga_con)
   def 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>:
  PROOF.b_go_app (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_go_app)
   def b_go_app(a: List<&1, T.BG>, -b: List<&1, T.BG>, -c: List<&1, T.BG>) -> b_GAR<a, b, c>:
  PROOF.b_CGR (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_CGR)
   type b_CGR<-k: Nat, -xs: List<&1, T.BG>, -acc: List<&1, T.BG>> is Type:
     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>}}
  PROOF.b_cg_base (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_cg_base)
   def 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>:
  PROOF.b_cg_con (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_cg_con)
   def 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>:
  PROOF.b_cg (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_cg)
   def b_cg(k: Nat, xs: List<&1, T.BG>, acc: List<&1, T.BG>) -> b_CGR<k, xs, acc>:
  PROOF.b_MR (https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_MR)
   type b_MR<-d: Nat, -gs: T.Halves<T.BG>, -n: Nat, -h: Nat, -dm: T.Dm> is Type:
     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>}}
More: https://jend.leeeet.dev/packages/bendtorch.txt?definitions_offset=100