X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2FReverse_complexity%2Freverse.ma;fp=weblib%2FReverse_complexity%2Freverse.ma;h=c99de03c5a869581686e53474efdcca41b1d83fd;hb=adfe42bbd5aaa4130a4133f345930e79444f0f3e;hp=73814b17ac4c5153dc3c341cf5cbafc01a1194ad;hpb=4672640dc168a3adcbea86887c38d895358288e8;p=helm.git

diff --git a/weblib/Reverse_complexity/reverse.ma b/weblib/Reverse_complexity/reverse.ma
index 73814b17a..c99de03c5 100644
--- a/weblib/Reverse_complexity/reverse.ma
+++ b/weblib/Reverse_complexity/reverse.ma
@@ -6,11 +6,11 @@ include "arithmetics/bigO.ma".
  
 (*********************************** pairing **********************************) 
 
-axiom pair: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
-axiom fst : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
-axiom snd : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
-axiom fst_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a.
-axiom snd_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/snd.dec"snd/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b. 
+img class="anchor" src="icons/tick.png" id="pair"axiom pair: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="fst"axiom fst : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="snd"axiom snd : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="fst_pair"axiom fst_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a.
+img class="anchor" src="icons/tick.png" id="snd_pair"axiom snd_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/snd.dec"snd/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b. 
 
 interpretation "abstract pair" 'pair f g = (pair f g).
 
@@ -19,10 +19,10 @@ interpretation "abstract pair" 'pair f g = (pair f g).
 (* u is the deterministic configuration relation of the universal machine (one 
    step) *)
 
-axiom u: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="u"axiom u: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
 
-let rec U c n on n ≝ 
-  match n with  
+img class="anchor" src="icons/tick.png" id="U"let rec U c n on n ≝ 
+  match n in nat with  
   [ O ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
   | S m ⇒ match a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a c with 
     [ None ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? c (* halting case *)
@@ -30,12 +30,12 @@ let rec U c n on n ≝
     ]
   ].
  
