def sim_bloop

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

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/math/typed/u64laws.bend as UL
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend as BN

252def sim_bloop(f: Nat, +a: WU.U64, +d: WU.U64, +dz: Bool, +sm: Bool, +hsm: {I.u64_is(NM.Small{a, d}) == sm : Bool}) -> {v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, f, (a, (d, (dz, sm))))) == BN.nbloop(f, v(a), v(d), dz, sm) : Nat}:
253  match f dz sm:
254    case 0n _ _:
255      {==}
256    case 1n+g True{} _:
257      {==}
258    case 1n+g False{} True{}:
259      gsv(a, d)
260    case 1n+ +g False{} False{}:
261      +s = G.strip(~WU.U64, ~I.u64_op, ~I.u64_is, d)
262      %sim_strip(d) : {v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, g, G.bnx(~WU.U64, ~I.u64_op, ~I.u64_is, a, s))) == BN.nbloop(g, BN.nba(v(a), _, Nat.is_lt(_, v(a))), BN.nbd(v(a), _, Nat.is_lt(_, v(a))), BN.iz(BN.nbd(v(a), _, Nat.is_lt(_, v(a)))), BN.nsm(BN.nba(v(a), _, Nat.is_lt(_, v(a))), BN.nbd(v(a), _, Nat.is_lt(_, v(a))))) : Nat}
263      %UL.tests_lt(s, a) : {v(G.bloop(~WU.U64, ~I.u64_op, ~I.u64_is, g, G.bnx(~WU.U64, ~I.u64_op, ~I.u64_is, a, s))) == BN.nbloop(g, BN.nba(v(a), v(s), _), BN.nbd(v(a), v(s), _), BN.iz(BN.nbd(v(a), v(s), _)), BN.nsm(BN.nba(v(a), v(s), _), BN.nbd(v(a), v(s), _))) : Nat}
264      sim_bnx(g, a, s, a2 => d2 => sim_bloop(g, a2, d2, I.u64_is(NM.IsZero{d2}), I.u64_is(NM.Small{a2, d2}), {==}), I.u64_is(NM.Lt{s, a}), {==})