law R

lawful-fields@0.1.1.0 · proof_digits.bend:585

import Base
import lawful-fields@0.1.1.0/fields.bend as FC

585# With n <= BK(k) the fuel k suffices; q = n / 10 and the spec's fuel f >= q.
586law R:
587  for +k: Nat
588  for +small: Bool
589  for +q: Nat
590  for +f: Nat
591  for +n: U32
592  for +acc: List<&2, U32>
593  for +hs: {U32.is_lt(n, 10) == small : Bool}
594  for +hq: {Nat.div(U32.to_nat(n), 10n) == q : Nat}
595  for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(k))) == True{} : Bool}
596  for +hf: {Nat.is_le(q, f) == True{} : Bool}
597  {FC.put_dec.digits(k, small, n, acc) == lgo(f, q, DG(U32.to_nat(n)), acc) : List<&2, U32>}