~/jendhub

law esum

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1359

import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend
import Base

1359# l1 + (n - h) = ld + n.
1360law esum:
1361  for +ld: U32
1362  for +l1: U32
1363  for +n: U32
1364  for +el: {U32.to_nat(l1) == Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))) : Nat}
1365  {Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))) == Nat.add(U32.to_nat(ld), U32.to_nat(n)) : Nat}

Uses (14)

Used by (1)