def sim_tw
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64bgcd.bend:278
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64bgcd.bend as U64bgcd
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/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/math/typed/u64laws.bend as UL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend as BN
278def sim_tw(f: Nat, +a: WU.U64, +b: WU.U64, +c: Nat, +both: Bool, +hfit: {C.fits(64n, BN.ntw(f, v(a), v(b), c, both)) == True{} : Bool}) -> {v(G.tw(~WU.U64, ~I.u64_op, ~I.u64_is, f, a, b, c, both)) == BN.ntw(f, v(a), v(b), c, both) : Nat}:
279 match f both:
280 case 0n _:
281 sim_exit(a, b, c, hfit)
282 case 1n+g False{}:
283 sim_exit(a, b, c, hfit)
284 case 1n+ +g True{}:
285 +eoa = Equal.trans(Bool, I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), BN.odd(v(I.u64_op(NM.Half{a}))), BN.odd(Nat.div(v(a), 2n)), UL.tests_odd(I.u64_op(NM.Half{a})), Equal.cong(Nat, Bool, t => BN.odd(t), v(I.u64_op(NM.Half{a})), Nat.div(v(a), 2n), UL.ops_half(a)))
286 +eob = Equal.trans(Bool, I.u64_is(NM.Odd{I.u64_op(NM.Half{b})}), BN.odd(v(I.u64_op(NM.Half{b}))), BN.odd(Nat.div(v(b), 2n)), UL.tests_odd(I.u64_op(NM.Half{b})), Equal.cong(Nat, Bool, t => BN.odd(t), v(I.u64_op(NM.Half{b})), Nat.div(v(b), 2n), UL.ops_half(b)))
287 +ee = Equal.trans(Bool, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})}))), Bool.not(Bool.or(BN.odd(Nat.div(v(a), 2n)), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})}))), BN.nev2(Nat.div(v(a), 2n), Nat.div(v(b), 2n)), Equal.cong(Bool, Bool, t => Bool.not(Bool.or(t, I.u64_is(NM.Odd{I.u64_op(NM.Half{b})}))), I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), BN.odd(Nat.div(v(a), 2n)), eoa), Equal.cong(Bool, Bool, t => Bool.not(Bool.or(BN.odd(Nat.div(v(a), 2n)), t)), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})}), BN.odd(Nat.div(v(b), 2n)), eob))
288 +x1 = Equal.cong(Nat, Nat, t => BN.ntw(g, t, v(I.u64_op(NM.Half{b})), 1n+c, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})})))), v(I.u64_op(NM.Half{a})), Nat.div(v(a), 2n), UL.ops_half(a))
289 +x2 = Equal.cong(Nat, Nat, t => BN.ntw(g, Nat.div(v(a), 2n), t, 1n+c, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})})))), v(I.u64_op(NM.Half{b})), Nat.div(v(b), 2n), UL.ops_half(b))
290 +x3 = Equal.cong(Bool, Nat, t => BN.ntw(g, Nat.div(v(a), 2n), Nat.div(v(b), 2n), 1n+c, t), Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})}))), BN.nev2(Nat.div(v(a), 2n), Nat.div(v(b), 2n)), ee)
291 +E = Equal.trans(Nat, BN.ntw(g, v(I.u64_op(NM.Half{a})), v(I.u64_op(NM.Half{b})), 1n+c, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})})))), BN.ntw(g, Nat.div(v(a), 2n), v(I.u64_op(NM.Half{b})), 1n+c, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})})))), BN.ntw(g, Nat.div(v(a), 2n), Nat.div(v(b), 2n), 1n+c, BN.nev2(Nat.div(v(a), 2n), Nat.div(v(b), 2n))), x1, Equal.trans(Nat, BN.ntw(g, Nat.div(v(a), 2n), v(I.u64_op(NM.Half{b})), 1n+c, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})})))), BN.ntw(g, Nat.div(v(a), 2n), Nat.div(v(b), 2n), 1n+c, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})})))), BN.ntw(g, Nat.div(v(a), 2n), Nat.div(v(b), 2n), 1n+c, BN.nev2(Nat.div(v(a), 2n), Nat.div(v(b), 2n))), x2, x3))
292 +hfit2 = Equal.trans(Bool, C.fits(64n, BN.ntw(g, v(I.u64_op(NM.Half{a})), v(I.u64_op(NM.Half{b})), 1n+c, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})}))))), C.fits(64n, BN.ntw(g, Nat.div(v(a), 2n), Nat.div(v(b), 2n), 1n+c, BN.nev2(Nat.div(v(a), 2n), Nat.div(v(b), 2n)))), True{}, Equal.cong(Nat, Bool, t => C.fits(64n, t), BN.ntw(g, v(I.u64_op(NM.Half{a})), v(I.u64_op(NM.Half{b})), 1n+c, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})})))), BN.ntw(g, Nat.div(v(a), 2n), Nat.div(v(b), 2n), 1n+c, BN.nev2(Nat.div(v(a), 2n), Nat.div(v(b), 2n))), E), hfit)
293 Equal.trans(Nat, v(G.tw(~WU.U64, ~I.u64_op, ~I.u64_is, g, I.u64_op(NM.Half{a}), I.u64_op(NM.Half{b}), 1n+c, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})}))))), BN.ntw(g, v(I.u64_op(NM.Half{a})), v(I.u64_op(NM.Half{b})), 1n+c, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})})))), BN.ntw(g, Nat.div(v(a), 2n), Nat.div(v(b), 2n), 1n+c, BN.nev2(Nat.div(v(a), 2n), Nat.div(v(b), 2n))), sim_tw(g, I.u64_op(NM.Half{a}), I.u64_op(NM.Half{b}), 1n+c, Bool.not(Bool.or(I.u64_is(NM.Odd{I.u64_op(NM.Half{a})}), I.u64_is(NM.Odd{I.u64_op(NM.Half{b})}))), hfit2), E)