def slots_length

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/array.bend:103

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

103def slots_length(-T: Data, +d: Nat, +t: Tree<T>, +pf: {perfect(T, d, t) == True{} : Bool}) -> {SC.length(T, slots(T, t)) == SC.pow2(d) : Nat}:
104  match d t:
105    case 0n TLeaf{x}:
106      {==}
107    case 0n TNode{l, r}:
108      Empty.absurd({SC.length(T, slots(T, TNode{l, r})) == 1n : Nat}, L.false_true(pf))
109    case 1n+p TLeaf{x}:
110      Empty.absurd({1n == Nat.double(SC.pow2(p)) : Nat}, L.false_true(pf))
111    case 1n+ +p TNode{+l, +r}:
112      %Equal.sym(Nat, SC.length(T, SC.append(T, slots(T, l), slots(T, r))), Nat.add(SC.length(T, slots(T, l)), SC.length(T, slots(T, r))), LL.length_append(T, slots(T, l), slots(T, r))) : {_ == Nat.double(SC.pow2(p)) : Nat}
113      %Equal.sym(Nat, SC.length(T, slots(T, l)), SC.pow2(p), slots_length(T, p, l, pf_left(T, p, l, r, pf))) : {Nat.add(_, SC.length(T, slots(T, r))) == Nat.double(SC.pow2(p)) : Nat}
114      %Equal.sym(Nat, SC.length(T, slots(T, r)), SC.pow2(p), slots_length(T, p, r, pf_right(T, p, l, r, pf))) : {Nat.add(SC.pow2(p), _) == Nat.double(SC.pow2(p)) : Nat}
115      Equal.sym(Nat, Nat.double(SC.pow2(p)), Nat.add(SC.pow2(p), SC.pow2(p)), NA.double_self(SC.pow2(p)))