law el1
lawful-bytes@0.1.1.0 · proof_fast_append.bend:1331
import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend
import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-arrays@0.1.0.0/proof_tree.bend as P
1331law el1:
1332 for +ld: U32
1333 for +td: P.Tree<U32>
1334 for +ls: U32
1335 for +ts: P.Tree<U32>
1336 for +d: Nat
1337 for +s: U32
1338 for +n: U32
1339 for +l1: U32
1340 for +t1: P.Tree<U32>
1341 for +e1: {C.BT(l1, t1) == D1(ld, td, ls, ts, s, n) : D.Bytes}
1342 for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1343 for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1344 {U32.to_nat(l1) == Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))) : Nat}