def bends_bound

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

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/proofs/lib/nat.bend as N

153# n < 2^j and j <= f: f halvings reach 0
154def bends_bound(+j: Nat, +f: Nat, +n: Nat, +hn: {Nat.is_lt(n, C.pow2(j)) == True{} : Bool}, +hf: {Nat.is_le(j, f) == True{} : Bool}) -> {bends(f, n) == True{} : Bool}:
155  match j f n:
156    case _ _ 0n:
157      bends_zero(f)
158    case 0n _ 1n+np:
159      Empty.absurd({bends(f, 1n+np) == True{} : Bool}, N.lt_zero_absurd(np, hn))
160    case 1n+i 0n 1n+np:
161      Empty.absurd({bends(0n, 1n+np) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, hf)))
162    case 1n+ +i 1n+ +g 1n+ +np:
163      bends_bound(i, g, Nat.div(1n+np, 2n), half_below(1n+np, C.pow2(i), hn), hf)