def wd.dz

bend-osdev-word64@0.1.1.0 · PROOF_div.bend:420

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-word64@0.1.1.0/LAWS.bend as WB
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

420def wd.dz(+hw: Word(32n), +lw: Word(32n), +b: W.W64, z: Bool, ez: {W.W64.is_zero(b) == z : Bool}, +h: {W.W64.is_zero(b) == False{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.divmod.pick(z, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(z, W.W64{U32{hw}, U32{lw}}, b)))) == W.W64.to_nat(W.W64{U32{hw}, U32{lw}}) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(z, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)) == True{} : Bool}:
421  match z:
422    case True{}:
423      Empty.absurd({Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.divmod.pick(True{}, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(True{}, W.W64{U32{hw}, U32{lw}}, b)))) == W.W64.to_nat(W.W64{U32{hw}, U32{lw}}) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(True{}, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)) == True{} : Bool}, wn.tf(Equal.trans(Bool, True{}, W.W64.is_zero(b), False{}, Equal.sym(Bool, W.W64.is_zero(b), True{}, ez), h)))
424    case False{}:
425      wd.dz2(hw, lw, b, h, wd.bits(32n, hw, b, W.W64.zero(), W.W64.zero(), Equal.trans(Bool, Nat.is_lt(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), Nat.is_lt(0n, W.W64.to_nat(b)), True{}, {==}, wd.nz(W.W64.to_nat(b), Equal.trans(Bool, Nat.is_eq(W.W64.to_nat(b), 0n), W.W64.is_zero(b), False{}, Equal.sym(Bool, W.W64.is_zero(b), Nat.is_eq(W.W64.to_nat(b), 0n), WB.eq_value(b, W.W64.zero())), h))), wv.lt64(b), Equal.trans(Bool, Nat.is_lt(Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), W.W64.to_nat(W.W64.zero()))), Word.to_nat(32n, hw)), U.U32Nat.dbl(64n, 1n)), Nat.is_lt(Word.to_nat(32n, hw), U.U32Nat.dbl(64n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(64n, 1n)), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), W.W64.to_nat(W.W64.zero()))), Word.to_nat(32n, hw)), Word.to_nat(32n, hw), Equal.sym(Nat, Word.to_nat(32n, hw), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), W.W64.to_nat(W.W64.zero()))), Word.to_nat(32n, hw)), {==})), UO.nat_lt_le_trans(Word.to_nat(32n, hw), U.U32Nat.dbl(32n, 1n), U.U32Nat.dbl(64n, 1n), UL.word_value_lt(32n, hw), UL.dbl_le_exp(32n, 64n, 1n, {==})))))