def fm0c

import bendtorch@1.3.0.0/PROOF.bend as PROOF
import Base
import bendtorch@1.3.0.0/main.bend as T

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

Used by (1)

bendtorch@1.3.0.0/PROOF:fm0b