def AP.size_perf

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

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

707def AP.size_perf(-T: Data, +d: Nat, +t: AP.Tree<T>, h: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}) -> {AP.size(T, t) == U32.shln(1, d) : U32}:
708  match d t:
709    case 0n APLeaf{x}:
710      {==}
711    case 0n APNode{xs, ys}:
712      Empty.absurd({AP.size(T, APNode{xs, ys}) == U32.shln(1, 0n) : U32}, AP.ft(h))
713    case 1n+p APLeaf{x}:
714      Empty.absurd({AP.size(T, APLeaf{x}) == U32.shln(1, 1n+p) : U32}, AP.ft(h))
715    case 1n+p APNode{xs, ys}:
716      +hx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), h)
717      %Equal.sym(U32, AP.size(T, xs), U32.shln(1, p), AP.size_perf(T, p, xs, hx)) : {U32.shl(_) == U32.shl(U32.shln(1, p)) : U32}
718      {==}