law divstep_lt

bend-osdev-u32@0.1.0.0 · LAWS.bend:717

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

717law divstep_lt:
718  for +n: Nat
719  for +s: Nat
720  for +b: Nat
721  for +r: Nat
722  for +a: Nat
723  for +r1: Nat
724  for +t: Bool
725  for +l: Bool
726  for +g: Bool
727  for e: {Nat.add(s, U.U32Nat.dbl(n, U.U32Nat.bit(t))) == Nat.add(a, Nat.double(r)) : Nat}
728  for el: {Nat.is_lt(s, b) == l : Bool}
729  for eg: {Bool.or(t, Bool.not(l)) == g : Bool}
730  for er: {Nat.add(r1, Nat.mul(U.U32Nat.bit(g), b)) == Nat.add(s, U.U32Nat.dbl(n, Nat.mul(U.U32Nat.bit(g), U.U32Nat.bit(l)))) : Nat}
731  for ha: {Nat.is_le(a, 1n) == True{} : Bool}
732  for hr: {Nat.is_lt(r, b) == True{} : Bool}
733  for hb: {Nat.is_lt(b, U.U32Nat.dbl(n, 1n)) == True{} : Bool}
734  {Nat.is_lt(r1, b) == True{} : Bool}