def top_r

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:571

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/natural.bend as M
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/natural/roots.bend as RT
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/misc.bend as MS

571def top_r(+w: Nat, +hw: {Nat.is_le(Nat.add(w, w), 139n) == True{} : Bool}, +hw140: {Nat.is_le(w, 140n) == True{} : Bool}, +a: Nat, +bp: Nat, +hb: {Nat.is_lt(1n+bp, C.pow2(w)) == True{} : Bool}, +rv: Nat, +hr: {Nat.mod(a, 1n+bp) == rv : Nat}) -> {nbg_b(1n+bp, Nat.mod(a, 1n+bp), iz(Nat.mod(a, 1n+bp))) == M.gcd(a, 1n+bp) : Nat}:
572  match rv:
573    case 0n:
574      +e1 = Equal.trans(Nat, M.gcd(a, 1n+bp), M.gcd(1n+bp, Nat.mod(a, 1n+bp)), M.gcd(1n+bp, 0n), gcd_rec(a, bp), Equal.cong(Nat, Nat, t => M.gcd(1n+bp, t), Nat.mod(a, 1n+bp), 0n, hr))
575      %Equal.sym(Nat, Nat.mod(a, 1n+bp), 0n, hr) : {nbg_b(1n+bp, _, iz(_)) == M.gcd(a, 1n+bp) : Nat}
576      Equal.sym(Nat, M.gcd(a, 1n+bp), 1n+bp, e1)
577    case 1n+rp:
578      +hrl = Equal.trans(Bool, Nat.is_lt(1n+rp, 1n+bp), Nat.is_lt(Nat.mod(a, 1n+bp), 1n+bp), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, 1n+bp), 1n+rp, Nat.mod(a, 1n+bp), Equal.sym(Nat, Nat.mod(a, 1n+bp), 1n+rp, hr)), MS.divmod_lt(a, bp))
579      +hsq = mul_lt_sq(1n+bp, 1n+rp, C.pow2(w), hb, N.lt_trans(1n+rp, 1n+bp, C.pow2(w), hrl, hb))
580      +hab = N.lt_le_trans(Nat.mul(1n+bp, 1n+rp), Nat.mul(C.pow2(w), C.pow2(w)), C.pow2(139n), hsq, N.le_trans(Nat.mul(C.pow2(w), C.pow2(w)), C.pow2(Nat.add(w, w)), C.pow2(139n), N.eq_le(Nat.mul(C.pow2(w), C.pow2(w)), C.pow2(Nat.add(w, w)), Equal.sym(Nat, C.pow2(Nat.add(w, w)), Nat.mul(C.pow2(w), C.pow2(w)), RT.pow2_add(w, w))), N.pow2_mono(Nat.add(w, w), 139n, hw)))
581      +hb140 = N.lt_le_trans(1n+bp, C.pow2(w), C.pow2(140n), hb, N.pow2_mono(w, 140n, hw140))
582      +t = tw(140n, 1n+bp, 1n+rp, 0n, {==}, {==}, hb140, {==}, hab)
583      +e2 = Equal.trans(Nat, M.gcd(1n+bp, 1n+rp), M.gcd(1n+bp, Nat.mod(a, 1n+bp)), M.gcd(a, 1n+bp), Equal.cong(Nat, Nat, t => M.gcd(1n+bp, t), 1n+rp, Nat.mod(a, 1n+bp), Equal.sym(Nat, Nat.mod(a, 1n+bp), 1n+rp, hr)), Equal.sym(Nat, M.gcd(a, 1n+bp), M.gcd(1n+bp, Nat.mod(a, 1n+bp)), gcd_rec(a, bp)))
584      %Equal.sym(Nat, Nat.mod(a, 1n+bp), 1n+rp, hr) : {nbg_b(1n+bp, _, iz(_)) == M.gcd(a, 1n+bp) : Nat}
585      Equal.trans(Nat, ntw(140n, 1n+bp, 1n+rp, 0n, nev2(1n+bp, 1n+rp)), M.gcd(1n+bp, 1n+rp), M.gcd(a, 1n+bp), t, e2)