law aw_full

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1018

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

1018law aw_full:
1019  for +n: Nat
1020  for +ts: P.Tree<U32>
1021  for +p: U32
1022  for +lo: U32
1023  for +td: P.Tree<U32>
1024  for +si: U32
1025  for +di: U32
1026  for +sh: Nat
1027  for +d: Nat
1028  for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool}
1029  {A.full(U32, P.fromT(U32, AWT(n, ts, p, lo, td, si, di, sh)), d) == True{} : Bool}