PROOF.b_m1c: def of bendtorch@1.3.0.0 Import: import bendtorch@1.3.0.0/PROOF.bend as PROOF Lines 669-679 of bendtorch@1.3.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/PROOF.bend&start_line=669&end_line=679 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 # depth 1 + e: each half cut in two and its b_tree (the closures run main at depth e), then the two maps appended def b_m1c(-e: Nat, -l: List<&1, T.BG>, -r: List<&1, T.BG>, +n: Nat, +h: Nat, +dm: T.Dm, -hh1: T.Halves, s1: {hh1 == T.cut(T.BG, TA.half(TA.half(n)), l, Nil{}) : T.Halves}, +cat1: {T.hcat(T.BG, hh1) == l : List<&1, T.BG>}, -hh2: T.Halves, s2: {hh2 == T.cut(T.BG, TA.half(Nat.sub(n, TA.half(n))), r, Nil{}) : T.Halves}, +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) -> b_MR<1n+e, T.Halves{l, r}, n, h, dm>: match ma: case b_MAR{y1b, sb, fa}: +ly1 = Equal.trans(List<&1, T.BG>, y1, T.hcat(T.BG, hh1), l, sy1, cat1) +ly2 = Equal.trans(List<&1, T.BG>, y2, T.hcat(T.BG, hh2), r, sy2, cat2) +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, 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, 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))) +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, 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, 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))) +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)))) 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), 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))} Uses (19): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor-array@0.1.19.0/main.bend&name=half https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=app2 https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_MAR https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_MR https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_fmap https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=BG https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=DB https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=Dm https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=Halves https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=bpar https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=cut https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=hcat