def bl_fuel

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

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

182def bl_fuel(+f1: Nat, +f2: Nat, +n: Nat, +k: Nat, +h1: {bends(f1, n) == True{} : Bool}, +h2: {bends(f2, n) == True{} : Bool}) -> {M.bit_length_go(f1, n, k) == M.bit_length_go(f2, n, k) : Nat}:
183  match f1 f2 n:
184    case _ _ 0n:
185      Equal.trans(Nat, M.bit_length_go(f1, 0n, k), k, M.bit_length_go(f2, 0n, k), bl_zero(f1, k), Equal.sym(Nat, M.bit_length_go(f2, 0n, k), k, bl_zero(f2, k)))
186    case 0n _ 1n+np:
187      Empty.absurd({M.bit_length_go(0n, 1n+np, k) == M.bit_length_go(f2, 1n+np, k) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, h1)))
188    case 1n+g1 0n 1n+np:
189      Empty.absurd({M.bit_length_go(1n+g1, 1n+np, k) == M.bit_length_go(0n, 1n+np, k) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, h2)))
190    case 1n+ +g1 1n+ +g2 1n+ +np:
191      bl_fuel(g1, g2, Nat.div(1n+np, 2n), 1n+k, h1, h2)