def AP.len_perf

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

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

1051def AP.len_perf(-T: Data, +d: Nat, +t: AP.Tree<T>, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}) -> {List.length(&2, T, A.Arrays.leaves(T, AP.build(T, t))) == A.Arrays.slots(d) : Nat}:
1052  match d t:
1053    case 0n APLeaf{x}:
1054      {==}
1055    case 0n APNode{xs, ys}:
1056      Empty.absurd({List.length(&2, T, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys}))) == A.Arrays.slots(0n) : Nat}, AP.ft(hp))
1057    case 1n+p APLeaf{x}:
1058      Empty.absurd({List.length(&2, T, A.Arrays.leaves(T, AP.build(T, APLeaf{x}))) == A.Arrays.slots(1n+p) : Nat}, AP.ft(hp))
1059    case 1n+ +p APNode{xs, ys}:
1060      +lx = A.Arrays.leaves(T, AP.build(T, xs))
1061      +ly = A.Arrays.leaves(T, AP.build(T, ys))
1062      +s = A.Arrays.slots(p)
1063      +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1064      +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1065      %Equal.sym(Nat, List.length(&2, T, List.append(&2, T, lx, ly)), Nat.add(List.length(&2, T, lx), List.length(&2, T, ly)), AP.len_app(T, lx, ly)) : {_ == Nat.double(s) : Nat}
1066      %Equal.sym(Nat, List.length(&2, T, lx), s, AP.len_perf(T, p, xs, hpx)) : {Nat.add(_, List.length(&2, T, ly)) == Nat.double(s) : Nat}
1067      %Equal.sym(Nat, List.length(&2, T, ly), s, AP.len_perf(T, p, ys, hpy)) : {Nat.add(s, _) == Nat.double(s) : Nat}
1068      Equal.sym(Nat, Nat.double(s), Nat.add(s, s), UL.nat_double(s))