def inv_fuel

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:227

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

227def inv_fuel(+f1: Nat, +f2: Nat, +m: Nat, +r0: Nat, +s0: Nat, +r1: Nat, +s1: Nat, +h1: {ends(f1, r0, r1) == True{} : Bool}, +h2: {ends(f2, r0, r1) == True{} : Bool}) -> {M.inv_go(f1, m, r0, s0, r1, s1) == M.inv_go(f2, m, r0, s0, r1, s1) : M.Bezout}:
228  match f1 f2 r1:
229    case 0n _ 0n:
230      Equal.sym(M.Bezout, M.inv_go(f2, m, r0, s0, 0n, s1), M.BZ{r0, s0}, iv_zero(f2, m, r0, s0, s1))
231    case 0n _ 1n+rp:
232      Empty.absurd({M.inv_go(0n, m, r0, s0, 1n+rp, s1) == M.inv_go(f2, m, r0, s0, 1n+rp, s1) : M.Bezout}, true_ne_false(Equal.sym(Bool, False{}, True{}, h1)))
233    case 1n+g1 _ 0n:
234      Equal.sym(M.Bezout, M.inv_go(f2, m, r0, s0, 0n, s1), M.BZ{r0, s0}, iv_zero(f2, m, r0, s0, s1))
235    case 1n+g1 0n 1n+rp:
236      Empty.absurd({M.inv_go(1n+g1, m, r0, s0, 1n+rp, s1) == M.inv_go(0n, m, r0, s0, 1n+rp, s1) : M.Bezout}, true_ne_false(Equal.sym(Bool, False{}, True{}, h2)))
237    case 1n+ +g1 1n+ +g2 1n+ +rp:
238      inv_fuel(g1, g2, m, 1n+rp, s1, Nat.mod(r0, 1n+rp), M.inv_step(m, Nat.div(r0, 1n+rp), s0, s1), h1, h2)