def sim_bnx

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64bgcd.bend:236

import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
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/math/typed/u64laws.bend as UL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend as BN

236def sim_bnx(+g: Nat, +a: WU.U64, +s: WU.U64, ih: @+a2: WU.U64 -> @+d2: WU.U64 -> {v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, g, (a2, (d2, (I.u64_is(NM.IsZero{d2}), I.u64_is(NM.Small{a2, d2})))))) == BN.nbloop(g, v(a2), v(d2), I.u64_is(NM.IsZero{d2}), I.u64_is(NM.Small{a2, d2})) : Nat}, +lb: Bool, +hl: {I.u64_is(NM.Lt{s, a}) == lb : Bool}) -> {v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, g, G.bnx2(~WU.U64, ~I.u64_op, ~I.u64_is, a, s, lb))) == BN.nbloop(g, BN.nba(v(a), v(s), lb), BN.nbd(v(a), v(s), lb), BN.iz(BN.nbd(v(a), v(s), lb)), BN.nsm(BN.nba(v(a), v(s), lb), BN.nbd(v(a), v(s), lb))) : Nat}:
237  match lb:
238    case True{}:
239      +hlt = Equal.trans(Bool, Nat.is_lt(v(s), v(a)), I.u64_is(NM.Lt{s, a}), True{}, Equal.sym(Bool, I.u64_is(NM.Lt{s, a}), Nat.is_lt(v(s), v(a)), UL.tests_lt(s, a)), hl)
240      +hle = N.lt_le(v(s), v(a), hlt)
241      +r = ih(s, I.u64_op(NM.Sub{a, s}))
242      +ez = Equal.trans(Bool, I.u64_is(NM.IsZero{I.u64_op(NM.Sub{a, s})}), BN.iz(v(I.u64_op(NM.Sub{a, s}))), BN.iz(Nat.sub(v(a), v(s))), UL.tests_is_zero(I.u64_op(NM.Sub{a, s})), Equal.cong(Nat, Bool, t => BN.iz(t), v(I.u64_op(NM.Sub{a, s})), Nat.sub(v(a), v(s)), UL.ops_sub(a, s, hle)))
243      +ew = Equal.trans(Bool, I.u64_is(NM.Small{s, I.u64_op(NM.Sub{a, s})}), BN.nsm(v(s), v(I.u64_op(NM.Sub{a, s}))), BN.nsm(v(s), Nat.sub(v(a), v(s))), smv(s, I.u64_op(NM.Sub{a, s})), Equal.cong(Nat, Bool, t => BN.nsm(v(s), t), v(I.u64_op(NM.Sub{a, s})), Nat.sub(v(a), v(s)), UL.ops_sub(a, s, hle)))
244      Equal.trans(Nat, v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, g, (s, (I.u64_op(NM.Sub{a, s}), (I.u64_is(NM.IsZero{I.u64_op(NM.Sub{a, s})}), I.u64_is(NM.Small{s, I.u64_op(NM.Sub{a, s})})))))), BN.nbloop(g, v(s), v(I.u64_op(NM.Sub{a, s})), I.u64_is(NM.IsZero{I.u64_op(NM.Sub{a, s})}), I.u64_is(NM.Small{s, I.u64_op(NM.Sub{a, s})})), BN.nbloop(g, v(s), Nat.sub(v(a), v(s)), BN.iz(Nat.sub(v(a), v(s))), BN.nsm(v(s), Nat.sub(v(a), v(s)))), r, nbc(g, v(s), v(I.u64_op(NM.Sub{a, s})), Nat.sub(v(a), v(s)), I.u64_is(NM.IsZero{I.u64_op(NM.Sub{a, s})}), BN.iz(Nat.sub(v(a), v(s))), I.u64_is(NM.Small{s, I.u64_op(NM.Sub{a, s})}), BN.nsm(v(s), Nat.sub(v(a), v(s))), UL.ops_sub(a, s, hle), ez, ew))
245    case False{}:
246      +hge = N.not_lt_le(v(s), v(a), Equal.trans(Bool, Nat.is_lt(v(s), v(a)), I.u64_is(NM.Lt{s, a}), False{}, Equal.sym(Bool, I.u64_is(NM.Lt{s, a}), Nat.is_lt(v(s), v(a)), UL.tests_lt(s, a)), hl))
247      +r = ih(a, I.u64_op(NM.Sub{s, a}))
248      +ez = Equal.trans(Bool, I.u64_is(NM.IsZero{I.u64_op(NM.Sub{s, a})}), BN.iz(v(I.u64_op(NM.Sub{s, a}))), BN.iz(Nat.sub(v(s), v(a))), UL.tests_is_zero(I.u64_op(NM.Sub{s, a})), Equal.cong(Nat, Bool, t => BN.iz(t), v(I.u64_op(NM.Sub{s, a})), Nat.sub(v(s), v(a)), UL.ops_sub(s, a, hge)))
249      +ew = Equal.trans(Bool, I.u64_is(NM.Small{a, I.u64_op(NM.Sub{s, a})}), BN.nsm(v(a), v(I.u64_op(NM.Sub{s, a}))), BN.nsm(v(a), Nat.sub(v(s), v(a))), smv(a, I.u64_op(NM.Sub{s, a})), Equal.cong(Nat, Bool, t => BN.nsm(v(a), t), v(I.u64_op(NM.Sub{s, a})), Nat.sub(v(s), v(a)), UL.ops_sub(s, a, hge)))
250      Equal.trans(Nat, v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, g, (a, (I.u64_op(NM.Sub{s, a}), (I.u64_is(NM.IsZero{I.u64_op(NM.Sub{s, a})}), I.u64_is(NM.Small{a, I.u64_op(NM.Sub{s, a})})))))), BN.nbloop(g, v(a), v(I.u64_op(NM.Sub{s, a})), I.u64_is(NM.IsZero{I.u64_op(NM.Sub{s, a})}), I.u64_is(NM.Small{a, I.u64_op(NM.Sub{s, a})})), BN.nbloop(g, v(a), Nat.sub(v(s), v(a)), BN.iz(Nat.sub(v(s), v(a))), BN.nsm(v(a), Nat.sub(v(s), v(a)))), r, nbc(g, v(a), v(I.u64_op(NM.Sub{s, a})), Nat.sub(v(s), v(a)), I.u64_is(NM.IsZero{I.u64_op(NM.Sub{s, a})}), BN.iz(Nat.sub(v(s), v(a))), I.u64_is(NM.Small{a, I.u64_op(NM.Sub{s, a})}), BN.nsm(v(a), Nat.sub(v(s), v(a))), UL.ops_sub(s, a, hge), ez, ew))