def size_thaw

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

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/u32.bend as U

222def size_thaw(-T: Data, +d: Nat, +t: Tree<T>, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.size(T, thaw(T, t)) == (thaw(T, t), U.pow2u(d)) : Array<T> & U32}:
223  match d t:
224    case 0n TLeaf{x}:
225      {==}
226    case 0n TNode{l, r}:
227      Empty.absurd({Array.size(T, thaw(T, TNode{l, r})) == (thaw(T, TNode{l, r}), 1) : Array<T> & U32}, L.false_true(pf))
228    case 1n+p TLeaf{x}:
229      Empty.absurd({Array.size(T, ALeaf{x}) == (ALeaf{x}, U.pow2u(1n+p)) : Array<T> & U32}, L.false_true(pf))
230    case 1n+ +p TNode{+l, +r}:
231      %Equal.sym(Array<T> & U32, Array.size(T, thaw(T, l)), (thaw(T, l), U.pow2u(p)), size_thaw(T, p, l, pf_left(T, p, l, r, pf))) : {Array.size.node(T, thaw(T, r), _) == (ANode{thaw(T, l), thaw(T, r)}, U32.shl(U.pow2u(p))) : Array<T> & U32}
232      {==}