def bf_case

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

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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH

454def bf_case(+a: Nat, +ha: {Nat.mod(a, 2n) == 1n : Nat}, +bp: Nat, +hab: {Nat.is_lt(Nat.mul(a, 1n+bp), C.pow2(139n)) == True{} : Bool}, +hs: {Nat.mod(nstrip(1n+bp), 2n) == 1n : Nat}, +hga: {M.gcd(a, 1n+bp) == M.gcd(a, nstrip(1n+bp)) : Nat}, +hsa: {Nat.is_le(Nat.mul(a, nstrip(1n+bp)), Nat.mul(a, 1n+bp)) == True{} : Bool}, +lb: Bool, +hl: {Nat.is_lt(nstrip(1n+bp), a) == lb : Bool}) -> {nbloop(139n, nba(a, nstrip(1n+bp), lb), nbd(a, nstrip(1n+bp), lb), iz(nbd(a, nstrip(1n+bp), lb)), nsm(nba(a, nstrip(1n+bp), lb), nbd(a, nstrip(1n+bp), lb))) == M.gcd(a, 1n+bp) : Nat}:
455  match lb:
456    case True{}:
457      +sle = N.lt_le(nstrip(1n+bp), a, hl)
458      +le1 = N.le_trans(Nat.mul(nstrip(1n+bp), Nat.sub(a, nstrip(1n+bp))), Nat.mul(nstrip(1n+bp), a), Nat.mul(a, 1n+bp), NF.mul_le_r(nstrip(1n+bp), Nat.sub(a, nstrip(1n+bp)), a, UH.sub_le(a, nstrip(1n+bp))), N.le_trans(Nat.mul(nstrip(1n+bp), a), Nat.mul(a, nstrip(1n+bp)), Nat.mul(a, 1n+bp), N.eq_le(Nat.mul(nstrip(1n+bp), a), Nat.mul(a, nstrip(1n+bp)), NA.mul_comm(nstrip(1n+bp), a)), hsa))
459      +hDs = Equal.sym(Nat, Nat.sub(a, nstrip(1n+bp)), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(1n+bp), 2n))), odd_sub(a, ha, nstrip(1n+bp), hs))
460      +hb2 = Equal.trans(Bool, Nat.is_lt(Nat.mul(nstrip(1n+bp), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(1n+bp), 2n)))), C.pow2(139n)), Nat.is_lt(Nat.mul(nstrip(1n+bp), Nat.sub(a, nstrip(1n+bp))), C.pow2(139n)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(Nat.mul(nstrip(1n+bp), t), C.pow2(139n)), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(1n+bp), 2n))), Nat.sub(a, nstrip(1n+bp)), hDs), N.le_lt_trans(Nat.mul(nstrip(1n+bp), Nat.sub(a, nstrip(1n+bp))), Nat.mul(a, 1n+bp), C.pow2(139n), le1, hab))
461      +r = bl(139n, nstrip(1n+bp), hs, Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(1n+bp), 2n)), hb2, {==})
462      %hDs : {nbloop(139n, nstrip(1n+bp), _, iz(_), nsm(nstrip(1n+bp), _)) == M.gcd(a, 1n+bp) : Nat}
463      Equal.trans(Nat, nbloop(139n, nstrip(1n+bp), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(1n+bp), 2n))), iz(Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(1n+bp), 2n)))), nsm(nstrip(1n+bp), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(1n+bp), 2n))))), M.gcd(nstrip(1n+bp), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(1n+bp), 2n)))), M.gcd(a, 1n+bp), r, Equal.trans(Nat, M.gcd(nstrip(1n+bp), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(1n+bp), 2n)))), M.gcd(nstrip(1n+bp), Nat.sub(a, nstrip(1n+bp))), M.gcd(a, 1n+bp), Equal.cong(Nat, Nat, t => M.gcd(nstrip(1n+bp), t), Nat.double(Nat.sub(Nat.div(a, 2n), Nat.div(nstrip(1n+bp), 2n))), Nat.sub(a, nstrip(1n+bp)), hDs), Equal.trans(Nat, M.gcd(nstrip(1n+bp), Nat.sub(a, nstrip(1n+bp))), M.gcd(nstrip(1n+bp), a), M.gcd(a, 1n+bp), Equal.sym(Nat, M.gcd(nstrip(1n+bp), a), M.gcd(nstrip(1n+bp), Nat.sub(a, nstrip(1n+bp))), gcd_sub(nstrip(1n+bp), a, sle)), Equal.trans(Nat, M.gcd(nstrip(1n+bp), a), M.gcd(a, nstrip(1n+bp)), M.gcd(a, 1n+bp), gcd_comm(nstrip(1n+bp), a), Equal.sym(Nat, M.gcd(a, 1n+bp), M.gcd(a, nstrip(1n+bp)), hga)))))
464    case False{}:
465      +ale = N.not_lt_le(nstrip(1n+bp), a, hl)
466      +le1 = N.le_trans(Nat.mul(a, Nat.sub(nstrip(1n+bp), a)), Nat.mul(a, nstrip(1n+bp)), Nat.mul(a, 1n+bp), NF.mul_le_r(a, Nat.sub(nstrip(1n+bp), a), nstrip(1n+bp), UH.sub_le(nstrip(1n+bp), a)), hsa)
467      +hDs = Equal.sym(Nat, Nat.sub(nstrip(1n+bp), a), Nat.double(Nat.sub(Nat.div(nstrip(1n+bp), 2n), Nat.div(a, 2n))), odd_sub(nstrip(1n+bp), hs, a, ha))
468      +hb2 = Equal.trans(Bool, Nat.is_lt(Nat.mul(a, Nat.double(Nat.sub(Nat.div(nstrip(1n+bp), 2n), Nat.div(a, 2n)))), C.pow2(139n)), Nat.is_lt(Nat.mul(a, Nat.sub(nstrip(1n+bp), a)), C.pow2(139n)), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(Nat.mul(a, t), C.pow2(139n)), Nat.double(Nat.sub(Nat.div(nstrip(1n+bp), 2n), Nat.div(a, 2n))), Nat.sub(nstrip(1n+bp), a), hDs), N.le_lt_trans(Nat.mul(a, Nat.sub(nstrip(1n+bp), a)), Nat.mul(a, 1n+bp), C.pow2(139n), le1, hab))
469      +r = bl(139n, a, ha, Nat.sub(Nat.div(nstrip(1n+bp), 2n), Nat.div(a, 2n)), hb2, {==})
470      %hDs : {nbloop(139n, a, _, iz(_), nsm(a, _)) == M.gcd(a, 1n+bp) : Nat}
471      Equal.trans(Nat, nbloop(139n, a, Nat.double(Nat.sub(Nat.div(nstrip(1n+bp), 2n), Nat.div(a, 2n))), iz(Nat.double(Nat.sub(Nat.div(nstrip(1n+bp), 2n), Nat.div(a, 2n)))), nsm(a, Nat.double(Nat.sub(Nat.div(nstrip(1n+bp), 2n), Nat.div(a, 2n))))), M.gcd(a, Nat.double(Nat.sub(Nat.div(nstrip(1n+bp), 2n), Nat.div(a, 2n)))), M.gcd(a, 1n+bp), r, Equal.trans(Nat, M.gcd(a, Nat.double(Nat.sub(Nat.div(nstrip(1n+bp), 2n), Nat.div(a, 2n)))), M.gcd(a, Nat.sub(nstrip(1n+bp), a)), M.gcd(a, 1n+bp), Equal.cong(Nat, Nat, t => M.gcd(a, t), Nat.double(Nat.sub(Nat.div(nstrip(1n+bp), 2n), Nat.div(a, 2n))), Nat.sub(nstrip(1n+bp), a), hDs), Equal.trans(Nat, M.gcd(a, Nat.sub(nstrip(1n+bp), a)), M.gcd(a, nstrip(1n+bp)), M.gcd(a, 1n+bp), Equal.sym(Nat, M.gcd(a, nstrip(1n+bp)), M.gcd(a, Nat.sub(nstrip(1n+bp), a)), gcd_sub(a, nstrip(1n+bp), ale)), Equal.sym(Nat, M.gcd(a, 1n+bp), M.gcd(a, nstrip(1n+bp)), hga))))