ProofDigits.dtop: law of lawful-fields@0.1.1.0
Import: import lawful-fields@0.1.1.0/proof_digits.bend as ProofDigits
Lines 170-179 of lawful-fields@0.1.1.0/proof_digits.bend: https://jend.leeeet.dev/read.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&start_line=170&end_line=179

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-fields@0.1.1.0/defs.bend as F

# The start test of digits against the slice it reads.
law dtop:
  for +n: Nat
  for +from: U32
  for +to: U32
  for +xs: List<&2, U32>
  for +hn: {Nat.sub(U32.to_nat(to), U32.to_nat(from)) == n : Nat}
  for +hle: {Nat.is_le(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}
  for +hlen: {Nat.is_le(Nat.add(U32.to_nat(from), n), List.length(&2, U32, xs)) == True{} : Bool}
  {Bool.and(U32.is_lt(from, to), alld(D.slice(xs, U32.to_nat(from), n))) == Maybe.is_some(&2, Nat, F.dec(D.slice(xs, U32.to_nat(from), n))) : Bool}

Uses (32):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.drop
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.is_some
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=slice
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_same.bend&name=lt_of_le
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_seq.bend&name=take_length
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_seq.bend&name=take_zero
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_shift.bend&name=drop_length
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=dec
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&name=alld
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&name=ne_dec
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_refl
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_sub_add
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_sub_r
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_irrefl
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=is_lt_to_nat