law LN

lawful-fields@0.1.1.0 · proof_digits.bend:637

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

637law LN:
638  for +k: Nat
639  for +small: Bool
640  for +j: Nat
641  for +n: U32
642  for +acc: List<&2, U32>
643  for +hs: {U32.is_lt(n, 10) == small : Bool}
644  for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(j))) == True{} : Bool}
645  for +hj: {Nat.is_le(j, k) == True{} : Bool}
646  {Nat.is_le(List.length(&2, U32, FC.put_dec.digits(k, small, n, acc)), Nat.add(1n+j, List.length(&2, U32, acc))) == True{} : Bool}