law dw

lawful-bytes@0.1.1.0 · proof_fast_find.bend:480

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

480law dw:
481  for +t: P.Tree<U32>
482  for +d: Nat
483  for +wi: U32
484  for +o: Nat
485  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
486  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
487  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
488  for +ho: {Nat.is_le(o, 4n) == True{} : Bool}
489  {List.drop(&2, U32, UB(t), SS(wi, o)) == List.append(&2, U32, AW(t, wi, o), BW(t, wi)) : List<&2, U32>}