law tl_dec

lawful-bytes@0.1.1.0 · proof_same.bend:265

import Base

265# j - 1 for j = 1 + m + s.
266law tl_dec:
267  for +m: Nat
268  for +s: U32
269  for +j: U32
270  for +hj: {U32.to_nat(j) == 1n+Nat.add(m, U32.to_nat(s)) : Nat}
271  {U32.to_nat((j - 1 : U32)) == Nat.add(m, U32.to_nat(s)) : Nat}