law dm_ok

lawful-words@0.1.0.0 · proof_u32.bend:799

import lawful-words@0.1.0.0/proof_u32.bend as ProofU32

import Base

799law dm_ok:
800  for +k: Nat
801  for +a: Word(k)
802  for +b: U32
803  for +hb: {Nat.is_lt(0n, U32.to_nat(b)) == True{} : Bool}
804  for +m: Nat
805  for +hm: {Nat.pow(2n, 32n) == m : Nat}
806  DMOK(k, Word.to_nat(k, a), U32.to_nat(b), U32.divmod.go(k, a, b))

Uses (14)

Used by (2)