def AP.tof_leaves

bend-osdev-array@0.1.0.1 · PROOF.bend:1435

import Base
import bend-osdev-array@0.1.0.1/array.bend as A
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

1435def AP.tof_leaves(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T, +h: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}) -> {A.Arrays.leaves(T, AP.build(T, AP.tof(T, d, xs, f))) == xs : List<&2, T>}:
1436  match d:
1437    case 0n:
1438      AP.one_elem(T, xs, f, h)
1439    case 1n+ +p:
1440      +s = A.Arrays.slots(p)
1441      +l = List.take(&2, T, xs, s)
1442      +r = List.drop(&2, T, xs, s)
1443      +h2 = Equal.trans(Nat, List.length(&2, T, xs), Nat.double(s), Nat.add(s, s), h, UL.nat_double(s))
1444      %Equal.sym(List<&2, T>, A.Arrays.leaves(T, AP.build(T, AP.tof(T, p, l, f))), l, AP.tof_leaves(T, p, l, f, AP.len_take(T, xs, s, s, h2))) : {List.append(&2, T, _, A.Arrays.leaves(T, AP.build(T, AP.tof(T, p, r, f)))) == xs : List<&2, T>}
1445      %Equal.sym(List<&2, T>, A.Arrays.leaves(T, AP.build(T, AP.tof(T, p, r, f))), r, AP.tof_leaves(T, p, r, f, AP.len_drop(T, xs, s, s, h2))) : {List.append(&2, T, l, _) == xs : List<&2, T>}
1446      AP.take_drop(T, xs, s)