law full_set

lawful-bytes@0.1.1.0 · proof_core.bend:483

import Base
import lawful-arrays@0.1.0.0/defs.bend as A
import lawful-arrays@0.1.0.0/proof_tree.bend as P
import lawful-arrays@0.1.0.0/proof_index.bend as I

483law full_set:
484  for +t: P.Tree<U32>
485  for +d: Nat
486  for +k: U32
487  for +w: U32
488  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
489  {A.full(U32, P.fromT(U32, I.set_tree(U32, t, k, w)), d) == True{} : Bool}