def sim_exit

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

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

268def sim_exit(+a: WU.U64, +b: WU.U64, +c: Nat, +hfit: {C.fits(64n, BN.ndbl(c, BN.nbloop(140n, BN.nstrip(v(a)), v(b), BN.iz(v(b)), BN.nsm(BN.nstrip(v(a)), v(b))))) == True{} : Bool}) -> {v(G.dbl(~WU.U64, ~I.u64_op, c, G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, (G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), (b, (I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b}))))))) == BN.ndbl(c, BN.nbloop(140n, BN.nstrip(v(a)), v(b), BN.iz(v(b)), BN.nsm(BN.nstrip(v(a)), v(b)))) : Nat}:
269  +e1 = sim_bloop(140n, G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b, I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b}), {==})
270  +ex = sim_strip(a)
271  +e2 = Equal.cong(Nat, Nat, t => BN.nbloop(140n, t, v(b), I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b})), v(G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a)), BN.nstrip(v(a)), ex)
272  +ew = Equal.trans(Bool, I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b}), BN.nsm(v(G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a)), v(b)), BN.nsm(BN.nstrip(v(a)), v(b)), smv(G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b), Equal.cong(Nat, Bool, t => BN.nsm(t, v(b)), v(G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a)), BN.nstrip(v(a)), ex))
273  +e3 = nbc(140n, BN.nstrip(v(a)), v(b), v(b), I.u64_is(NM.IsZero{b}), BN.iz(v(b)), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b}), BN.nsm(BN.nstrip(v(a)), v(b)), {==}, UL.tests_is_zero(b), ew)
274  +eL = Equal.trans(Nat, v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, (G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), (b, (I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b})))))), BN.nbloop(140n, v(G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a)), v(b), I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b})), BN.nbloop(140n, BN.nstrip(v(a)), v(b), BN.iz(v(b)), BN.nsm(BN.nstrip(v(a)), v(b))), e1, Equal.trans(Nat, BN.nbloop(140n, v(G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a)), v(b), I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b})), BN.nbloop(140n, BN.nstrip(v(a)), v(b), I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b})), BN.nbloop(140n, BN.nstrip(v(a)), v(b), BN.iz(v(b)), BN.nsm(BN.nstrip(v(a)), v(b))), e2, e3))
275  +hfit2 = Equal.trans(Bool, C.fits(64n, BN.ndbl(c, v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, (G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), (b, (I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b})))))))), C.fits(64n, BN.ndbl(c, BN.nbloop(140n, BN.nstrip(v(a)), v(b), BN.iz(v(b)), BN.nsm(BN.nstrip(v(a)), v(b))))), True{}, Equal.cong(Nat, Bool, t => C.fits(64n, BN.ndbl(c, t)), v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, (G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), (b, (I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b})))))), BN.nbloop(140n, BN.nstrip(v(a)), v(b), BN.iz(v(b)), BN.nsm(BN.nstrip(v(a)), v(b))), eL), hfit)
276  Equal.trans(Nat, v(G.dbl(~WU.U64, ~I.u64_op, c, G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, (G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), (b, (I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b}))))))), BN.ndbl(c, v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, (G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), (b, (I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b}))))))), BN.ndbl(c, BN.nbloop(140n, BN.nstrip(v(a)), v(b), BN.iz(v(b)), BN.nsm(BN.nstrip(v(a)), v(b)))), sim_dbl(c, G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, (G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), (b, (I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b}))))), hfit2), Equal.cong(Nat, Nat, t => BN.ndbl(c, t), v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, 140n, (G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), (b, (I.u64_is(NM.IsZero{b}), I.u64_is(NM.Small{G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, a), b})))))), BN.nbloop(140n, BN.nstrip(v(a)), v(b), BN.iz(v(b)), BN.nsm(BN.nstrip(v(a)), v(b))), eL))