def hi_nz_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divv.bend:36

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

36def hi_nz_c(+l: U32, +h: U32, +hf: {C.fits(32n, SW.value(WU.U64{l, h})) == False{} : Bool}, +z: Bool, +hz: {Nat.is_eq(v(h), 0n) == z : Bool}) -> {z == False{} : Bool}:
37  match z:
38    case True{}:
39      +e0 = N.eq_from_is_eq(v(h), 0n, hz)
40      +e1 = Equal.trans(Nat, SW.value(WU.U64{l, h}), Nat.add(v(l), C.shift(32n, 0n)), v(l), Equal.cong(Nat, Nat, w => Nat.add(v(l), C.shift(32n, w)), v(h), 0n, e0), N.add_zero(v(l)))
41      +f1 = L.subst(Nat, w => {C.fits(32n, w) == True{} : Bool}, v(l), SW.value(WU.U64{l, h}), Equal.sym(Nat, SW.value(WU.U64{l, h}), v(l), e1), LW.vb(l))
42      Equal.trans(Bool, True{}, C.fits(32n, SW.value(WU.U64{l, h})), False{}, Equal.sym(Bool, C.fits(32n, SW.value(WU.U64{l, h})), True{}, f1), hf)
43    case False{}:
44      {==}