law step_n

lawful-bytes@0.1.1.0 · proof_find.bend:242

import Base

242law step_n:
243  for +j: U32
244  for +k: Nat
245  for +to: U32
246  for +d: Nat
247  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
248  for +hj4: {Nat.is_lt(U32.to_nat(j), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
249  for +hn: {Nat.add(U32.to_nat(j), 1n+k) == U32.to_nat(to) : Nat}
250  {Nat.add(U32.to_nat((j + 1 : U32)), k) == U32.to_nat(to) : Nat}