def cmpv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addc.bend:61

import Base
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/w64.bend as X
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/math/typed/w64add.bend as WA

61def cmpv(+a: WU.U64, +b: WU.U64) -> {X.cmp(a, b) == Nat.cmp(SW.value(a), SW.value(b)) : Cmp}:
62  l1 = WA.lt_value(a, b)
63  q1 = WA.eq_value(a, b)
64  +e1 = Equal.cong(Bool, Cmp, t => X.cmp_pick(t, X.eq(a, b)), X.lt(a, b), Nat.is_lt(SW.value(a), SW.value(b)), l1)
65  +e2 = Equal.cong(Bool, Cmp, t => X.cmp_pick(Nat.is_lt(SW.value(a), SW.value(b)), t), X.eq(a, b), Nat.is_eq(SW.value(a), SW.value(b)), q1)
66  Equal.trans(Cmp, X.cmp_pick(X.lt(a, b), X.eq(a, b)), X.cmp_pick(Nat.is_lt(SW.value(a), SW.value(b)), X.eq(a, b)), Nat.cmp(SW.value(a), SW.value(b)), e1, Equal.trans(Cmp, X.cmp_pick(Nat.is_lt(SW.value(a), SW.value(b)), X.eq(a, b)), X.cmp_pick(Nat.is_lt(SW.value(a), SW.value(b)), Nat.is_eq(SW.value(a), SW.value(b))), Nat.cmp(SW.value(a), SW.value(b)), e2, cp_c(SW.value(a), SW.value(b), Nat.cmp(SW.value(a), SW.value(b)), {==})))