W64dm.ov96: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend as W64dm
Lines 84-89 of bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend&start_line=84&end_line=89

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as LW

# the 96-bit comparison of over96
def ov96(+xl: WU.U64, +xh: U32, +pl: WU.U64, +ph: U32) -> {X.over96(xl, xh, (pl, ph)) == Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))) : Bool}:
  +e1 = Equal.cong(Bool, Bool, z => Bool.or(z, Bool.and(U32.is_eq(xh, ph), X.lt(xl, pl))), U32.is_lt(xh, ph), Nat.is_lt(v(xh), v(ph)), U.is_lt_nat(xh, ph))
  +e2 = Equal.cong(Bool, Bool, z => Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(z, X.lt(xl, pl))), U32.is_eq(xh, ph), Nat.is_eq(v(xh), v(ph)), LW.eq_nat(xh, ph))
  +e3 = Equal.cong(Bool, Bool, z => Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), z)), X.lt(xl, pl), Nat.is_lt(SW.value(xl), SW.value(pl)), WA.lt_value(xl, pl))
  Equal.trans(Bool, X.over96(xl, xh, (pl, ph)), Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(U32.is_eq(xh, ph), X.lt(xl, pl))), Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))), e1, Equal.trans(Bool, Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(U32.is_eq(xh, ph), X.lt(xl, pl))), Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), X.lt(xl, pl))), Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))), e2, Equal.trans(Bool, Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), X.lt(xl, pl))), Bool.or(Nat.is_lt(v(xh), v(ph)), Bool.and(Nat.is_eq(v(xh), v(ph)), Nat.is_lt(SW.value(xl), SW.value(pl)))), Nat.is_lt(Nat.add(SW.value(xl), C.shift(64n, v(xh))), Nat.add(SW.value(pl), C.shift(64n, v(ph)))), e3, WW.lt_limbs(64n, SW.value(xl), v(xh), SW.value(pl), v(ph), fit64(xl), fit64(pl)))))

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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.is_eq
  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=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=is_lt_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend&name=eq_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend&name=lt_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend&name=fit64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=lt_limbs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=over96