X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Freverse_complexity%2Falmost.ma;fp=matita%2Fmatita%2Flib%2Freverse_complexity%2Falmost.ma;h=75578d0f91d584ada1d123a98f88fe55506dcd72;hb=600fba840c748f67593838673a6eb40eab9b68e5;hp=0000000000000000000000000000000000000000;hpb=b4f76b0d8fa0e5365fb48e91474febe200b647a7;p=helm.git

diff --git a/matita/matita/lib/reverse_complexity/almost.ma b/matita/matita/lib/reverse_complexity/almost.ma
new file mode 100644
index 000000000..75578d0f9
--- /dev/null
+++ b/matita/matita/lib/reverse_complexity/almost.ma
@@ -0,0 +1,24 @@
+include "reverse_complexity/speedup.ma".
+
+definition aes : (nat → nat) → (nat → nat) → Prop ≝ λf,g.
+  ∃n.∀m. n ≤ m → f m = g m.
+
+lemma CF_almost: ∀f,g,s. CF s g → aes g f → CF s f.
+#f #g #s #CFg * #n lapply CFg -CFg lapply g -g
+elim n 
+  [#g #CFg #H @(ext_CF … g) [#m @H // |//]
+  |#i #Hind #g #CFg #H
+   @(Hind (λx. if eqb i x then f i else g x))
+    [@CF_if 
+      [@(O_to_CF … MSC) [@le_to_O @(MSC_in … CFg)] @CF_eqb //
+      |@(O_to_CF … MSC) [@le_to_O @(MSC_in … CFg)] @CF_const
+      |@CFg
+      ]
+    |#m #leim cases (le_to_or_lt_eq … leim)
+      [#ltim lapply (lt_to_not_eq … ltim) #noteqim 
+       >(not_eq_to_eqb_false … noteqim) @H @ltim
+      |#eqim >eqim >eqb_n_n //
+      ]
+    ]
+  ]
+qed.
\ No newline at end of file