ProofDigits.show_fin: law of lawful-fields@0.1.1.0
Import: import lawful-fields@0.1.1.0/proof_digits.bend as ProofDigits
Lines 262-267 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=262&end_line=267

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

law show_fin:
  for +g: Nat
  for +q: Nat
  for +d: U32
  for +sacc: String
  {F.codes(Nat.show.fin(g, sacc, (Chr{d}, q))) == lgo(g, q, d, F.codes(sacc)) : List<&2, U32>}

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.divmod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.show.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.show.put
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=codes
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&name=DG
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&name=eta_nn
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_digits.bend&name=lgo