-lemma halt_U: ∀i,n,y. a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a i.
+img class="anchor" src="icons/tick.png" id="halt_U"lemma halt_U: ∀i,n,y. a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a i.
 #i #n #y #H cases n
   [normalize #H1 destruct |#m normalize >H normalize #H1 destruct //]
 qed. 
 
-lemma Some_to_halt: ∀n,i,y. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? .
+img class="anchor" src="icons/tick.png" id="Some_to_halt"lemma Some_to_halt: ∀n,i,y. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? .
 #n elim n
   [#i #y normalize #H destruct (H)
   |#m #Hind #i #y normalize 
@@ -45,7 +45,7 @@ lemma Some_to_halt: ∀n,i,y. a href="cic:/matita/Reverse_complexity/reverse/U.
   ]
 qed. 
 
-lemma monotonici_U: ∀y,n,m,i.
+img class="anchor" src="icons/tick.png" id="monotonici_U"lemma monotonici_U: ∀y,n,m,i.
   a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i (na title="natural plus" href="cic:/fakeuri.def(1)"+/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
 #y #n #m elim m 
   [#i normalize #H destruct 
@@ -56,7 +56,7 @@ lemma monotonici_U: ∀y,n,m,i.
   ]
 qed.
 
-lemma monotonic_U: ∀i,n,m,y.n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am →
+img class="anchor" src="icons/tick.png" id="monotonic_U"lemma monotonic_U: ∀i,n,m,y.n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am →
   a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
 #i #n #m #y #lenm #H >(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a m n) // @a href="cic:/matita/Reverse_complexity/reverse/monotonici_U.def(5)"monotonici_U/a //
 qed.
@@ -65,7 +65,7 @@ qed.
 (* axiom monotonic_U: ∀i,n,m,y.n ≤m →
    U i n = Some ? y → U i m = Some ? y. *)
   
-lemma unique_U: ∀i,n,m,yn,ym.
+img class="anchor" src="icons/tick.png" id="unique_U"lemma unique_U: ∀i,n,m,yn,ym.
   a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? yn → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? ym → yn a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ym.
 #i #n #m #yn #ym #Hn #Hm cases (a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a n m)
   [#lenm lapply (a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … lenm Hn) >Hm #HS destruct (HS) //
@@ -74,16 +74,16 @@ lemma unique_U: ∀i,n,m,yn,ym.
   ]
 qed.
 
-definition code_for ≝ λf,i.∀x.
+img class="anchor" src="icons/tick.png" id="code_for"definition code_for ≝ λf,i.∀x.
   a title="exists" href="cic:/fakeuri.def(1)"∃/an.∀m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x.
 
-definition terminate ≝ λc,r. a title="exists" href="cic:/fakeuri.def(1)"∃/ay. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a c r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
+img class="anchor" src="icons/tick.png" id="terminate"definition terminate ≝ λc,r. a title="exists" href="cic:/fakeuri.def(1)"∃/ay. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a c r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
 
 interpretation "termination" 'fintersects c r = (terminate c r).
  
-definition lang ≝ λi,x.a title="exists" href="cic:/fakeuri.def(1)"∃/ar,ya title="exists" href="cic:/fakeuri.def(1)"./a a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a  a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y. 
+img class="anchor" src="icons/tick.png" id="lang"definition lang ≝ λi,x.a title="exists" href="cic:/fakeuri.def(1)"∃/ar,ya title="exists" href="cic:/fakeuri.def(1)"./a a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a  a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y. 
 
-lemma lang_cf :∀f,i,x. a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"code_for/a f i → 
+img class="anchor" src="icons/tick.png" id="lang_cf"lemma lang_cf :∀f,i,x. a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"code_for/a f i → 
   a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"lang/a i x a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="exists" href="cic:/fakeuri.def(1)"∃/ay.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y.
 #f #i #x normalize #H %
   [* #n * #y * #H1 #posy %{y} % // 
@@ -95,175 +95,173 @@ qed.
 
 (******************************* complexity classes ***************************)
 
-axiom size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
-axiom of_size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="size"axiom size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="of_size"axiom of_size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
 
 interpretation "size" 'card n = (size n).
 
-axiom size_of_size: ∀n. |a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
-axiom of_size_max: ∀i,n. |ia title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n.
+img class="anchor" src="icons/tick.png" id="size_of_size"axiom size_of_size: ∀n. |a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
+img class="anchor" src="icons/tick.png" id="of_size_max"axiom of_size_max: ∀i,n. |ia title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n.
 
-axiom size_fst : ∀n. |a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |na title="size" href="cic:/fakeuri.def(1)"|/a.
+img class="anchor" src="icons/tick.png" id="size_fst"axiom size_fst : ∀n. |a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |na title="size" href="cic:/fakeuri.def(1)"|/a.
 
-axiom a : Max0.
+img class="anchor" src="icons/tick.png" id="size_f"definition size_f ≝ λf,n.Max_{ifont class="Apple-style-span" color="#FF0000" < /fonta href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n) | a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a (|ia title="size" href="cic:/fakeuri.def(1)"|/a) n a title="bigop" href="cic:/fakeuri.def(1)"}/a|(f i)a title="size" href="cic:/fakeuri.def(1)"|/a.
 
-definition size_f ≝ λf,n.Max_{ifont class="Apple-style-span" color="#FF0000" < /fontS (of_size n) | eqb (|i|) n }|(f i)|.
-
-lemma size_f_def: ∀f,n. size_f f n = 
-  Max_{i < S (of_size n) | eqb (|i|) n}|(f i)|.
+img class="anchor" src="icons/tick.png" id="size_f_def"lemma size_f_def: ∀f,n. a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a f n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  Max_{i < a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n) | a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a (|ia title="size" href="cic:/fakeuri.def(1)"|/a) na title="bigop" href="cic:/fakeuri.def(1)"}/a|(f i)a title="size" href="cic:/fakeuri.def(1)"|/a.
 // qed.
 
-lemma size_f_size : ∀f,n. size_f (f ∘ size) n = |(f n)|.
-#f #n @le_to_le_to_eq
-  [@Max_le #a #lta #Ha normalize >(eqb_true_to_eq  … Ha) //
-  |<(size_of_size n) in ⊢ (?%?); >size_f_def
-   @(le_Max (λi.|f (|i|)|) ? (S (of_size n)) (of_size n) ??)
-    [@le_S_S // | @eq_to_eqb_true //]
+img class="anchor" src="icons/tick.png" id="size_f_size"lemma size_f_size : ∀f,n. a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a (f a title="function composition" href="cic:/fakeuri.def(1)"∘/a a href="cic:/matita/Reverse_complexity/reverse/size.dec"size/a) n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |(f n)a title="size" href="cic:/fakeuri.def(1)"|/a.
+#f #n @a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"le_to_le_to_eq/a
+  [@a href="cic:/matita/arithmetics/min_max/Max_le.def(9)"Max_le/a #a #lta #Ha normalize >(a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"eqb_true_to_eq/a  … Ha) //
+  |<(a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"size_of_size/a n) in ⊢ (?%?); >a href="cic:/matita/Reverse_complexity/reverse/size_f_def.def(4)"size_f_def/a
+   @(a href="cic:/matita/arithmetics/min_max/le_Max.def(12)"le_Max/a (λi.|f (|ia title="size" href="cic:/fakeuri.def(1)"|/a)a title="size" href="cic:/fakeuri.def(1)"|/a) ? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n)) (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n) ??)
+    [@a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a // | @a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"eq_to_eqb_true/a //]
   ]
 qed.
 
-lemma size_f_id : ∀n. size_f (λx.x) n = n.
-#n @le_to_le_to_eq
-  [@Max_le #a #lta #Ha >(eqb_true_to_eq  … Ha) //
-  |<(size_of_size n) in ⊢ (?%?); >size_f_def
-   @(le_Max (λi.|i|) ? (S (of_size n)) (of_size n) ??)
-    [@le_S_S // | @eq_to_eqb_true //]
+img class="anchor" src="icons/tick.png" id="size_f_id"lemma size_f_id : ∀n. a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a (λx.x) n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
+#n @a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"le_to_le_to_eq/a
+  [@a href="cic:/matita/arithmetics/min_max/Max_le.def(9)"Max_le/a #a #lta #Ha >(a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"eqb_true_to_eq/a  … Ha) //
+  |<(a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"size_of_size/a n) in ⊢ (?%?); >a href="cic:/matita/Reverse_complexity/reverse/size_f_def.def(4)"size_f_def/a
+   @(a href="cic:/matita/arithmetics/min_max/le_Max.def(12)"le_Max/a (λi.|ia title="size" href="cic:/fakeuri.def(1)"|/a) ? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n)) (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n) ??)
+    [@a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a // | @a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"eq_to_eqb_true/a //]
   ]
 qed.
 
-lemma size_f_fst : ∀n. size_f fst n ≤ n.
-#n @Max_le #a #lta #Ha <(eqb_true_to_eq  … Ha) //
+img class="anchor" src="icons/tick.png" id="size_f_fst"lemma size_f_fst : ∀n. a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n.
+#n @a href="cic:/matita/arithmetics/min_max/Max_le.def(9)"Max_le/a #a #lta #Ha <(a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"eqb_true_to_eq/a  … Ha) //
 qed.
 
 (* definition def ≝ λf:nat → option nat.λx.∃y. f x = Some ? y.*)
 
 (* C s i means that the complexity of i is O(s) *)
 
-definition C ≝ λs,i.∃c.∃a.∀x.a ≤ |x| → ∃y. 
-  U 〈i,x〉 (c*(s(|x|))) = Some ? y.
+img class="anchor" src="icons/tick.png" id="C"definition C ≝ λs,i.a title="exists" href="cic:/fakeuri.def(1)"∃/ac.a title="exists" href="cic:/fakeuri.def(1)"∃/aa.∀x.a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |xa title="size" href="cic:/fakeuri.def(1)"|/a → a title="exists" href="cic:/fakeuri.def(1)"∃/ay. 
+  a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a (ca title="natural times" href="cic:/fakeuri.def(1)"*/a(s(|xa title="size" href="cic:/fakeuri.def(1)"|/a))) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
 
-definition CF ≝ λs,f.∃i.code_for f i ∧ C s i.
+img class="anchor" src="icons/tick.png" id="CF"definition CF ≝ λs,f.a title="exists" href="cic:/fakeuri.def(1)"∃/ai.a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"code_for/a f i a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/Reverse_complexity/reverse/C.def(3)"C/a s i.
 
-lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
+img class="anchor" src="icons/tick.png" id="ext_CF"lemma ext_CF : ∀f,g,s. (∀n. f n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g n) → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s f → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s g.
 #f #g #s #Hext * #i * #Hcode #HC %{i} %
   [#x cases (Hcode x) #a #H %{a} <Hext @H | //] 
 qed. 
 
-lemma monotonic_CF: ∀s1,s2,f. O s2 s1 → CF s1 f → CF s2 f.
+img class="anchor" src="icons/tick.png" id="monotonic_CF"lemma monotonic_CF: ∀s1,s2,f. a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a s2 s1 → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s1 f → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s2 f.
 #s1 #s2 #f * #c1 * #a #H * #i * #Hcodef #HCs1 %{i} % //
-cases HCs1 #c2 * #b #H2 %{(c2*c1)} %{(max a b)} 
-#x #Hmax cases (H2 x ?) [2:@(le_maxr … Hmax)] #y #Hy
-%{y} @(monotonic_U …Hy) >associative_times @le_times // @H @(le_maxl … Hmax)
+cases HCs1 #c2 * #b #H2 %{(c2a title="natural times" href="cic:/fakeuri.def(1)"*/ac1)} %{(a href="cic:/matita/arithmetics/nat/max.def(2)"max/a a b)} 
+#x #Hmax cases (H2 x ?) [2:@(a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"le_maxr/a … Hmax)] #y #Hy
+%{y} @(a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a …Hy) >a href="cic:/matita/arithmetics/nat/associative_times.def(10)"associative_times/a @a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a // @H @(a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a … Hmax)
 qed. 
 
 (************************** The diagonal language *****************************)
 
 (* the diagonal language used for the hierarchy theorem *)
 
-definition diag ≝ λs,i. 
-  U 〈fst i,i〉 (s (|i|)) = Some ? 0. 
+img class="anchor" src="icons/tick.png" id="diag"definition diag ≝ λs,i. 
+  a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i,ia title="abstract pair" href="cic:/fakeuri.def(1)"〉/a (s (|ia title="size" href="cic:/fakeuri.def(1)"|/a)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? a title="natural number" href="cic:/fakeuri.def(1)"0/a. 
 
-lemma equiv_diag: ∀s,i. 
-  diag s i ↔ 〈fst i, i〉 ↓ s (|i|) ∧ ¬lang (fst i) i.
+img class="anchor" src="icons/tick.png" id="equiv_diag"lemma equiv_diag: ∀s,i. 
+  a href="cic:/matita/Reverse_complexity/reverse/diag.def(2)"diag/a s i a title="iff" href="cic:/fakeuri.def(1)"↔/a 〈a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i, ia title="abstract pair" href="cic:/fakeuri.def(1)"〉/a a title="termination" href="cic:/fakeuri.def(1)"↓/a s (|ia title="size" href="cic:/fakeuri.def(1)"|/a) a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="logical not" href="cic:/fakeuri.def(1)"¬/aa href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"lang/a (a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i) i.
 #s #i %
-  [whd in ⊢ (%→?); #H % [%{0} //] % * #x * #y *
-   #H1 #Hy cut (0 = y) [@(unique_U … H H1)] #eqy /2/
+  [whd in ⊢ (%→?); #H % [%{a title="natural number" href="cic:/fakeuri.def(1)"0/a} //] % * #x * #y *
+   #H1 #Hy cut (a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y) [@(a href="cic:/matita/Reverse_complexity/reverse/unique_U.def(9)"unique_U/a … H H1)] #eqy /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
   |* * #y cases y //
-   #y0 #H * #H1 @False_ind @H1 -H1 whd %{(s (|i|))} %{(S y0)} % //
+   #y0 #H * #H1 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @H1 -H1 whd %{(s (|ia title="size" href="cic:/fakeuri.def(1)"|/a))} %{(a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a y0)} % //
   ]
 qed.
 
 (* Let us define the characteristic function diag_cf for diag, and prove
 it correctness *)
 
-definition diag_cf ≝ λs,i.
-  match U 〈fst i,i〉 (s (|i|)) with
-  [ None ⇒ None ?
-  | Some y ⇒ if (eqb y 0) then (Some ? 1) else (Some ? 0)].
+img class="anchor" src="icons/tick.png" id="diag_cf"definition diag_cf ≝ λs,i.
+  match a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i,ia title="abstract pair" href="cic:/fakeuri.def(1)"〉/a (s (|ia title="size" href="cic:/fakeuri.def(1)"|/a)) with
+  [ None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
+  | Some y ⇒ if (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a y a title="natural number" href="cic:/fakeuri.def(1)"0/a) then (a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? a title="natural number" href="cic:/fakeuri.def(1)"1/a) else (a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? a title="natural number" href="cic:/fakeuri.def(1)"0/a)].
 
-lemma diag_cf_OK: ∀s,x. diag s x ↔ ∃y.diag_cf s x = Some ? y ∧ 0 < y.
+img class="anchor" src="icons/tick.png" id="diag_cf_OK"lemma diag_cf_OK: ∀s,x. a href="cic:/matita/Reverse_complexity/reverse/diag.def(2)"diag/a s x a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="exists" href="cic:/fakeuri.def(1)"∃/ay.a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"diag_cf/a s x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y.
 #s #x % 
-  [whd in ⊢ (%→?); #H %{1} % // whd in ⊢ (??%?); >H // 
+  [whd in ⊢ (%→?); #H %{a title="natural number" href="cic:/fakeuri.def(1)"1/a} % // whd in ⊢ (??%?); >H // 
   |* #y * whd in ⊢ (??%?→?→%); 
-   cases (U 〈fst x,x〉 (s (|x|))) normalize
+   cases (a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a x,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a (s (|xa title="size" href="cic:/fakeuri.def(1)"|/a))) normalize
     [#H destruct
-    |#x cases (true_or_false (eqb x 0)) #Hx >Hx 
-      [>(eqb_true_to_eq … Hx) // 
-      |normalize #H destruct #H @False_ind @(absurd ? H) @lt_to_not_le //  
+    |#x cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a x a title="natural number" href="cic:/fakeuri.def(1)"0/a)) #Hx >Hx 
+      [>(a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"eqb_true_to_eq/a … Hx) // 
+      |normalize #H destruct #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a ? H) @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a //  
       ]
     ]
   ]
 qed.
 
-lemma diag_spec: ∀s,i. code_for (diag_cf s) i → ∀x. lang i x ↔ diag s x.
-#s #i #Hcode #x @(iff_trans  … (lang_cf … Hcode)) @iff_sym @diag_cf_OK
+img class="anchor" src="icons/tick.png" id="diag_spec"lemma diag_spec: ∀s,i. a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"code_for/a (a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"diag_cf/a s) i → ∀x. a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"lang/a i x a title="iff" href="cic:/fakeuri.def(1)"↔/a a href="cic:/matita/Reverse_complexity/reverse/diag.def(2)"diag/a s x.
+#s #i #Hcode #x @(a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a  … (a href="cic:/matita/Reverse_complexity/reverse/lang_cf.def(10)"lang_cf/a … Hcode)) @a href="cic:/matita/basics/logic/iff_sym.def(2)"iff_sym/a @a href="cic:/matita/Reverse_complexity/reverse/diag_cf_OK.def(8)"diag_cf_OK/a
 qed. 
 
 (******************************************************************************)
 
-lemma absurd1: ∀P. iff P (¬ P) →False.
-#P * #H1 #H2 cut (¬P) [% #H2 @(absurd … H2) @H1 //] 
-#H3 @(absurd ?? H3) @H2 @H3 
+img class="anchor" src="icons/tick.png" id="absurd1"lemma absurd1: ∀P. a href="cic:/matita/basics/logic/iff.def(1)"iff/a P (a title="logical not" href="cic:/fakeuri.def(1)"¬/a P) →a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a.
+#P * #H1 #H2 cut (a title="logical not" href="cic:/fakeuri.def(1)"¬/aP) [% #H2 @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … H2) @H1 //] 
+#H3 @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a ?? H3) @H2 @H3 
 qed.
 
 (* axiom weak_pad : ∀a,∃a0.∀n. a0 < n → ∃b. |〈a,b〉| = n. *)
-axiom pad : ∀a,n. |a| < n → ∃b. |〈a,b〉| = n.
+img class="anchor" src="icons/tick.png" id="pad"axiom pad : ∀a,n. |aa title="size" href="cic:/fakeuri.def(1)"|/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a title="exists" href="cic:/fakeuri.def(1)"∃/ab. |〈a,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/aa title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
 
-lemma not_included_ex: ∀s1,s2. not_O s2 s1 → ∀i. C s2 i →
-  ∃b.〈i, 〈i,b〉〉 ↓ s1 (|〈i,b〉|).
+img class="anchor" src="icons/tick.png" id="not_included_ex"lemma not_included_ex: ∀s1,s2. a href="cic:/matita/arithmetics/bigO/not_O.def(3)"not_O/a s2 s1 → ∀i. a href="cic:/matita/Reverse_complexity/reverse/C.def(3)"C/a s2 i →
+  a title="exists" href="cic:/fakeuri.def(1)"∃/ab.〈i, 〈i,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/aa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a a title="termination" href="cic:/fakeuri.def(1)"↓/a s1 (|〈i,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/aa title="size" href="cic:/fakeuri.def(1)"|/a).
 #s1 #s2  #H #i * #c * #x0 #H1 
-cases (H c (max (S(|i|)) x0)) #x1 * #H2 #H3 cases (pad i x1 ?) 
+cases (H c (a href="cic:/matita/arithmetics/nat/max.def(2)"max/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a(|ia title="size" href="cic:/fakeuri.def(1)"|/a)) x0)) #x1 * #H2 #H3 cases (a href="cic:/matita/Reverse_complexity/reverse/pad.dec"pad/a i x1 ?) 
   [#b #H4 %{b}
-   cases (H1 〈i,b〉 ?)
-    [#z >H4 #H5 %{z} @(monotonic_U … H5) @lt_to_le //
-    |>H4 @(le_maxr … H2)
+   cases (H1 〈i,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/a ?)
+    [#z >H4 #H5 %{z} @(a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … H5) @a href="cic:/matita/arithmetics/nat/lt_to_le.def(6)"lt_to_le/a //
+    |>H4 @(a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"le_maxr/a … H2)
     ]
-  |@(le_maxl … H2)
+  |@(a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a … H2)
   ]
 qed.
 
-lemma diag1_not_s1: ∀s1,s2. not_O s2 s1 → ¬ CF s2 (diag_cf s1).
+img class="anchor" src="icons/tick.png" id="diag1_not_s1"lemma diag1_not_s1: ∀s1,s2. a href="cic:/matita/arithmetics/bigO/not_O.def(3)"not_O/a s2 s1 → a title="logical not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s2 (a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"diag_cf/a s1).
 #s1 #s2 #H1 % * #i * #Hcode_i #Hs2_i 
-cases (not_included_ex  … H1 ? Hs2_i) #b #H2
-lapply (diag_spec … Hcode_i) #H3
-@(absurd1 (lang i 〈i,b〉))
-@(iff_trans … (H3 〈i,b〉)) 
-@(iff_trans … (equiv_diag …)) >fst_pair 
+cases (a href="cic:/matita/Reverse_complexity/reverse/not_included_ex.def(10)"not_included_ex/a  … H1 ? Hs2_i) #b #H2
+lapply (a href="cic:/matita/Reverse_complexity/reverse/diag_spec.def(11)"diag_spec/a … Hcode_i) #H3
+@(a href="cic:/matita/Reverse_complexity/reverse/absurd1.def(3)"absurd1/a (a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"lang/a i 〈i,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/a))
+@(a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a … (H3 〈i,ba title="abstract pair" href="cic:/fakeuri.def(1)"〉/a)) 
+@(a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a … (a href="cic:/matita/Reverse_complexity/reverse/equiv_diag.def(10)"equiv_diag/a …)) >a href="cic:/matita/Reverse_complexity/reverse/fst_pair.dec"fst_pair/a 
 %[* #_ // |#H6 % // ]
 qed.
 
 (******************************************************************************)
 (* definition sumF ≝ λf,g:nat→nat.λn.f n + g n. *)
 
-definition to_Some ≝ λf.λx:nat. Some nat (f x).
+img class="anchor" src="icons/tick.png" id="to_Some"definition to_Some ≝ λf.λx:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a (f x).
 
-definition deopt ≝ λn. match n with 
-  [ None ⇒ 1
+img class="anchor" src="icons/tick.png" id="deopt"definition deopt ≝ λn. match n with 
+  [ None ⇒ a title="natural number" href="cic:/fakeuri.def(1)"1/a
   | Some n ⇒ n].
   
-definition opt_comp ≝ λf,g:nat → option nat. λx.
+img class="anchor" src="icons/tick.png" id="opt_comp"definition opt_comp ≝ λf,g:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. λx.
   match g x with 
-  [ None ⇒ None ?
+  [ None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
   | Some y ⇒ f y ].   
 
 (* axiom CFU: ∀h,g,s. CF s (to_Some h)  → CF s (to_Some (of_size ∘ g)) → 
   CF (Slow s) (λx.U (h x) (g x)). *)
   
-axiom sU2: nat → nat → nat.
-axiom sU: nat → nat → nat → nat.
+img class="anchor" src="icons/tick.png" id="sU2"axiom sU2: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="sU"axiom sU: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
 
 (* axiom CFU: CF sU (λx.U (fst x) (snd x)). *)
 
-axiom CFU: ∀h,g,f,s1,s2,s3. 
-  CF s1 (to_Some h)  → CF s2 (to_Some g) → CF s3 (to_Some f) → 
-  CF (λx. s1 x + s2 x + s3 x + sU (size_f h x) (size_f g x) (size_f f x)) 
-    (λx.U 〈h x,g x〉 (|f x|)).
+img class="anchor" src="icons/tick.png" id="CFU"axiom CFU: ∀h,g,f,s1,s2,s3. 
+  a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s1 (a href="cic:/matita/Reverse_complexity/reverse/to_Some.def(1)"to_Some/a h)  → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s2 (a href="cic:/matita/Reverse_complexity/reverse/to_Some.def(1)"to_Some/a g) → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s3 (a href="cic:/matita/Reverse_complexity/reverse/to_Some.def(1)"to_Some/a f) → 
+  a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a (λx. s1 x a title="natural plus" href="cic:/fakeuri.def(1)"+/a s2 x a title="natural plus" href="cic:/fakeuri.def(1)"+/a s3 x a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a h x) (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a g x) (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a f x)) 
+    (λx.a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈h x,g xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a (|f xa title="size" href="cic:/fakeuri.def(1)"|/a)).
     
-axiom monotonic_sU: ∀a1,a2,b1,b2,c1,c2. a1 ≤ a2 → b1 ≤ b2 → c1 ≤c2 →
-  sU a1 b1 c1 ≤ sU a2 b2 c2.
+img class="anchor" src="icons/tick.png" id="monotonic_sU"axiom monotonic_sU: ∀a1,a2,b1,b2,c1,c2. a1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a2 → b1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b2 → c1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/ac2 →
+  a href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a a1 b1 c1 a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a a2 b2 c2.
 
-definition sU_space ≝ λi,x,r.i+x+r.
-definition sU_time ≝ λi,x,r.i+x+(i^2)*r*(log 2 r).
+(* definition sU_space ≝ λi,x,r.i+x+r.
+definition sU_time ≝ λi,x,r.i+x+(i^2)*r*(log 2 r). *)
 
 (*
 axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g → 
@@ -275,33 +273,33 @@ axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g →
 axiom CF_comp_strong: ∀f,g,s1,s2. CF s1 f → CF s2 g → 
   CF (s1 ∘ s2) (opt_comp f g). *)
 
-definition IF ≝ λb,f,g:nat →option nat. λx.
+img class="anchor" src="icons/tick.png" id="IF"definition IF ≝ λb,f,g:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a →a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. λx.
   match b x with 
-  [None ⇒ None ?
-  |Some n ⇒ if (eqb n 0) then f x else g x].
+  [None ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
+  |Some n ⇒ if (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a n a title="natural number" href="cic:/fakeuri.def(1)"0/a) then f x else g x].
 
-axiom IF_CF: ∀b,f,g,sb,sf,sg. CF sb b → CF sf f → CF sg g → 
-  CF (λn. sb n + sf n + sg n) (IF b f g).
+img class="anchor" src="icons/tick.png" id="IF_CF"axiom IF_CF: ∀b,f,g,sb,sf,sg. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a sb b → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a sf f → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a sg g → 
+  a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a (λn. sb n a title="natural plus" href="cic:/fakeuri.def(1)"+/a sf n a title="natural plus" href="cic:/fakeuri.def(1)"+/a sg n) (a href="cic:/matita/Reverse_complexity/reverse/IF.def(2)"IF/a b f g).
 
-lemma diag_cf_def : ∀s.∀i. 
-  diag_cf s i =  
-    IF (λi.U (pair (fst i) i) (|of_size (s (|i|))|)) (λi.Some ? 1) (λi.Some ? 0) i.
-#s #i normalize >size_of_size // qed. 
+img class="anchor" src="icons/tick.png" id="diag_cf_def"lemma diag_cf_def : ∀s.∀i. 
+  a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"diag_cf/a s i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a  
+    a href="cic:/matita/Reverse_complexity/reverse/IF.def(2)"IF/a (λi.a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a (a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i) i) (|a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a (s (|ia title="size" href="cic:/fakeuri.def(1)"|/a))a title="size" href="cic:/fakeuri.def(1)"|/a)) (λi.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? a title="natural number" href="cic:/fakeuri.def(1)"1/a) (λi.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? a title="natural number" href="cic:/fakeuri.def(1)"0/a) i.
+#s #i normalize >a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"size_of_size/a // qed. 
 
 (* and now ... *)
-axiom CF_pair: ∀f,g,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (g x)) → 
-  CF s (λx.Some ? (pair (f x) (g x))).
+img class="anchor" src="icons/tick.png" id="CF_pair"axiom CF_pair: ∀f,g,s. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (f x)) → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (g x)) → 
+  a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a (f x) (g x))).
 
-axiom CF_fst: ∀f,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (fst (f x))).
+img class="anchor" src="icons/tick.png" id="CF_fst"axiom CF_fst: ∀f,s. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (f x)) → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a (f x))).
 
-definition minimal ≝ λs. CF s (λn. Some ? n) ∧ ∀c. CF s (λn. Some ? c).
+img class="anchor" src="icons/tick.png" id="minimal"definition minimal ≝ λs. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λn. a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? n) a title="logical and" href="cic:/fakeuri.def(1)"∧/a ∀c. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λn. a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? c).
 
 
 (*
 axiom le_snd: ∀n. |snd n| ≤ |n|.
 axiom daemon: ∀P:Prop.P. *)
 
-definition constructible ≝ λs. CF s (λx.Some ? (of_size (s (|x|)))).
+img class="anchor" src="icons/tick.png" id="constructible"definition constructible ≝ λs. a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s (λx.a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? (a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a (s (|xa title="size" href="cic:/fakeuri.def(1)"|/a)))).
 
 (*
 lemma compl1: ∀s. 
@@ -318,20 +316,20 @@ lemma compl1: ∀s.
 #s #H1 #H2 #H3 @monotonic_CF [3: @(CFU ??? s s s) @CFU //
 qed.  *)
 
-lemma diag_s: ∀s. minimal s → constructible s → 
-  CF (λx.s x + sU x x (s x)) (diag_cf s).
+img class="anchor" src="icons/tick.png" id="diag_s"lemma diag_s: ∀s. a href="cic:/matita/Reverse_complexity/reverse/minimal.def(5)"minimal/a s → a href="cic:/matita/Reverse_complexity/reverse/constructible.def(5)"constructible/a s → 
+  a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a (λx.s x a title="natural plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a x x (s x)) (a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"diag_cf/a s).
 #s * #Hs_id #Hs_c #Hs_constr 
-@ext_CF [2: #n @sym_eq @diag_cf_def | skip]
-@(monotonic_CF ???? (IF_CF (λi:ℕ.U (pair (fst i) i) (|of_size (s (|i|))|))
-   … (λi.s i + s i + s i + (sU (size_f fst i) (size_f (λi.i) i) (size_f (λi.of_size (s (|i|))) i))) … (Hs_c 1) (Hs_c 0) … ))
-  [2: @CFU [@CF_fst // | // |@Hs_constr]
-  |@(O_ext2 (λn:ℕ.s n+sU (size_f fst n) n (s n) + (s n+s n+s n+s n))) 
-    [2: #i >size_f_size >size_of_size >size_f_id //] 
-   @O_absorbr 
-    [%{1} %{0} #n #_ >commutative_times <times_n_1 @le_plus //
-     @monotonic_sU // 
-    |@O_plus_l @(O_plus … (O_refl s)) @(O_plus … (O_refl s)) 
-     @(O_plus … (O_refl s)) //
+@a href="cic:/matita/Reverse_complexity/reverse/ext_CF.def(5)"ext_CF/a [2: #n @a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a @a href="cic:/matita/Reverse_complexity/reverse/diag_cf_def.def(3)"diag_cf_def/a | skip]
+@(a href="cic:/matita/Reverse_complexity/reverse/monotonic_CF.def(11)"monotonic_CF/a ???? (a href="cic:/matita/Reverse_complexity/reverse/IF_CF.dec"IF_CF/a (λi:a title="Natural numbers" href="cic:/fakeuri.def(1)"ℕ/a.a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a (a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i) i) (|a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a (s (|ia title="size" href="cic:/fakeuri.def(1)"|/a))a title="size" href="cic:/fakeuri.def(1)"|/a))
+   … (λi.s i a title="natural plus" href="cic:/fakeuri.def(1)"+/a s i a title="natural plus" href="cic:/fakeuri.def(1)"+/a s i a title="natural plus" href="cic:/fakeuri.def(1)"+/a (a href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a i) (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a (λi.i) i) (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a (λi.a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a (s (|ia title="size" href="cic:/fakeuri.def(1)"|/a))) i))) … (Hs_c a title="natural number" href="cic:/fakeuri.def(1)"1/a) (Hs_c a title="natural number" href="cic:/fakeuri.def(1)"0/a) … ))
+  [2: @a href="cic:/matita/Reverse_complexity/reverse/CFU.dec"CFU/a [@a href="cic:/matita/Reverse_complexity/reverse/CF_fst.dec"CF_fst/a // | // |@Hs_constr]
+  |@(a href="cic:/matita/arithmetics/bigO/O_ext2.def(4)"O_ext2/a (λn:a title="Natural numbers" href="cic:/fakeuri.def(1)"ℕ/a.s na title="natural plus" href="cic:/fakeuri.def(1)"+/aa href="cic:/matita/Reverse_complexity/reverse/sU.dec"sU/a (a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"size_f/a a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a n) n (s n) a title="natural plus" href="cic:/fakeuri.def(1)"+/a (s na title="natural plus" href="cic:/fakeuri.def(1)"+/as na title="natural plus" href="cic:/fakeuri.def(1)"+/as na title="natural plus" href="cic:/fakeuri.def(1)"+/as n))) 
+    [2: #i >a href="cic:/matita/Reverse_complexity/reverse/size_f_size.def(13)"size_f_size/a >a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"size_of_size/a >a href="cic:/matita/Reverse_complexity/reverse/size_f_id.def(13)"size_f_id/a //] 
+   @a href="cic:/matita/arithmetics/bigO/O_absorbr.def(12)"O_absorbr/a 
+    [%{a title="natural number" href="cic:/fakeuri.def(1)"1/a} %{a title="natural number" href="cic:/fakeuri.def(1)"0/a} #n #_ >a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"commutative_times/a <a href="cic:/matita/arithmetics/nat/times_n_1.def(8)"times_n_1/a @a href="cic:/matita/arithmetics/nat/le_plus.def(7)"le_plus/a //
+     @a href="cic:/matita/Reverse_complexity/reverse/monotonic_sU.dec"monotonic_sU/a // 
+    |@a href="cic:/matita/arithmetics/bigO/O_plus_l.def(10)"O_plus_l/a @(a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"O_plus/a … (a href="cic:/matita/arithmetics/bigO/O_refl.def(9)"O_refl/a s)) @(a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"O_plus/a … (a href="cic:/matita/arithmetics/bigO/O_refl.def(9)"O_refl/a s)) 
+     @(a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"O_plus/a … (a href="cic:/matita/arithmetics/bigO/O_refl.def(9)"O_refl/a s)) //
   ]
 qed.
 
@@ -348,12 +346,12 @@ theorem hierarchy_theorem_right: ∀s1,s2:nat→nat.
 qed.
 *)
 
-theorem hierarchy_theorem_left: ∀s1,s2:nat→nat.
-   O(s1) ⊆ O(s2) → CF s1 ⊆ CF s2.
+img class="anchor" src="icons/tick.png" id="hierarchy_theorem_left"theorem hierarchy_theorem_left: ∀s1,s2:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+   a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a(s1) a title="subset" href="cic:/fakeuri.def(1)"⊆/a a href="cic:/matita/arithmetics/bigO/O.def(3)"O/a(s2) → a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s1 a title="subset" href="cic:/fakeuri.def(1)"⊆/a a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"CF/a s2.
 #s1 #s2 #HO #f * #i * #Hcode * #c * #a #Hs1_i %{i} % //
-cases (sub_O_to_O … HO) -HO #c1 * #b #Hs1s2 
-%{(c*c1)} %{(max a b)} #x #lemax 
-cases (Hs1_i x ?) [2: @(le_maxl …lemax)]
-#y #Hy %{y} @(monotonic_U … Hy) >associative_times
-@le_times // @Hs1s2 @(le_maxr … lemax)
+cases (a href="cic:/matita/arithmetics/bigO/sub_O_to_O.def(10)"sub_O_to_O/a … HO) -HO #c1 * #b #Hs1s2 
+%{(ca title="natural times" href="cic:/fakeuri.def(1)"*/ac1)} %{(a href="cic:/matita/arithmetics/nat/max.def(2)"max/a a b)} #x #lemax 
+cases (Hs1_i x ?) [2: @(a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a …lemax)]
+#y #Hy %{y} @(a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … Hy) >a href="cic:/matita/arithmetics/nat/associative_times.def(10)"associative_times/a
+@a href="cic:/matita/arithmetics/nat/le_times.def(9)"le_times/a // @Hs1s2 @(a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"le_maxr/a … lemax)
 qed.
\ No newline at end of file