law FITSU

lawful-fields@0.1.1.0 · proof_num.bend:224

import Base

224# num's test on words is the test on numbers (c the constant, q its value).
225law FITSU:
226  for +acc: U32
227  for +x: U32
228  for +c: U32
229  for +q: Nat
230  for +M: Nat
231  for +hcq: {U32.to_nat(c) == q : Nat}
232  for +hq: {Nat.add(Nat.mul(q, 10n), 6n) == M : Nat}
233  for +hge: {U32.is_ge(x, 48) == True{} : Bool}
234  for +hle: {U32.is_le(x, 57) == True{} : Bool}
235  {Bool.or(U32.is_lt(acc, c), Bool.and(U32.is_eq(acc, c), U32.is_le(U32.sub(x, 48), 5))) == Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n)), M) : Bool}