def tw_case

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

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/typed/natfuel.bend as NF
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR

545def tw_case(+g: Nat, +a: Nat, +b: Nat, +c: Nat, +ha0: {Nat.is_lt(0n, a) == True{} : Bool}, +hb0: {Nat.is_lt(0n, b) == True{} : Bool}, +haf: {Nat.is_lt(a, C.pow2(1n+g)) == True{} : Bool}, +hf: {Nat.is_le(1n+g, 140n) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), C.pow2(139n)) == True{} : Bool}, ih: @+a2: Nat -> @+b2: Nat -> @+c2: Nat -> @+ha2: {Nat.is_lt(0n, a2) == True{} : Bool} -> @+hb2: {Nat.is_lt(0n, b2) == True{} : Bool} -> @+haf2: {Nat.is_lt(a2, C.pow2(g)) == True{} : Bool} -> @+hab2: {Nat.is_lt(Nat.mul(a2, b2), C.pow2(139n)) == True{} : Bool} -> {ntw(g, a2, b2, c2, nev2(a2, b2)) == ndbl(c2, M.gcd(a2, b2)) : Nat}, +ev: Bool, +hev: {nev2(a, b) == ev : Bool}) -> {ntw(1n+g, a, b, c, ev) == ndbl(c, M.gcd(a, b)) : Nat}:
546  match ev:
547    case True{}:
548      +ea = even_form(a, not_odd(a, ev_ta(odd(a), odd(b), hev)))
549      +eb = even_form(b, not_odd(b, ev_tb(odd(a), odd(b), hev)))
550      +ha2 = half_pos(a, ha0, ea, Nat.div(a, 2n), {==})
551      +hb2 = half_pos(b, hb0, eb, Nat.div(b, 2n), {==})
552      +haf2 = double_lt_inv(Nat.div(a, 2n), C.pow2(g), Equal.trans(Bool, Nat.is_lt(Nat.double(Nat.div(a, 2n)), Nat.double(C.pow2(g))), Nat.is_lt(a, Nat.double(C.pow2(g))), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, Nat.double(C.pow2(g))), Nat.double(Nat.div(a, 2n)), a, Equal.sym(Nat, a, Nat.double(Nat.div(a, 2n)), ea)), haf))
553      +hab2 = N.le_lt_trans(Nat.mul(Nat.div(a, 2n), Nat.div(b, 2n)), Nat.mul(a, b), C.pow2(139n), N.le_trans(Nat.mul(Nat.div(a, 2n), Nat.div(b, 2n)), Nat.mul(a, Nat.div(b, 2n)), Nat.mul(a, b), AR.mul_le(Nat.div(a, 2n), a, Nat.div(b, 2n), div2_le(a)), NF.mul_le_r(a, Nat.div(b, 2n), b, div2_le(b))), hab)
554      +r = ih(Nat.div(a, 2n), Nat.div(b, 2n), 1n+c, ha2, hb2, haf2, hab2)
555      Equal.trans(Nat, ntw(g, Nat.div(a, 2n), Nat.div(b, 2n), 1n+c, nev2(Nat.div(a, 2n), Nat.div(b, 2n))), ndbl(c, Nat.add(M.gcd(Nat.div(a, 2n), Nat.div(b, 2n)), M.gcd(Nat.div(a, 2n), Nat.div(b, 2n)))), ndbl(c, M.gcd(a, b)), r, Equal.cong(Nat, Nat, t => ndbl(c, t), Nat.add(M.gcd(Nat.div(a, 2n), Nat.div(b, 2n)), M.gcd(Nat.div(a, 2n), Nat.div(b, 2n))), M.gcd(a, b), Equal.sym(Nat, M.gcd(a, b), Nat.add(M.gcd(Nat.div(a, 2n), Nat.div(b, 2n)), M.gcd(Nat.div(a, 2n), Nat.div(b, 2n))), gcd_twice(a, b, ea, eb))))
556    case False{}:
557      +ha140 = N.lt_le_trans(a, C.pow2(1n+g), C.pow2(140n), haf, N.pow2_mono(1n+g, 140n, hf))
558      Equal.cong(Nat, Nat, t => ndbl(c, t), nbloop(140n, nstrip(a), b, iz(b), nsm(nstrip(a), b)), M.gcd(a, b), tw_exit(a, b, ha0, ha140, hab, hev, hb0, b, {==}))