commit by user andrea

diff --git a/weblib/Reverse_complexity/reverse.ma b/weblib/Reverse_complexity/reverse.ma
index 73814b17ac4c5153dc3c341cf5cbafc01a1194ad..c99de03c5a869581686e53474efdcca41b1d83fd 100644 (file)
--- a/weblib/Reverse_complexity/reverse.ma
+++ b/weblib/Reverse_complexity/reverse.ma
@@ -6,11 +6,11 @@ include "arithmetics/bigO.ma".
  
 (*********************************** pairing **********************************) 
 
-axiom pair: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
-axiom fst : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
-axiom snd : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
-axiom fst_pair: ∀a,b. \ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/pair.dec"\ 6pair\ 5/a\ 6 a b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a.
-axiom snd_pair: ∀a,b. \ 5a href="cic:/matita/Reverse_complexity/reverse/snd.dec"\ 6snd\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/pair.dec"\ 6pair\ 5/a\ 6 a b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b. 
+\ 5img class="anchor" src="icons/tick.png" id="pair"\ 6axiom pair: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="fst"\ 6axiom fst : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="snd"\ 6axiom snd : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="fst_pair"\ 6axiom fst_pair: ∀a,b. \ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/pair.dec"\ 6pair\ 5/a\ 6 a b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a.
+\ 5img class="anchor" src="icons/tick.png" id="snd_pair"\ 6axiom snd_pair: ∀a,b. \ 5a href="cic:/matita/Reverse_complexity/reverse/snd.dec"\ 6snd\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/pair.dec"\ 6pair\ 5/a\ 6 a b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"\ 6option\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="u"\ 6axiom u: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"\ 6option\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 
-let rec U c n on n ≝ 
-  match n with  
+\ 5img class="anchor" src="icons/tick.png" id="U"\ 6let rec U c n on n ≝ 
+  match n in nat with  
   [ O ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
   | S m ⇒ match \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 c with 
     [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? c (* halting case *)
@@ -30,12 +30,12 @@ let rec U c n on n ≝
     ]
   ].
  
-lemma halt_U: ∀i,n,y. \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i.
+\ 5img class="anchor" src="icons/tick.png" id="halt_U"\ 6lemma halt_U: ∀i,n,y. \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i.
 #i #n #y #H cases n
   [normalize #H1 destruct |#m normalize >H normalize #H1 destruct //]
 qed. 
 
-lemma Some_to_halt: ∀n,i,y. \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? .
+\ 5img class="anchor" src="icons/tick.png" id="Some_to_halt"\ 6lemma Some_to_halt: ∀n,i,y. \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? .
 #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. \ 5a href="cic:/matita/Reverse_complexity/reverse/U.
   ]
 qed. 
 
-lemma monotonici_U: ∀y,n,m,i.
+\ 5img class="anchor" src="icons/tick.png" id="monotonici_U"\ 6lemma monotonici_U: ∀y,n,m,i.
   \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? 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 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6m →
+\ 5img class="anchor" src="icons/tick.png" id="monotonic_U"\ 6lemma monotonic_U: ∀i,n,m,y.n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6m →
   \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y.
 #i #n #m #y #lenm #H >(\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 m n) // @\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonici_U.def(5)"\ 6monotonici_U\ 5/a\ 6 //
 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.
