LAWS.divstep_value: law of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/LAWS.bend as LAWS
Lines 698-715 of bend-osdev-u32@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&start_line=698&end_line=715

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

law divstep_value:
  for +n: Nat
  for +s: Nat
  for +b: Nat
  for +r: Nat
  for +a: Nat
  for +r1: Nat
  for +t: Bool
  for +l: Bool
  for +g: Bool
  for e: {Nat.add(s, U.U32Nat.dbl(n, U.U32Nat.bit(t))) == Nat.add(a, Nat.double(r)) : Nat}
  for el: {Nat.is_lt(s, b) == l : Bool}
  for eg: {Bool.or(t, Bool.not(l)) == g : Bool}
  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}
  for ha: {Nat.is_le(a, 1n) == True{} : Bool}
  for hr: {Nat.is_lt(r, b) == True{} : Bool}
  for hb: {Nat.is_lt(b, U.U32Nat.dbl(n, 1n)) == True{} : Bool}
  {Nat.add(r1, Nat.mul(U.U32Nat.bit(g), b)) == Nat.add(a, Nat.double(r)) : Nat}

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ud.k
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ud.p1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.bit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl