weblib/Reverse_complexity/reverse.ma

   1
   2 include "arithmetics/nat.ma".
   3 include "basics/types.ma".
   4 include "arithmetics/min_max.ma".
   5 include "arithmetics/bigO.ma".
   6
   7 (*********************************** pairing **********************************)
   8
   9 \ 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.
  10 \ 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.
  11 \ 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.
  12 \ 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.
  13 \ 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.
  14
  15 interpretation "abstract pair" 'pair f g = (pair f g).
  16
  17 (************************ basic complexity notions ****************************)
  18
  19 (* u is the deterministic configuration relation of the universal machine (one
  20    step) *)
  21
  22 \ 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.
  23
  24 \ 5img class="anchor" src="icons/tick.png" id="U"\ 6let rec U c n on n ≝
  25   match n in nat with
  26   [ O ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
  27   | S m ⇒ match \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 c with
  28     [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? c (* halting case *)
  29     | Some c1 ⇒ U c1 m
  30     ]
  31   ].
  32
  33 \ 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.
  34 #i #n #y #H cases n
  35   [normalize #H1 destruct |#m normalize >H normalize #H1 destruct //]
  36 qed.
  37
  38 \ 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 ? .
  39 #n elim n
  40   [#i #y normalize #H destruct (H)
  41   |#m #Hind #i #y normalize
  42    cut (\ 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 title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6c. \ 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,2,1)"\ 6Some\ 5/a\ 6 ? c)
  43     [cases (\ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i) [/\ 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/ | #c %2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ ]]
  44    *[#H >H normalize #H1 destruct (H1) // |* #c #H >H normalize @Hind ]
  45   ]
  46 qed.
  47
  48 \ 5img class="anchor" src="icons/tick.png" id="monotonici_U"\ 6lemma monotonici_U: ∀y,n,m,i.
  49   \ 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.
  50 #y #n #m elim m
  51   [#i normalize #H destruct
  52   |#p #Hind #i <\ 5a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"\ 6plus_n_Sm\ 5/a\ 6 normalize
  53     cut (\ 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 title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6c. \ 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,2,1)"\ 6Some\ 5/a\ 6 ? c)
  54     [cases (\ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i) [/\ 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/ | #c %2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ ]]
  55    *[#H1 >H1 normalize // |* #c #H >H normalize #H1 @Hind //]
  56   ]
  57 qed.
  58
  59 \ 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 →
  60   \ 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.
  61 #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 //
  62 qed.
  63
  64 (* axiom U: nat → nat → option nat. *)
  65 (* axiom monotonic_U: ∀i,n,m,y.n ≤m →
  66    U i n = Some ? y → U i m = Some ? y. *)
  67
  68 \ 5img class="anchor" src="icons/tick.png" id="unique_U"\ 6lemma unique_U: ∀i,n,m,yn,ym.
  69   \ 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.
  70 #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)
  71   [#lenm lapply (\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … lenm Hn) >Hm #HS destruct (HS) //
  72   |#ltmn lapply (\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … n … Hm) [@\ 5a href="cic:/matita/arithmetics/nat/lt_to_le.def(6)"\ 6lt_to_le\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 //]
  73    >Hn #HS destruct (HS) //
  74   ]
  75 qed.
  76
  77 \ 5img class="anchor" src="icons/tick.png" id="code_for"\ 6definition code_for ≝ λf,i.∀x.
  78   \ 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.
  79
  80 \ 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.
  81
  82 interpretation "termination" 'fintersects c r = (terminate c r).
  83
  84 \ 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.
  85
  86 \ 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 →
  87   \ 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.
  88 #f #i #x normalize #H %
  89   [* #n * #y * #H1 #posy %{y} % //
  90    cases (H x) -H #m #H <(H (\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 n m)) [2:@(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … n) //]
  91    @(\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … H1) @(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … m) //
  92   |cases (H x) -H #m #Hm * #y #Hy %{m} %{y} >Hm //
  93   ]
  94 qed.
  95
  96 (******************************* complexity classes ***************************)
  97
  98 \ 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.
  99 \ 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.
 100
 101 interpretation "size" 'card n = (size n).
 102
 103 \ 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.
 104 \ 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.
 105
 106 \ 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.
 107
 108 \ 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.
 109
 110 \ 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
 111   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.
 112 // qed.
 113
 114 \ 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.
 115 #f #n @\ 5a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"\ 6le_to_le_to_eq\ 5/a\ 6
 116   [@\ 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) //
 117   |<(\ 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
 118    @(\ 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) ??)
 119     [@\ 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 //]
 120   ]
 121 qed.
 122
 123 \ 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.
 124 #n @\ 5a href="cic:/matita/arithmetics/nat/le_to_le_to_eq.def(5)"\ 6le_to_le_to_eq\ 5/a\ 6
 125   [@\ 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) //
 126   |<(\ 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
 127    @(\ 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) ??)
 128     [@\ 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 //]
 129   ]
 130 qed.
 131
 132 \ 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.
 133 #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) //
 134 qed.
 135
 136 (* definition def ≝ λf:nat → option nat.λx.∃y. f x = Some ? y.*)
 137
 138 (* C s i means that the complexity of i is O(s) *)
 139
 140 \ 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.
 141   \ 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.
 142
 143 \ 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.
 144
 145 \ 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.
 146 #f #g #s #Hext * #i * #Hcode #HC %{i} %
 147   [#x cases (Hcode x) #a #H %{a} <Hext @H | //]
 148 qed.
 149
 150 \ 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.
 151 #s1 #s2 #f * #c1 * #a #H * #i * #Hcodef #HCs1 %{i} % //
 152 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)}
 153 #x #Hmax cases (H2 x ?) [2:@(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … Hmax)] #y #Hy
 154 %{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)
 155 qed.
 156
 157 (************************** The diagonal language *****************************)
 158
 159 (* the diagonal language used for the hierarchy theorem *)
 160
 161 \ 5img class="anchor" src="icons/tick.png" id="diag"\ 6definition diag ≝ λs,i.
 162   \ 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.
 163
 164 \ 5img class="anchor" src="icons/tick.png" id="equiv_diag"\ 6lemma equiv_diag: ∀s,i.
 165   \ 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.
 166 #s #i %
 167   [whd in ⊢ (%→?); #H % [%{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6} //] % * #x * #y *
 168    #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/
 169   |* * #y cases y //
 170    #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)} % //
 171   ]
 172 qed.
 173
 174 (* Let us define the characteristic function diag_cf for diag, and prove
 175 it correctness *)
 176
 177 \ 5img class="anchor" src="icons/tick.png" id="diag_cf"\ 6definition diag_cf ≝ λs,i.
 178   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
 179   [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
 180   | 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)].
 181
 182 \ 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.
 183 #s #x %
 184   [whd in ⊢ (%→?); #H %{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6} % // whd in ⊢ (??%?); >H //
 185   |* #y * whd in ⊢ (??%?→?→%);
 186    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
 187     [#H destruct
 188     |#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
 189       [>(\ 5a href="cic:/matita/arithmetics/nat/eqb_true_to_eq.def(6)"\ 6eqb_true_to_eq\ 5/a\ 6 … Hx) //
 190       |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 //
 191       ]
 192     ]
 193   ]
 194 qed.
 195
 196 \ 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.
 197 #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
 198 qed.
 199
 200 (******************************************************************************)
 201
 202 \ 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.
 203 #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 //]
 204 #H3 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ?? H3) @H2 @H3
 205 qed.
 206
 207 (* axiom weak_pad : ∀a,∃a0.∀n. a0 < n → ∃b. |〈a,b〉| = n. *)
 208 \ 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.
 209
 210 \ 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 →
 211   \ 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).
 212 #s1 #s2  #H #i * #c * #x0 #H1
 213 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 ?)
 214   [#b #H4 %{b}
 215    cases (H1 〈i,b\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 ?)
 216     [#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 //
 217     |>H4 @(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … H2)
 218     ]
 219   |@(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … H2)
 220   ]
 221 qed.
 222
 223 \ 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).
 224 #s1 #s2 #H1 % * #i * #Hcode_i #Hs2_i
 225 cases (\ 5a href="cic:/matita/Reverse_complexity/reverse/not_included_ex.def(10)"\ 6not_included_ex\ 5/a\ 6  … H1 ? Hs2_i) #b #H2
 226 lapply (\ 5a href="cic:/matita/Reverse_complexity/reverse/diag_spec.def(11)"\ 6diag_spec\ 5/a\ 6 … Hcode_i) #H3
 227 @(\ 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))
 228 @(\ 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))
 229 @(\ 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
 230 %[* #_ // |#H6 % // ]
 231 qed.
 232
 233 (******************************************************************************)
 234 (* definition sumF ≝ λf,g:nat→nat.λn.f n + g n. *)
 235
 236 \ 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).
 237
 238 \ 5img class="anchor" src="icons/tick.png" id="deopt"\ 6definition deopt ≝ λn. match n with
 239   [ None ⇒ \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6
 240   | Some n ⇒ n].
 241
 242 \ 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.
 243   match g x with
 244   [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
 245   | Some y ⇒ f y ].
 246
 247 (* axiom CFU: ∀h,g,s. CF s (to_Some h)  → CF s (to_Some (of_size ∘ g)) →
 248   CF (Slow s) (λx.U (h x) (g x)). *)
 249
 250 \ 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.
 251 \ 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.
 252
 253 (* axiom CFU: CF sU (λx.U (fst x) (snd x)). *)
 254
 255 \ 5img class="anchor" src="icons/tick.png" id="CFU"\ 6axiom CFU: ∀h,g,f,s1,s2,s3.
 256   \ 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) →
 257   \ 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))
 258     (λ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)).
 259
 260 \ 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 →
 261   \ 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.
 262
 263 (* definition sU_space ≝ λi,x,r.i+x+r.
 264 definition sU_time ≝ λi,x,r.i+x+(i^2)*r*(log 2 r). *)
 265
 266 (*
 267 axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g →
 268   CF (λx.s2 x + s1 (size (deopt (g x)))) (opt_comp f g).
 269
 270 (* axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g →
 271   CF (s1 ∘ (λx. size (deopt (g x)))) (opt_comp f g). *)
 272
 273 axiom CF_comp_strong: ∀f,g,s1,s2. CF s1 f → CF s2 g →
 274   CF (s1 ∘ s2) (opt_comp f g). *)
 275
 276 \ 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.
 277   match b x with
 278   [None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
 279   |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].
 280
 281 \ 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 →
 282   \ 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).
 283
 284 \ 5img class="anchor" src="icons/tick.png" id="diag_cf_def"\ 6lemma diag_cf_def : ∀s.∀i.
 285   \ 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
 286     \ 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.
 287 #s #i normalize >\ 5a href="cic:/matita/Reverse_complexity/reverse/size_of_size.dec"\ 6size_of_size\ 5/a\ 6 // qed.
 288
 289 (* and now ... *)
 290 \ 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)) →
 291   \ 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))).
 292
 293 \ 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))).
 294
 295 \ 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).
 296
 297
 298 (*
 299 axiom le_snd: ∀n. |snd n| ≤ |n|.
 300 axiom daemon: ∀P:Prop.P. *)
 301
 302 \ 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)))).
 303
 304 (*
 305 lemma compl1: ∀s.
 306   CF s (to_Some fst)  → CF s (to_Some (λx.x)) → CF s (to_Some (λx.(s (|x|)))) →
 307   CF (λx. s x + s x + s x + sU (size_f fst x) (size_f (λx.x) x) (size_f (λx.(s (|x|))) x))
 308     (λx.U 〈fst x,x〉 (|s (|x|)|)).
 309 #s #H1 #H2 #H3 @CFU //
 310 qed.
 311
 312 lemma compl1: ∀s.
 313   CF s (to_Some fst)  → CF s (to_Some (λx.x)) → CF s (to_Some (λx.(s (|x|)))) →
 314   CF (λx. s x + s x + s x + sU (size_f fst x) (size_f (λx.x) x) (|(s x)| ))
 315     (λx.U 〈fst x,x〉 (|s (|x|)|)).
 316 #s #H1 #H2 #H3 @monotonic_CF [3: @(CFU ??? s s s) @CFU //
 317 qed.  *)
 318
 319 \ 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 →
 320   \ 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).
 321 #s * #Hs_id #Hs_c #Hs_constr
 322 @\ 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]
 323 @(\ 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))
 324    … (λ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) … ))
 325   [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]
 326   |@(\ 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)))
 327     [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 //]
 328    @\ 5a href="cic:/matita/arithmetics/bigO/O_absorbr.def(12)"\ 6O_absorbr\ 5/a\ 6
 329     [%{\ 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 //
 330      @\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_sU.dec"\ 6monotonic_sU\ 5/a\ 6 //
 331     |@\ 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))
 332      @(\ 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)) //
 333   ]
 334 qed.
 335
 336
 337 (*************************** The hierachy theorem *****************************)
 338
 339 (*
 340 theorem hierarchy_theorem_right: ∀s1,s2:nat→nat.
 341   O s1 idN → constructible s1 →
 342     not_O s2 s1 → ¬ CF s1 ⊆ CF s2.
 343 #s1 #s2 #Hs1 #monos1 #H % #H1
 344 @(absurd … (CF s2 (diag_cf s1)))
 345   [@H1 @diag_s // |@(diag1_not_s1 … H)]
 346 qed.
 347 *)
 348
 349 \ 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.
 350    \ 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.
 351 #s1 #s2 #HO #f * #i * #Hcode * #c * #a #Hs1_i %{i} % //
 352 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
 353 %{(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
 354 cases (Hs1_i x ?) [2: @(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 …lemax)]
 355 #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
 356 @\ 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)
 357 qed.