+\ 5img class="anchor" src="icons/tick.png" id="unique_U"\ 6lemma unique_U: ∀i,n,m,yn,ym.
   \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? yn → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? ym → yn \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 ym.
 #i #n #m #yn #ym #Hn #Hm cases (\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"\ 6decidable_le\ 5/a\ 6 n m)
   [#lenm lapply (\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … 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.
+\ 5img class="anchor" src="icons/tick.png" id="code_for"\ 6definition code_for ≝ λf,i.∀x.
   \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6n.∀m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 〈i,x\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.
 
-definition terminate ≝ λc,r. \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6y. \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 c r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y.
+\ 5img class="anchor" src="icons/tick.png" id="terminate"\ 6definition terminate ≝ λc,r. \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6y. \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 c r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y.
 
 interpretation "termination" 'fintersects c r = (terminate c r).
  
-definition lang ≝ λi,x.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6r,y\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 〈i,x\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6  \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 y. 
+\ 5img class="anchor" src="icons/tick.png" id="lang"\ 6definition lang ≝ λi,x.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6r,y\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 〈i,x\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6  \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 y. 
 
-lemma lang_cf :∀f,i,x. \ 5a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"\ 6code_for\ 5/a\ 6 f i → 
+\ 5img class="anchor" src="icons/tick.png" id="lang_cf"\ 6lemma lang_cf :∀f,i,x. \ 5a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"\ 6code_for\ 5/a\ 6 f i → 
   \ 5a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"\ 6lang\ 5/a\ 6 i x \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6y.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 y.
 #f #i #x normalize #H %
   [* #n * #y * #H1 #posy %{y} % // 
@@ -95,175 +95,173 @@ qed.
 
 (******************************* complexity classes ***************************)
 
-axiom size: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
-axiom of_size: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="size"\ 6axiom size: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="of_size"\ 6axiom of_size: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 
 interpretation "size" 'card n = (size n).
 
-axiom size_of_size: ∀n. |\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
-axiom of_size_max: ∀i,n. |i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n → i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n.
+\ 5img class="anchor" src="icons/tick.png" id="size_of_size"\ 6axiom size_of_size: ∀n. |\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
+\ 5img class="anchor" src="icons/tick.png" id="of_size_max"\ 6axiom of_size_max: ∀i,n. |i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n → i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n.
 
-axiom size_fst : ∀n. |\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 |n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="size_fst"\ 6axiom size_fst : ∀n. |\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 |n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
 
-axiom a : Max0.
+\ 5img class="anchor" src="icons/tick.png" id="size_f"\ 6definition size_f ≝ λf,n.Max_{i\ 5font class="Apple-style-span" color="#FF0000"\ 6 < \ 5/font\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n) | \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 (|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6) n \ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6|(f i)\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
 
-definition size_f ≝ λf,n.Max_{i\ 5font class="Apple-style-span" color="#FF0000"\ 6 < \ 5/font\ 6S (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)|.
+\ 5img class="anchor" src="icons/tick.png" id="size_f_def"\ 6lemma size_f_def: ∀f,n. \ 5a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"\ 6size_f\ 5/a\ 6 f n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
+  Max_{i < \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n) | \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 (|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6) n\ 5a title="bigop" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6|(f i)\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
 // 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 //]
+\ 5img class="anchor" src="icons/tick.png" id="size_f_size"\ 6lemma size_f_size : ∀f,n. \ 5a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"\ 6size_f\ 5/a\ 6 (f \ 5a title="function composition" href="cic:/fakeuri.def(1)"\ 6∘\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/size.dec"\ 6size\ 5/a\ 6) n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 |(f n)\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
+#f #n @\ 5a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"\ 6le_to_le_to_eq\ 5/a\ 6
+  [@\ 5a href="cic:/matita/arithmetics/min_max/Max_le.def(9)"\ 6Max_le\ 5/a\ 6 #a #lta #Ha normalize >(\ 5a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"\ 6eqb_true_to_eq\ 5/a\ 6  … Ha) //
+  |<(\ 5a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"\ 6size_of_size\ 5/a\ 6 n) in ⊢ (?%?); >\ 5a href="cic:/matita/Reverse_complexity/reverse/size_f_def.def(4)"\ 6size_f_def\ 5/a\ 6
+   @(\ 5a href="cic:/matita/arithmetics/min_max/le_Max.def(12)"\ 6le_Max\ 5/a\ 6 (λi.|f (|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6) ? (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n)) (\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n) ??)
+    [@\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 // | @\ 5a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"\ 6eq_to_eqb_true\ 5/a\ 6 //]
   ]
 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 //]
+\ 5img class="anchor" src="icons/tick.png" id="size_f_id"\ 6lemma size_f_id : ∀n. \ 5a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"\ 6size_f\ 5/a\ 6 (λx.x) n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
+#n @\ 5a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"\ 6le_to_le_to_eq\ 5/a\ 6
+  [@\ 5a href="cic:/matita/arithmetics/min_max/Max_le.def(9)"\ 6Max_le\ 5/a\ 6 #a #lta #Ha >(\ 5a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"\ 6eqb_true_to_eq\ 5/a\ 6  … Ha) //
+  |<(\ 5a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"\ 6size_of_size\ 5/a\ 6 n) in ⊢ (?%?); >\ 5a href="cic:/matita/Reverse_complexity/reverse/size_f_def.def(4)"\ 6size_f_def\ 5/a\ 6
+   @(\ 5a href="cic:/matita/arithmetics/min_max/le_Max.def(12)"\ 6le_Max\ 5/a\ 6 (λi.|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6) ? (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n)) (\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n) ??)
+    [@\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 // | @\ 5a href="cic:/matita/arithmetics/nat/eq_to_eqb_true.def(5)"\ 6eq_to_eqb_true\ 5/a\ 6 //]
   ]
 qed.
 
-lemma size_f_fst : ∀n. size_f fst n ≤ n.
-#n @Max_le #a #lta #Ha <(eqb_true_to_eq  … Ha) //
+\ 5img class="anchor" src="icons/tick.png" id="size_f_fst"\ 6lemma size_f_fst : ∀n. \ 5a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"\ 6size_f\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
+#n @\ 5a href="cic:/matita/arithmetics/min_max/Max_le.def(9)"\ 6Max_le\ 5/a\ 6 #a #lta #Ha <(\ 5a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"\ 6eqb_true_to_eq\ 5/a\ 6  … 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.
+\ 5img class="anchor" src="icons/tick.png" id="C"\ 6definition C ≝ λs,i.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6c.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6a.∀x.a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 |x\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 → \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6y. 
+  \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 〈i,x\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 (c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(s(|x\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y.
 
-definition CF ≝ λs,f.∃i.code_for f i ∧ C s i.
+\ 5img class="anchor" src="icons/tick.png" id="CF"\ 6definition CF ≝ λs,f.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6i.\ 5a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"\ 6code_for\ 5/a\ 6 f i \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/C.def(3)"\ 6C\ 5/a\ 6 s i.
 
-lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
+\ 5img class="anchor" src="icons/tick.png" id="ext_CF"\ 6lemma ext_CF : ∀f,g,s. (∀n. f n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g n) → \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s f → \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 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.
+\ 5img class="anchor" src="icons/tick.png" id="monotonic_CF"\ 6lemma monotonic_CF: ∀s1,s2,f. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s2 s1 → \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s1 f → \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 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 %{(c2\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c1)} %{(\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 a b)} 
+#x #Hmax cases (H2 x ?) [2:@(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … Hmax)] #y #Hy
+%{y} @(\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 …Hy) >\ 5a href="cic:/matita/arithmetics/nat/associative_times.def(10)"\ 6associative_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 // @H @(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … 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. 
+\ 5img class="anchor" src="icons/tick.png" id="diag"\ 6definition diag ≝ λs,i. 
+  \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 〈\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 i,i\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 (s (|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6. 
 
-lemma equiv_diag: ∀s,i. 
-  diag s i ↔ 〈fst i, i〉 ↓ s (|i|) ∧ ¬lang (fst i) i.
+\ 5img class="anchor" src="icons/tick.png" id="equiv_diag"\ 6lemma equiv_diag: ∀s,i. 
+  \ 5a href="cic:/matita/Reverse_complexity/reverse/diag.def(2)"\ 6diag\ 5/a\ 6 s i \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 〈\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 i, i\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 \ 5a title="termination" href="cic:/fakeuri.def(1)"\ 6↓\ 5/a\ 6 s (|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6\ 5a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"\ 6lang\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 i) i.
 #s #i %
-  [whd in ⊢ (%→?); #H % [%{0} //] % * #x * #y *
-   #H1 #Hy cut (0 = y) [@(unique_U … H H1)] #eqy /2/
+  [whd in ⊢ (%→?); #H % [%{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6} //] % * #x * #y *
+   #H1 #Hy cut (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y) [@(\ 5a href="cic:/matita/Reverse_complexity/reverse/unique_U.def(9)"\ 6unique_U\ 5/a\ 6 … H H1)] #eqy /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
   |* * #y cases y //
-   #y0 #H * #H1 @False_ind @H1 -H1 whd %{(s (|i|))} %{(S y0)} % //
+   #y0 #H * #H1 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @H1 -H1 whd %{(s (|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))} %{(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 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)].
+\ 5img class="anchor" src="icons/tick.png" id="diag_cf"\ 6definition diag_cf ≝ λs,i.
+  match \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 〈\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 i,i\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 (s (|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) with
+  [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
+  | Some y ⇒ if (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 y \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6) then (\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6) else (\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6)].
 
-lemma diag_cf_OK: ∀s,x. diag s x ↔ ∃y.diag_cf s x = Some ? y ∧ 0 < y.
+\ 5img class="anchor" src="icons/tick.png" id="diag_cf_OK"\ 6lemma diag_cf_OK: ∀s,x. \ 5a href="cic:/matita/Reverse_complexity/reverse/diag.def(2)"\ 6diag\ 5/a\ 6 s x \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6y.\ 5a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"\ 6diag_cf\ 5/a\ 6 s x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 y.
 #s #x % 
-  [whd in ⊢ (%→?); #H %{1} % // whd in ⊢ (??%?); >H // 
+  [whd in ⊢ (%→?); #H %{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6} % // whd in ⊢ (??%?); >H // 
   |* #y * whd in ⊢ (??%?→?→%); 
-   cases (U 〈fst x,x〉 (s (|x|))) normalize
+   cases (\ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 〈\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 x,x\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 (s (|x\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))) 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 (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 x \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6)) #Hx >Hx 
+      [>(\ 5a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"\ 6eqb_true_to_eq\ 5/a\ 6 … Hx) // 
+      |normalize #H destruct #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ? H) @\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 //  
       ]
     ]
   ]
 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
+\ 5img class="anchor" src="icons/tick.png" id="diag_spec"\ 6lemma diag_spec: ∀s,i. \ 5a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"\ 6code_for\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"\ 6diag_cf\ 5/a\ 6 s) i → ∀x. \ 5a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"\ 6lang\ 5/a\ 6 i x \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/diag.def(2)"\ 6diag\ 5/a\ 6 s x.
+#s #i #Hcode #x @(\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6  … (\ 5a href="cic:/matita/Reverse_complexity/reverse/lang_cf.def(10)"\ 6lang_cf\ 5/a\ 6 … Hcode)) @\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @\ 5a href="cic:/matita/Reverse_complexity/reverse/diag_cf_OK.def(8)"\ 6diag_cf_OK\ 5/a\ 6
 qed. 
 
 (******************************************************************************)
 
-lemma absurd1: ∀P. iff P (¬ P) →False.
-#P * #H1 #H2 cut (¬P) [% #H2 @(absurd … H2) @H1 //] 
-#H3 @(absurd ?? H3) @H2 @H3 
+\ 5img class="anchor" src="icons/tick.png" id="absurd1"\ 6lemma absurd1: ∀P. \ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 P (\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 P) →\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
+#P * #H1 #H2 cut (\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6P) [% #H2 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … H2) @H1 //] 
+#H3 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ?? 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.
+\ 5img class="anchor" src="icons/tick.png" id="pad"\ 6axiom pad : ∀a,n. |a\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6b. |〈a,b\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
 
-lemma not_included_ex: ∀s1,s2. not_O s2 s1 → ∀i. C s2 i →
-  ∃b.〈i, 〈i,b〉〉 ↓ s1 (|〈i,b〉|).
+\ 5img class="anchor" src="icons/tick.png" id="not_included_ex"\ 6lemma not_included_ex: ∀s1,s2. \ 5a href="cic:/matita/arithmetics/bigO/not_O.def(3)"\ 6not_O\ 5/a\ 6 s2 s1 → ∀i. \ 5a href="cic:/matita/Reverse_complexity/reverse/C.def(3)"\ 6C\ 5/a\ 6 s2 i →
+  \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6b.〈i, 〈i,b\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 \ 5a title="termination" href="cic:/fakeuri.def(1)"\ 6↓\ 5/a\ 6 s1 (|〈i,b\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6).
 #s1 #s2  #H #i * #c * #x0 #H1 
-cases (H c (max (S(|i|)) x0)) #x1 * #H2 #H3 cases (pad i x1 ?) 
+cases (H c (\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6(|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) x0)) #x1 * #H2 #H3 cases (\ 5a href="cic:/matita/Reverse_complexity/reverse/pad.dec"\ 6pad\ 5/a\ 6 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,b\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 ?)
+    [#z >H4 #H5 %{z} @(\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … H5) @\ 5a href="cic:/matita/arithmetics/nat/lt_to_le.def(6)"\ 6lt_to_le\ 5/a\ 6 //
+    |>H4 @(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … H2)
     ]
-  |@(le_maxl … H2)
+  |@(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … H2)
   ]
 qed.
 
-lemma diag1_not_s1: ∀s1,s2. not_O s2 s1 → ¬ CF s2 (diag_cf s1).
+\ 5img class="anchor" src="icons/tick.png" id="diag1_not_s1"\ 6lemma diag1_not_s1: ∀s1,s2. \ 5a href="cic:/matita/arithmetics/bigO/not_O.def(3)"\ 6not_O\ 5/a\ 6 s2 s1 → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s2 (\ 5a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"\ 6diag_cf\ 5/a\ 6 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 (\ 5a href="cic:/matita/Reverse_complexity/reverse/not_included_ex.def(10)"\ 6not_included_ex\ 5/a\ 6  … H1 ? Hs2_i) #b #H2
+lapply (\ 5a href="cic:/matita/Reverse_complexity/reverse/diag_spec.def(11)"\ 6diag_spec\ 5/a\ 6 … Hcode_i) #H3
+@(\ 5a href="cic:/matita/Reverse_complexity/reverse/absurd1.def(3)"\ 6absurd1\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"\ 6lang\ 5/a\ 6 i 〈i,b\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6))
+@(\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 … (H3 〈i,b\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6)) 
+@(\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 … (\ 5a href="cic:/matita/Reverse_complexity/reverse/equiv_diag.def(10)"\ 6equiv_diag\ 5/a\ 6 …)) >\ 5a href="cic:/matita/Reverse_complexity/reverse/fst_pair.dec"\ 6fst_pair\ 5/a\ 6 
 %[* #_ // |#H6 % // ]
 qed.
 
 (******************************************************************************)
 (* definition sumF ≝ λf,g:nat→nat.λn.f n + g n. *)
 
-definition to_Some ≝ λf.λx:nat. Some nat (f x).
+\ 5img class="anchor" src="icons/tick.png" id="to_Some"\ 6definition to_Some ≝ λf.λx:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 (f x).
 
-definition deopt ≝ λn. match n with 
-  [ None ⇒ 1
+\ 5img class="anchor" src="icons/tick.png" id="deopt"\ 6definition deopt ≝ λn. match n with 
+  [ None ⇒ \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6
   | Some n ⇒ n].
   
-definition opt_comp ≝ λf,g:nat → option nat. λx.
+\ 5img class="anchor" src="icons/tick.png" id="opt_comp"\ 6definition opt_comp ≝ λf,g:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"\ 6option\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. λx.
   match g x with 
-  [ None ⇒ None ?
+  [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
   | 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.
+\ 5img class="anchor" src="icons/tick.png" id="sU2"\ 6axiom sU2: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="sU"\ 6axiom sU: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
 
 (* 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|)).
+\ 5img class="anchor" src="icons/tick.png" id="CFU"\ 6axiom CFU: ∀h,g,f,s1,s2,s3. 
+  \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s1 (\ 5a href="cic:/matita/Reverse_complexity/reverse/to_Some.def(1)"\ 6to_Some\ 5/a\ 6 h)  → \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s2 (\ 5a href="cic:/matita/Reverse_complexity/reverse/to_Some.def(1)"\ 6to_Some\ 5/a\ 6 g) → \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s3 (\ 5a href="cic:/matita/Reverse_complexity/reverse/to_Some.def(1)"\ 6to_Some\ 5/a\ 6 f) → 
+  \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 (λx. s1 x \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 s2 x \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 s3 x \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/sU.dec"\ 6sU\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"\ 6size_f\ 5/a\ 6 h x) (\ 5a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"\ 6size_f\ 5/a\ 6 g x) (\ 5a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"\ 6size_f\ 5/a\ 6 f x)) 
+    (λx.\ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 〈h x,g x\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 (|f x\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)).
     
-axiom monotonic_sU: ∀a1,a2,b1,b2,c1,c2. a1 ≤ a2 → b1 ≤ b2 → c1 ≤c2 →
-  sU a1 b1 c1 ≤ sU a2 b2 c2.
+\ 5img class="anchor" src="icons/tick.png" id="monotonic_sU"\ 6axiom monotonic_sU: ∀a1,a2,b1,b2,c1,c2. a1 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 a2 → b1 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b2 → c1 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6c2 →
+  \ 5a href="cic:/matita/Reverse_complexity/reverse/sU.dec"\ 6sU\ 5/a\ 6 a1 b1 c1 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/sU.dec"\ 6sU\ 5/a\ 6 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.
+\ 5img class="anchor" src="icons/tick.png" id="IF"\ 6definition IF ≝ λb,f,g:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 →\ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"\ 6option\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. λx.
   match b x with 
-  [None ⇒ None ?
-  |Some n ⇒ if (eqb n 0) then f x else g x].
+  [None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
+  |Some n ⇒ if (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 n \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6) 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).
+\ 5img class="anchor" src="icons/tick.png" id="IF_CF"\ 6axiom IF_CF: ∀b,f,g,sb,sf,sg. \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 sb b → \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 sf f → \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 sg g → 
+  \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 (λn. sb n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 sf n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 sg n) (\ 5a href="cic:/matita/Reverse_complexity/reverse/IF.def(2)"\ 6IF\ 5/a\ 6 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. 
+\ 5img class="anchor" src="icons/tick.png" id="diag_cf_def"\ 6lemma diag_cf_def : ∀s.∀i. 
+  \ 5a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"\ 6diag_cf\ 5/a\ 6 s i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6  
+    \ 5a href="cic:/matita/Reverse_complexity/reverse/IF.def(2)"\ 6IF\ 5/a\ 6 (λi.\ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/pair.dec"\ 6pair\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 i) i) (|\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 (s (|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)) (λi.\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6) (λi.\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6) i.
+#s #i normalize >\ 5a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"\ 6size_of_size\ 5/a\ 6 // 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))).
+\ 5img class="anchor" src="icons/tick.png" id="CF_pair"\ 6axiom CF_pair: ∀f,g,s. \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s (λx.\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (f x)) → \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s (λx.\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (g x)) → 
+  \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s (λx.\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (\ 5a href="cic:/matita/Reverse_complexity/reverse/pair.dec"\ 6pair\ 5/a\ 6 (f x) (g x))).
 
-axiom CF_fst: ∀f,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (fst (f x))).
+\ 5img class="anchor" src="icons/tick.png" id="CF_fst"\ 6axiom CF_fst: ∀f,s. \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s (λx.\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (f x)) → \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s (λx.\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 (f x))).
 
-definition minimal ≝ λs. CF s (λn. Some ? n) ∧ ∀c. CF s (λn. Some ? c).
+\ 5img class="anchor" src="icons/tick.png" id="minimal"\ 6definition minimal ≝ λs. \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s (λn. \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? n) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 ∀c. \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s (λn. \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? c).
 
 
 (*
 axiom le_snd: ∀n. |snd n| ≤ |n|.
 axiom daemon: ∀P:Prop.P. *)
 
-definition constructible ≝ λs. CF s (λx.Some ? (of_size (s (|x|)))).
+\ 5img class="anchor" src="icons/tick.png" id="constructible"\ 6definition constructible ≝ λs. \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s (λx.\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 (s (|x\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6)))).
 
 (*
 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).
+\ 5img class="anchor" src="icons/tick.png" id="diag_s"\ 6lemma diag_s: ∀s. \ 5a href="cic:/matita/Reverse_complexity/reverse/minimal.def(5)"\ 6minimal\ 5/a\ 6 s → \ 5a href="cic:/matita/Reverse_complexity/reverse/constructible.def(5)"\ 6constructible\ 5/a\ 6 s → 
+  \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 (λx.s x \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/sU.dec"\ 6sU\ 5/a\ 6 x x (s x)) (\ 5a href="cic:/matita/Reverse_complexity/reverse/diag_cf.def(2)"\ 6diag_cf\ 5/a\ 6 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)) //
+@\ 5a href="cic:/matita/Reverse_complexity/reverse/ext_CF.def(5)"\ 6ext_CF\ 5/a\ 6 [2: #n @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @\ 5a href="cic:/matita/Reverse_complexity/reverse/diag_cf_def.def(3)"\ 6diag_cf_def\ 5/a\ 6 | skip]
+@(\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_CF.def(11)"\ 6monotonic_CF\ 5/a\ 6 ???? (\ 5a href="cic:/matita/Reverse_complexity/reverse/IF_CF.dec"\ 6IF_CF\ 5/a\ 6 (λi:\ 5a title="Natural numbers" href="cic:/fakeuri.def(1)"\ 6ℕ\ 5/a\ 6.\ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/pair.dec"\ 6pair\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 i) i) (|\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 (s (|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))
+   … (λi.s i \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 s i \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 s i \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/sU.dec"\ 6sU\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"\ 6size_f\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 i) (\ 5a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"\ 6size_f\ 5/a\ 6 (λi.i) i) (\ 5a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"\ 6size_f\ 5/a\ 6 (λi.\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 (s (|i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))) i))) … (Hs_c \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6) (Hs_c \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6) … ))
+  [2: @\ 5a href="cic:/matita/Reverse_complexity/reverse/CFU.dec"\ 6CFU\ 5/a\ 6 [@\ 5a href="cic:/matita/Reverse_complexity/reverse/CF_fst.dec"\ 6CF_fst\ 5/a\ 6 // | // |@Hs_constr]
+  |@(\ 5a href="cic:/matita/arithmetics/bigO/O_ext2.def(4)"\ 6O_ext2\ 5/a\ 6 (λn:\ 5a title="Natural numbers" href="cic:/fakeuri.def(1)"\ 6ℕ\ 5/a\ 6.s n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6\ 5a href="cic:/matita/Reverse_complexity/reverse/sU.dec"\ 6sU\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/size_f.def(3)"\ 6size_f\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 n) n (s n) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (s n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6s n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6s n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6s n))) 
+    [2: #i >\ 5a href="cic:/matita/Reverse_complexity/reverse/size_f_size.def(13)"\ 6size_f_size\ 5/a\ 6 >\ 5a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"\ 6size_of_size\ 5/a\ 6 >\ 5a href="cic:/matita/Reverse_complexity/reverse/size_f_id.def(13)"\ 6size_f_id\ 5/a\ 6 //] 
+   @\ 5a href="cic:/matita/arithmetics/bigO/O_absorbr.def(12)"\ 6O_absorbr\ 5/a\ 6 
+    [%{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6} %{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6} #n #_ >\ 5a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"\ 6commutative_times\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/times_n_1.def(8)"\ 6times_n_1\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le_plus.def(7)"\ 6le_plus\ 5/a\ 6 //
+     @\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_sU.dec"\ 6monotonic_sU\ 5/a\ 6 // 
+    |@\ 5a href="cic:/matita/arithmetics/bigO/O_plus_l.def(10)"\ 6O_plus_l\ 5/a\ 6 @(\ 5a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"\ 6O_plus\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/bigO/O_refl.def(9)"\ 6O_refl\ 5/a\ 6 s)) @(\ 5a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"\ 6O_plus\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/bigO/O_refl.def(9)"\ 6O_refl\ 5/a\ 6 s)) 
+     @(\ 5a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"\ 6O_plus\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/bigO/O_refl.def(9)"\ 6O_refl\ 5/a\ 6 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.
+\ 5img class="anchor" src="icons/tick.png" id="hierarchy_theorem_left"\ 6theorem hierarchy_theorem_left: ∀s1,s2:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+   \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6(s1) \ 5a title="subset" href="cic:/fakeuri.def(1)"\ 6⊆\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6(s2) → \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 s1 \ 5a title="subset" href="cic:/fakeuri.def(1)"\ 6⊆\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/CF.def(4)"\ 6CF\ 5/a\ 6 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 (\ 5a href="cic:/matita/arithmetics/bigO/sub_O_to_O.def(10)"\ 6sub_O_to_O\ 5/a\ 6 … HO) -HO #c1 * #b #Hs1s2 
+%{(c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c1)} %{(\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 a b)} #x #lemax 
+cases (Hs1_i x ?) [2: @(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 …lemax)]
+#y #Hy %{y} @(\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … Hy) >\ 5a href="cic:/matita/arithmetics/nat/associative_times.def(10)"\ 6associative_times\ 5/a\ 6
+@\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 // @Hs1s2 @(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … lemax)
 qed.
\ No newline at end of file

diff --git a/weblib/arithmetics/bounded_quantifiers.ma b/weblib/arithmetics/bounded_quantifiers.ma
new file mode 100644 (file)
index 0000000..6eef112
--- /dev/null
+++ b/weblib/arithmetics/bounded_quantifiers.ma
@@ -0,0 +1,51 @@
+include "arithmetics/nat.ma".
+
+\ 5img class="anchor" src="icons/tick.png" id="decidable_not"\ 6lemma decidable_not: ∀P. \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 P → \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6P).
+#P * #H [%2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] 
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="decidable_or"\ 6lemma decidable_or: ∀P,Q. \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 P → \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 Q → \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (P\ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6Q).
+#P #Q * #HP [#_ %1 %1 // |* #HQ [ %1 %2 // | %2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] 
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="decidable_forall"\ 6lemma decidable_forall: ∀P. (∀i.\ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (P i))→ 
+  ∀n.\ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → P i).
+#P #Hdec #n elim n
+  [%1 #i #lti0 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … lti0) @\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6 //
+  |#m * #H
+    [cases (Hdec m) #HPm
+      [%1 #i #lei0 cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … lei0) #H1
+        [@H @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H1 |>(\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"\ 6injective_S\ 5/a\ 6 … H1) @HPm]
+      |%2 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … HPm) #H1 @H1 //
+      ]
+    |%2 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 #i #leim @H1 @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 //
+    ]
+  ]
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="not_exists_to_forall"\ 6lemma not_exists_to_forall: ∀P,n.
+  \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 P i) → ∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 P i.
+#P #n elim n 
+  [#_ #i #lti0 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … lti0) @\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6 //
+  |#m #Hind #H1 #i #leiS cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … leiS) #H2
+    [@(Hind … (\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 … H2)) @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H1) *
+     #a * #leam #Pa %{a} % // @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 //
+    |@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H1) #Pi %{i} % //
+    ]
+  ]
+qed. 
+ 
+\ 5img class="anchor" src="icons/tick.png" id="not_forall_to_exists"\ 6lemma not_forall_to_exists: ∀P,n. (∀i.\ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (P i)) → 
+  \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → P i) → (\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 (P i)).
+#P #n #decP elim n
+  [* #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @H #i #lti0 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 … lti0) @\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6 //
+  |#m #Hind #H1 cases (decP m) #H2
+    [cases (Hind ?)
+      [#i * #leim #nPi %{i} % // @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 //
+      |@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H1) #H3 #i #leiS cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … leiS)
+        [#ltiS @H3 @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 // |#eqi //]
+      ]
+    |%{m} % //
+    ]
+  ]
+qed.
\ No newline at end of file

diff --git a/weblib/arithmetics/pidgeon_hole.ma b/weblib/arithmetics/pidgeon_hole.ma
new file mode 100644 (file)
index 0000000..e4aed16
--- /dev/null
+++ b/weblib/arithmetics/pidgeon_hole.ma
@@ -0,0 +1,90 @@
+
+include "arithmetics/bounded_quantifiers.ma".
+include "basics/list.ma".
+
+(* A bit of combinatorics *)
+interpretation "list membership" 'mem a l = (mem ? a l).
+
+lemma decidable_mem_nat: ∀n:nat.∀l. decidable (n ∈ l).
+#n #l elim l
+  [%2 % @False_ind |#a #tl #Htl @decidable_or //]
+qed.
+
+lemma length_unique_le: ∀n,l. unique ? l  → (∀x. x ∈ l → x < n) → |l| ≤ n.
+#n elim n 
+  [* // #a #tl #_ #H @False_ind @(absurd (a < 0)) 
+    [@H %1 % | @le_to_not_lt //]
+  |#m #Hind #l #Huni #Hmem <(filter_length2 ? (eqb m) l)
+   lapply (length_filter_eqb … m l Huni) #Hle
+   @(transitive_le ? (1+|filter ? (λx.¬ eqb m x) l|))
+    [@le_plus // 
+    |@le_S_S @Hind
+      [@unique_filter // 
+      |#x #memx cut (x ≤ m)
+        [@le_S_S_to_le @Hmem @(mem_filter … memx)] #Hcut
+       cases(le_to_or_lt_eq … Hcut) // #eqxm @False_ind
+       @(absurd ? eqxm) @sym_not_eq @eqb_false_to_not_eq
+       @injective_notb @(mem_filter_true ???? memx)
+      ]
+    ]
+  ]
+qed.    
+
+lemma eq_length_to_mem : ∀n,l. |l| = S n → unique ? l → 
+  (∀x. x ∈ l → x ≤ n) → n ∈ l.
+#n #l #H1 #H2 #H3 cases (decidable_mem_nat n l) // 
+#H4 @False_ind @(absurd (|l| > n))
+  [>H1 // 
+  |@le_to_not_lt @length_unique_le //
+   #x #memx cases(le_to_or_lt_eq … (H3 x memx)) //
+   #Heq @not_le_to_lt @(not_to_not … H4) #_ <Heq //
+  ]
+qed.
+
+lemma eq_length_to_mem_all: ∀n,l. |l| = n → unique ? l  → 
+  (∀x. x ∈ l → x < n) → ∀i. i < n → i ∈ l.
+#n elim n
+  [#l #_ #_ #_ #i #lti0 @False_ind @(absurd ? lti0 (not_le_Sn_O ?))
+  |#m #Hind #l #H #H1 #H2 #i #lei cases (le_to_or_lt_eq … lei)
+    [#leim @(mem_filter… (λi.¬(eqb m i))) 
+     cases (filter_eqb m … H1)
+      [2: * #H @False_ind @(absurd ?? H) @eq_length_to_mem //
+       #x #memx @le_S_S_to_le @H2 //]
+      * #memm #Hfilter @Hind
+        [@injective_S <H <(filter_length2 ? (eqb m) l) >Hfilter %
+        |@unique_filter @H1
+        |#x #memx cases (le_to_or_lt_eq … (H2 x (mem_filter … memx))) #H3
+          [@le_S_S_to_le @H3
+          |@False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
+           @injective_notb >(mem_filter_true ???? memx) %
+          ]
+      |@le_S_S_to_le @leim
+      ]
+    |#eqi @eq_length_to_mem >eqi [@H |@H1 |#x #Hx @le_S_S_to_le >eqi @H2 //]
+    ]
+  ]
+qed. 
+
+lemma lt_length_to_not_mem: ∀n,l. unique ? l  → (∀x. x ∈ l → x < n) → |l| < n →
+∃i. i < n ∧ ¬ (i ∈ l). 
+#n elim n
+  [#l #_ #_ #H @False_ind /2/
+  |#m #Hind #l #Huni #Hmem #Hlen cases (filter_eqb m … Huni)
+    [2: * #H #_ %{m} % //
+    |* #memm #Hfilter cases (Hind (filter ? (λx. ¬(eqb m x)) l) ? ? ?)
+      [#i * #ltim #memi %{i} % [@le_S // ]
+       @(not_to_not … memi) @mem_filter_l @injective_notb >notb_notb
+       @not_eq_to_eqb_false @sym_not_eq @lt_to_not_eq //
+      |@unique_filter //
+      |#x #memx cases (le_to_or_lt_eq … (Hmem x ?))
+        [#H @le_S_S_to_le @H
+        |#H @False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
+         @injective_notb >(mem_filter_true ???? memx) %
+        |@(mem_filter … memx)
+        ]
+      |<(filter_length2 … (eqb m)) in Hlen; >Hfilter #H
+       @le_S_S_to_le @H
+      ]
+    ]
+  ]
+qed.
\ No newline at end of file

diff --git a/weblib/basics/append.ma b/weblib/basics/append.ma
new file mode 100644 (file)
index 0000000..5fe5dce
--- /dev/null
+++ b/weblib/basics/append.ma
@@ -0,0 +1 @@
+(* new script *)
\ No newline at end of file

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index d542416c48c27885fb6e04d1df354e0b342f3ba0..49cc0a5afc548a567fe03d138d4c2649ab5b0aae 100644 (file)
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -11,7 +11,7 @@
 
 include "arithmetics/nat.ma".
 
-\ 5img class="anchor" src="icons/tick.png" id="list"\ 6inductive list (A:Type[0]) : Type[0] :=
+inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
   | cons: A -> list A -> list A.
 
@@ -30,10 +30,10 @@ notation "hvbox(l1 break @ l2)"
 interpretation "nil" 'nil = (nil ?).
 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
-\ 5img class="anchor" src="icons/tick.png" id="not_nil"\ 6definition not_nil: ∀A:Type[0].\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
+definition not_nil: ∀A:Type[0].\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
  λA.λl.match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons hd tl ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 ].
 
-\ 5img class="anchor" src="icons/tick.png" id="nil_cons"\ 6theorem nil_cons:
+theorem nil_cons:
   ∀A:Type[0].∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
   #A #l #a @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq (change with (\ 5a href="cic:/matita/basics/list/not_nil.def(1)"\ 6not_nil\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l))) >Heq //
 qed.
@@ -44,23 +44,23 @@ let rec id_list A (l: list A) on l :=
   [ nil => []
   | (cons hd tl) => hd :: id_list A tl ]. *)
 
-\ 5img class="anchor" src="icons/tick.png" id="append"\ 6let rec append A (l1: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝ 
+let rec append A (l1: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
   | cons hd tl ⇒  hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 append A tl l2 ].
 
-\ 5img class="anchor" src="icons/tick.png" id="hd"\ 6definition hd ≝ λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
+definition hd ≝ λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
   match l with [ nil ⇒ d | cons a _ ⇒ a].
 
-\ 5img class="anchor" src="icons/tick.png" id="tail"\ 6definition tail ≝  λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+definition tail ≝  λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
   match l with [ nil ⇒  \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 | cons hd tl ⇒  tl].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
-\ 5img class="anchor" src="icons/tick.png" id="append_nil"\ 6theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
 #A #l (elim l) normalize // qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="associative_append"\ 6theorem associative_append: 
+theorem associative_append: 
  ∀A.\ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/append.fix(0,1,1)"\ 6append\ 5/a\ 6 A).
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
@@ -70,51 +70,51 @@ ntheorem cons_append_commute:
     a :: (l1 @ l2) = (a :: l1) @ l2.
 //; nqed. *)
 
-\ 5img class="anchor" src="icons/tick.png" id="append_cons"\ 6theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6))\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5span class="autotactic"\ 6\ 5/span\ 6
+theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6))\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5span class="autotactic"\ 6\ 5/span\ 6
 #A #a #l1 #l2 >\ 5a href="cic:/matita/basics/list/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 // qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="nil_append_elim"\ 6theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop. 
+theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop. 
   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) → P l1 l2.
 #A #l1 #l2 #P (cases l1) normalize //
 #a #l3 #heq destruct
 qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="nil_to_nil"\ 6theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
   l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
 #A #l1 #l2 #isnil @(\ 5a href="cic:/matita/basics/list/nil_append_elim.def(4)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
 (* iterators *)
 
-\ 5img class="anchor" src="icons/tick.png" id="map"\ 6let rec map (A,B:Type[0]) (f: A → B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
+let rec map (A,B:Type[0]) (f: A → B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
  match l with [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ? | cons x tl ⇒ f x \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 (map A B f tl)].
   
-\ 5img class="anchor" src="icons/tick.png" id="map_append"\ 6lemma map_append : ∀A,B,f,l1,l2.
+lemma map_append : ∀A,B,f,l1,l2.
   (\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l1) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f (l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2).
 #A #B #f #l1 elim l1
 [ #l2 @\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6
 | #h #t #IH #l2 normalize //
 ] qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="foldr"\ 6let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝  
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝  
  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
  
-\ 5img class="anchor" src="icons/tick.png" id="filter"\ 6definition filter ≝ 
+definition filter ≝ 
   λT.λp:T → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
   \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T) (λx,l0.if (p x) then (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l0) else l0) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 T).
 
-\ 5img class="anchor" src="icons/tick.png" id="compose"\ 6definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
     \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 ?? (λi,acc.(\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? (f i) l2)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6acc) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 l1. 
 
-\ 5img class="anchor" src="icons/tick.png" id="filter_true"\ 6lemma filter_true : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
+lemma filter_true : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
   \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="filter_false"\ 6lemma filter_false : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → 
+lemma filter_false : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → 
   \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="eq_map"\ 6theorem eq_map : ∀A,B,f,g,l. (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
+theorem eq_map : ∀A,B,f,g,l. (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 
 (*
@@ -125,39 +125,39 @@ match l1 with
   ]. *)
 
 (**************************** reverse *****************************)
-\ 5img class="anchor" src="icons/tick.png" id="rev_append"\ 6let rec rev_append S (l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S) on l1 ≝
+let rec rev_append S (l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S) on l1 ≝
   match l1 with 
   [ nil ⇒ l2
   | cons a tl ⇒ rev_append S tl (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2)
   ]
 .
 
-\ 5img class="anchor" src="icons/tick.png" id="reverse"\ 6definition reverse ≝λS.λl.\ 5a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
+definition reverse ≝λS.λl.\ 5a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
 
-\ 5img class="anchor" src="icons/tick.png" id="reverse_single"\ 6lemma reverse_single : ∀S,a. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6). 
+lemma reverse_single : ∀S,a. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6). 
 // qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="rev_append_def"\ 6lemma rev_append_def : ∀S,l1,l2. 
+lemma rev_append_def : ∀S,l1,l2. 
   \ 5a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l1 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l1) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l2 .
 #S #l1 elim l1 normalize // 
 qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="reverse_cons"\ 6lemma reverse_cons : ∀S,a,l. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6).
+lemma reverse_cons : ∀S,a,l. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6).
 #S #a #l whd in ⊢ (??%?); // 
 qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="reverse_append"\ 6lemma reverse_append: ∀S,l1,l2. 
+lemma reverse_append: ∀S,l1,l2. 
   \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (l1 \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l2)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l1).
 #S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >\ 5a href="cic:/matita/basics/list/reverse_cons.def(7)"\ 6reverse_cons\ 5/a\ 6
 >\ 5a href="cic:/matita/basics/list/reverse_cons.def(7)"\ 6reverse_cons\ 5/a\ 6 // qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="reverse_reverse"\ 6lemma reverse_reverse : ∀S,l. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+lemma reverse_reverse : ∀S,l. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
 #S #l elim l // #a #tl #Hind >\ 5a href="cic:/matita/basics/list/reverse_cons.def(7)"\ 6reverse_cons\ 5/a\ 6 >\ 5a href="cic:/matita/basics/list/reverse_append.def(8)"\ 6reverse_append\ 5/a\ 6 
 normalize // qed.
 
 (* an elimination principle for lists working on the tail;
 useful for strings *)
-\ 5img class="anchor" src="icons/tick.png" id="list_elim_left"\ 6lemma list_elim_left: ∀S.∀P:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S → Prop. P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 S) →
+lemma list_elim_left: ∀S.∀P:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S → Prop. P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 S) →
 (∀a.∀tl.P tl → P (tl\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6))) → ∀l. P l.
 #S #P #Pnil #Pstep #l <(\ 5a href="cic:/matita/basics/list/reverse_reverse.def(9)"\ 6reverse_reverse\ 5/a\ 6 … l) 
 generalize in match (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l); #l elim l //
@@ -166,7 +166,7 @@ qed.
 
 (**************************** length *******************************)
 
-\ 5img class="anchor" src="icons/tick.png" id="length"\ 6let rec length (A:Type[0]) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝ 
+let rec length (A:Type[0]) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝ 
   match l with 
     [ nil ⇒ \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6
     | cons a tl ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (length A tl)].
@@ -174,19 +174,19 @@ qed.
 notation "|M|" non associative with precedence 60 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
-\ 5img class="anchor" src="icons/tick.png" id="length_append"\ 6lemma length_append: ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. 
+lemma length_append: ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. 
   \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l1\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l2\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
 #A #l1 elim l1 // normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
 qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="nth"\ 6let rec nth n (A:Type[0]) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (d:A)  ≝  
+let rec nth n (A:Type[0]) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (d:A)  ≝  
   match n with
     [O ⇒ \ 5a href="cic:/matita/basics/list/hd.def(1)"\ 6hd\ 5/a\ 6 A l d
     |S m ⇒ nth m A (\ 5a href="cic:/matita/basics/list/tail.def(1)"\ 6tail\ 5/a\ 6 A l) d].
 
 (***************************** fold *******************************)
 
-\ 5img class="anchor" src="icons/tick.png" id="fold"\ 6let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝  
+let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝  
  match l with 
   [ nil ⇒ b 
   | cons a l ⇒ if (p a) then (op (f a) (fold A B op b p f l))
@@ -203,19 +203,19 @@ for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 
 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 
-\ 5img class="anchor" src="icons/tick.png" id="fold_true"\ 6theorem fold_true: 
+theorem fold_true: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → 
   \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
     op (f a) \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i). 
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="fold_false"\ 6theorem fold_false: 
+theorem fold_false: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
 p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
   \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i).
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="fold_filter"\ 6theorem fold_filter: 
+theorem fold_filter: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
   \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 
     \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l)\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i).
