law align2

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1083

import Base

1083law align2:
1084  for +ld: U32
1085  for +k: Nat
1086  for +ek: {U32.to_nat((ld .&. 3 : U32)) == k : Nat}
1087  for +hk: {Nat.is_lt(k, 4n) == True{} : Bool}
1088  {Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))), 4n), 4n) == Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))) : Nat}