def fm1c

import bendtorch@1.3.0.0/PROOF.bend as PROOF
import Base
import bendtorch@1.3.0.0/main.bend as T
import bend-ml-tensor-array@0.1.18.0/main.bend as TA

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))}
Uses (20)

Used by (1)

bendtorch@1.3.0.0/PROOF:fm1b