@@ -225,14 +225,14 @@ p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic
   | >\ 5a href="cic:/matita/basics/list/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_false.def(3)"\ 6fold_false\ 5/a\ 6 // ]
 qed.
 
-\ 5img class="anchor" src="icons/tick.png" id="Aop"\ 6record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+record Aop (A:Type[0]) (nil:A) : Type[0] ≝
   {op :2> A → A → A; 
    nill:∀a. op nil a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a; 
    nilr:∀a. op a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
    assoc: ∀a,b,c.op a (op b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 op (op a b) c
   }.
 
-\ 5img class="anchor" src="icons/tick.png" id="fold_sum"\ 6theorem fold_sum: ∀A,B. ∀I,J:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀nil.∀op:\ 5a href="cic:/matita/basics/list/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f.
+theorem fold_sum: ∀A,B. ∀I,J:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀nil.∀op:\ 5a href="cic:/matita/basics/list/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f.
   op (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈I\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i)) (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈J\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
     \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈(I\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6J)\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 

diff --git a/weblib/basics/lists/append.ma b/weblib/basics/lists/append.ma
new file mode 100644 (file)
index 0000000..73fbd36
--- /dev/null
+++ b/weblib/basics/lists/append.ma
@@ -0,0 +1,52 @@
+(* append *)
+
+include "basics/lists/lists.ma".
+include "basics/relations.ma".
+
+\ 5img class="anchor" src="icons/tick.png" id="append"\ 6let rec append A (l1: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝ 
+  match l1 with
+  [ nil ⇒  l2
+  | cons hd tl ⇒  hd :\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 append A tl l2 ].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+\ 5img class="anchor" src="icons/tick.png" id="append_nil"\ 6theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+#A #l (elim l) normalize // qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="associative_append"\ 6theorem associative_append: 
+ ∀A.\ 5font class="Apple-style-span" color="#FF0000"\ 6\ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 \ 5/font\ 6(\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/lists/append/append.fix(0,1,1)"\ 6append\ 5/a\ 6 A).
+#A #l1 #l2 #l3 (elim l1) normalize // qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="append_cons"\ 6theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.
+#A #a #l #l1 >\ 5a href="cic:/matita/basics/lists/append/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 // qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="nil_append_elim"\ 6theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop. 
+  l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6[\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → P (\ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) → P l1 l2.
+#A #l1 #l2 #P (cases l1) normalize //
+#a #l3 #heq destruct
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="nil_to_nil"\ 6theorem nil_to_nil:  ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+  l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
+#A #l1 #l2 #isnil @(\ 5a href="cic:/matita/basics/lists/append/nil_append_elim.def(4)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
+
+(* comparing lists *)
+
+\ 5img class="anchor" src="icons/tick.png" id="compare_append"\ 6lemma compare_append : ∀A,l1,l2,l3,l4. l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l3\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l4 → 
+∃l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6(l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l3\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l4\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2) \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 (l3 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l4).
+#A #l1 elim l1
+  [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
+  |#a1 #tl1 #Hind #l2 #l3 cases l3
+    [#l4 #Heq %{(a1:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl1)} %1 % // @\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"\ 6sym_eq\ 5/a\ 6 @Heq 
+    |#a3 #tl3 #l4 normalize in ⊢ (%→?); #Heq cases (Hind l2 tl3 l4 ?)
+      [#l * * #Heq1 #Heq2 %{l}
+        [%1 % // >Heq1 >(\ 5a href="cic:/matita/basics/lists/lists/cons_injective_l.def(4)"\ 6cons_injective_l\ 5/a\ 6 ????? Heq) //
+        |%2 % // >Heq1 >(\ 5a href="cic:/matita/basics/lists/lists/cons_injective_l.def(4)"\ 6cons_injective_l\ 5/a\ 6 ????? Heq) //
+        ]
+      |@(\ 5a href="cic:/matita/basics/lists/lists/cons_injective_r.def(4)"\ 6cons_injective_r\ 5/a\ 6 ????? Heq) 
+      ]
+    ]
+  ]
+qed.
+

diff --git a/weblib/basics/lists/iterators.ma b/weblib/basics/lists/iterators.ma
new file mode 100644 (file)
index 0000000..d4497a1
--- /dev/null
+++ b/weblib/basics/lists/iterators.ma
@@ -0,0 +1,35 @@
+(**************************** iterators ******************************)
+
+include "basics/lists/append.ma".
+
+let rec map (A,B:Type[0]) (f: A \ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6→\ 5/span\ 6 B) (l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
+ match l with [ nil ⇒ \ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ? | cons x tl ⇒ f x \ 5font class="Apple-style-span" color="#FF0000"\ 6:\ 5/font\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6 (map A B f tl)].
+
+lemma map_append : ∀A,B,f,l1,l2.
+  (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
+#A #B #f #l1 elim l1 [ #l2 @refl | #h #t #IH #l2 normalize //] 
+qed.
+  
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
+ match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
+ 
+definition filter ≝ 
+  λT.λp:T → bool.
+  foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
+
+(* compose f [a1;...;an] [b1;...;bm] = 
+  [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
+ 
+definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+    foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
+
+lemma filter_true : ∀A,l,a,p. p a = true → 
+  filter A p (a::l) = a :: filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+lemma filter_false : ∀A,l,a,p. p a = false → 
+  filter A p (a::l) = filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+#A #B #f #g #l #eqfg (elim l) normalize // qed.
\ No newline at end of file

diff --git a/weblib/basics/lists/lists.ma b/weblib/basics/lists/lists.ma
new file mode 100644 (file)
index 0000000..ba7e484
--- /dev/null
+++ b/weblib/basics/lists/lists.ma
@@ -0,0 +1,47 @@
+(* Definition of list *)
+
+include "basics/logic.ma".
+
+\ 5img class="anchor" src="icons/tick.png" id="list"\ 6inductive list (A:Type[0]) : Type[0] :=
+  | nil: list A
+  | cons: A -> list A -> list A.
+
+notation "hvbox(hd break :: tl)"
+  right associative with precedence 47
+  for @{'cons $hd $tl}.
+
+notation "[ list0 term 19 x sep ; ]"
+  non associative with precedence 90
+  for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+  right associative with precedence 47
+  for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+
+\ 5img class="anchor" src="icons/tick.png" id="is_nil"\ 6definition is_nil: ∀A:Type[0].\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
+ λA.λl.match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons hd tl ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 ].
+
+\ 5img class="anchor" src="icons/tick.png" id="nil_cons"\ 6theorem nil_cons:
+  ∀A:Type[0].∀l:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
+  #A #l #a @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq (change with (\ 5a href="cic:/matita/basics/lists/lists/is_nil.def(1)"\ 6is_nil\ 5/a\ 6 ? (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l))) >Heq //
+qed.
+
+(* hd and tail *)
+\ 5img class="anchor" src="icons/tick.png" id="hd"\ 6definition hd ≝ λA.λl: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
+  match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+\ 5img class="anchor" src="icons/tick.png" id="tail"\ 6definition tail ≝  λA.λl: \ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+  match l with [ nil ⇒  [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 | cons hd tl ⇒  tl].
+
+(* injectivity *) 
+
+\ 5img class="anchor" src="icons/tick.png" id="cons_injective_l"\ 6lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a2:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2 → a1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="cons_injective_r"\ 6lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a2:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2 → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l2.
+#A #a1 #a2 #l1 #l2 #Heq destruct //
+qed.