law size_count_t

lawful-arrays@0.1.0.0 · proof_index.bend:445

import Base
import lawful-arrays@0.1.0.0/defs.bend as D
import lawful-arrays@0.1.0.0/proof_tree.bend as P

445law size_count_t:
446  for -T: Data
447  for +t: P.Tree<T>
448  for +d: Nat
449  for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool}
450  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
451  {U32.to_nat(Pair.snd(Array<T>, U32, Array.size(T, P.fromT(T, t)))) == Nat.pow(2n, d) : Nat}