matita/matita/lib/reverse_complexity/almost.ma

   1 include "reverse_complexity/speedup.ma".
   2
   3 definition aes : (nat → nat) → (nat → nat) → Prop ≝ λf,g.
   4   ∃n.∀m. n ≤ m → f m = g m.
   5
   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
   8 elim n
   9   [#g #CFg #H @(ext_CF … g) [#m @H // |//]
  10   |#i #Hind #g #CFg #H
  11    @(Hind (λx. if eqb i x then f i else g x))
  12     [@CF_if
  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
  15       |@CFg
  16       ]
  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 //
  21       ]
  22     ]
  23   ]
  24 qed.