def gcd_fuel

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

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

57def gcd_fuel(+f1: Nat, +f2: Nat, +a: Nat, +b: Nat, +h1: {ends(f1, a, b) == True{} : Bool}, +h2: {ends(f2, a, b) == True{} : Bool}) -> {M.gcd_go(f1, a, b) == M.gcd_go(f2, a, b) : Nat}:
58  match f1 f2 b:
59    case 0n _ 0n:
60      Equal.sym(Nat, M.gcd_go(f2, a, 0n), a, gz(f2, a))
61    case 0n _ 1n+bp:
62      Empty.absurd({M.gcd_go(0n, a, 1n+bp) == M.gcd_go(f2, a, 1n+bp) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, h1)))
63    case 1n+g1 _ 0n:
64      Equal.sym(Nat, M.gcd_go(f2, a, 0n), a, gz(f2, a))
65    case 1n+g1 0n 1n+bp:
66      Empty.absurd({M.gcd_go(1n+g1, a, 1n+bp) == M.gcd_go(0n, a, 1n+bp) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, h2)))
67    case 1n+ +g1 1n+ +g2 1n+ +bp:
68      gcd_fuel(g1, g2, 1n+bp, Nat.mod(a, 1n+bp), h1, h2)