1 include "reverse_complexity/speedup.ma".
3 definition aes : (nat → nat) → (nat → nat) → Prop ≝ λf,g.
4 ∃n.∀m. n ≤ m → f m = g m.
6 lemma CF_almost: ∀f,g,s. CF s g → aes g f → CF s f.
7 #f #g #s #CFg * #n lapply CFg -CFg lapply g -g
9 [#g #CFg #H @(ext_CF … g) [#m @H // |//]
11 @(Hind (λx. if eqb i x then f i else g x))
13 [@(O_to_CF … MSC) [@le_to_O @(MSC_in … CFg)] @CF_eqb //
14 |@(O_to_CF … MSC) [@le_to_O @(MSC_in … CFg)] @CF_const
17 |#m #leim cases (le_to_or_lt_eq … leim)
18 [#ltim lapply (lt_to_not_eq … ltim) #noteqim
19 >(not_eq_to_eqb_false … noteqim) @H @ltim
20 |#eqim >eqim >eqb_n_n //