def dm_if

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32div.bend:189

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

189def dm_if(+aw: Word(32n), +b: U32, +z: Bool, +hz: {z == False{} : Bool}, +hb: {Nat.is_lt(0n, v(b)) == True{} : Bool}) -> {Nat.add(Nat.mul(v(U32.div.if(aw, b, z)), v(b)), v(U32.mod.if(aw, b, z))) == v(U32{aw}) : Nat} & {Nat.is_lt(v(U32.mod.if(aw, b, z)), v(b)) == True{} : Bool}:
190  match z:
191    case True{}:
192      Empty.absurd({Nat.add(Nat.mul(v(U32.div.if(aw, b, True{})), v(b)), v(U32.mod.if(aw, b, True{}))) == v(U32{aw}) : Nat} & {Nat.is_lt(v(U32.mod.if(aw, b, True{})), v(b)) == True{} : Bool}, L.true_false(hz))
193    case False{}:
194      dm_fin(aw, b, U32.divmod.go(32n, aw, b), go_ok(32n, aw, b, hb, 1n, {==}))