law base

lawful-fields@0.1.1.0 · proof_num.bend:440

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

440law base:
441  for +ok: Bool
442  for +acc: U32
443  for +m: Maybe<&2, Nat>
444  for +M: Nat
445  for +hi: Inv(ok, acc, m, M)
446  {F.nat_of(C.num.fin(acc, ok)) == F.decb.of(m, M) : Maybe<&2, Nat>}