law divstep_value

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

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

698law divstep_value:
699  for +n: Nat
700  for +s: Nat
701  for +b: Nat
702  for +r: Nat
703  for +a: Nat
704  for +r1: Nat
705  for +t: Bool
706  for +l: Bool
707  for +g: Bool
708  for e: {Nat.add(s, U.U32Nat.dbl(n, U.U32Nat.bit(t))) == Nat.add(a, Nat.double(r)) : Nat}
709  for el: {Nat.is_lt(s, b) == l : Bool}
710  for eg: {Bool.or(t, Bool.not(l)) == g : Bool}
711  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}
712  for ha: {Nat.is_le(a, 1n) == True{} : Bool}
713  for hr: {Nat.is_lt(r, b) == True{} : Bool}
714  for hb: {Nat.is_lt(b, U.U32Nat.dbl(n, 1n)) == True{} : Bool}
715  {Nat.add(r1, Nat.mul(U.U32Nat.bit(g), b)) == Nat.add(a, Nat.double(r)) : Nat}