def il_fuel

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

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

290def il_fuel(+f1: Nat, +f2: Nat, +n: Nat, +b: Nat, +k: Nat, +p: Nat, +up: Bool, +h1: {ilends(f1, Nat.div(n, b), b, p, up) == True{} : Bool}, +h2: {ilends(f2, Nat.div(n, b), b, p, up) == True{} : Bool}) -> {M.ilog_go(f1, n, b, k, p, up) == M.ilog_go(f2, n, b, k, p, up) : Nat}:
291  match f1 f2 up:
292    case 0n _ False{}:
293      Equal.sym(Nat, M.ilog_go(f2, n, b, k, p, False{}), k, ilz(f2, n, b, k, p))
294    case 0n _ True{}:
295      Empty.absurd({M.ilog_go(0n, n, b, k, p, True{}) == M.ilog_go(f2, n, b, k, p, True{}) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, h1)))
296    case 1n+g1 _ False{}:
297      Equal.sym(Nat, M.ilog_go(f2, n, b, k, p, False{}), k, ilz(f2, n, b, k, p))
298    case 1n+g1 0n True{}:
299      Empty.absurd({M.ilog_go(1n+g1, n, b, k, p, True{}) == M.ilog_go(0n, n, b, k, p, True{}) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, h2)))
300    case 1n+ +g1 1n+ +g2 True{}:
301      il_fuel(g1, g2, n, b, 1n+k, Nat.mul(p, b), Nat.is_le(Nat.mul(p, b), Nat.div(n, b)), h1, h2)