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

diff --git a/weblib/Reverse_complexity/reverse.ma b/weblib/Reverse_complexity/reverse.ma
new file mode 100644
index 000000000..73814b17a
--- /dev/null
+++ b/weblib/Reverse_complexity/reverse.ma
@@ -0,0 +1,359 @@
+
+include "arithmetics/nat.ma".
+include "basics/types.ma".
+include "arithmetics/min_max.ma".
+include "arithmetics/bigO.ma".
+ 
+(*********************************** pairing **********************************) 
+
+axiom pair: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+axiom fst : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+axiom snd : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+axiom fst_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a.
+axiom snd_pair: ∀a,b. a href="cic:/matita/Reverse_complexity/reverse/snd.dec"snd/a (a href="cic:/matita/Reverse_complexity/reverse/pair.dec"pair/a a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b. 
+
+interpretation "abstract pair" 'pair f g = (pair f g).
+
+(************************ basic complexity notions ****************************)
+
+(* u is the deterministic configuration relation of the universal machine (one 
+   step) *)
+
+axiom u: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/basics/types/option.ind(1,0,1)"option/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+
+let rec U c n on n ≝ 
+  match n with  
+  [ O ⇒ a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ?
+  | S m ⇒ match a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a c with 
+    [ None ⇒ a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? c (* halting case *)
+    | Some c1 ⇒ U c1 m
+    ]
+  ].
+ 
+lemma halt_U: ∀i,n,y. a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a i.
+#i #n #y #H cases n
+  [normalize #H1 destruct |#m normalize >H normalize #H1 destruct //]
+qed. 
+
+lemma Some_to_halt: ∀n,i,y. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? .
+#n elim n
+  [#i #y normalize #H destruct (H)
+  |#m #Hind #i #y normalize 
+   cut (a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? a title="logical or" href="cic:/fakeuri.def(1)"∨/a a title="exists" href="cic:/fakeuri.def(1)"∃/ac. a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? c) 
+    [cases (a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i) [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ | #c %2 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a/span/span/ ]] 
+   *[#H >H normalize #H1 destruct (H1) // |* #c #H >H normalize @Hind ]
+  ]
+qed. 
+
+lemma monotonici_U: ∀y,n,m,i.
+  a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i (na title="natural plus" href="cic:/fakeuri.def(1)"+/am) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
+#y #n #m elim m 
+  [#i normalize #H destruct 
+  |#p #Hind #i <a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"plus_n_Sm/a normalize
+    cut (a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,1,1)"None/a ? a title="logical or" href="cic:/fakeuri.def(1)"∨/a a title="exists" href="cic:/fakeuri.def(1)"∃/ac. a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? c) 
+    [cases (a href="cic:/matita/Reverse_complexity/reverse/u.dec"u/a i) [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ | #c %2 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a/span/span/ ]] 
+   *[#H1 >H1 normalize // |* #c #H >H normalize #H1 @Hind //]
+  ]
+qed.
+
+lemma monotonic_U: ∀i,n,m,y.n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am →
+  a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
+#i #n #m #y #lenm #H >(a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a m n) // @a href="cic:/matita/Reverse_complexity/reverse/monotonici_U.def(5)"monotonici_U/a //
+qed.
+
+(* axiom U: nat → nat → option nat. *)
+(* 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.
+  a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? yn → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a i m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? ym → yn a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a ym.
+#i #n #m #yn #ym #Hn #Hm cases (a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a n m)
+  [#lenm lapply (a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … lenm Hn) >Hm #HS destruct (HS) //
+  |#ltmn lapply (a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … n … Hm) [@a href="cic:/matita/arithmetics/nat/lt_to_le.def(6)"lt_to_le/a @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a //]
+   >Hn #HS destruct (HS) //
+  ]
+qed.
+
+definition code_for ≝ λf,i.∀x.
+  a title="exists" href="cic:/fakeuri.def(1)"∃/an.∀m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x.
+
+definition terminate ≝ λc,r. a title="exists" href="cic:/fakeuri.def(1)"∃/ay. a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a c r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y.
+
+interpretation "termination" 'fintersects c r = (terminate c r).
+ 
+definition lang ≝ λi,x.a title="exists" href="cic:/fakeuri.def(1)"∃/ar,ya title="exists" href="cic:/fakeuri.def(1)"./a a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"U/a 〈i,xa title="abstract pair" href="cic:/fakeuri.def(1)"〉/a r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a  a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y. 
+
+lemma lang_cf :∀f,i,x. a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"code_for/a f i → 
+  a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"lang/a i x a title="iff" href="cic:/fakeuri.def(1)"↔/a a title="exists" href="cic:/fakeuri.def(1)"∃/ay.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/types/option.con(0,2,1)"Some/a ? y a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a y.
+#f #i #x normalize #H %
+  [* #n * #y * #H1 #posy %{y} % // 
+   cases (H x) -H #m #H <(H (a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m)) [2:@(a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"le_maxr/a … n) //]
+   @(a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"monotonic_U/a … H1) @(a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"le_maxl/a … m) //
+  |cases (H x) -H #m #Hm * #y #Hy %{m} %{y} >Hm // 
+  ]
+qed.
+
+(******************************* complexity classes ***************************)
+
+axiom size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+axiom of_size: a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+
+interpretation "size" 'card n = (size n).
+
+axiom size_of_size: ∀n. |a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n.
+axiom of_size_max: ∀i,n. |ia title="size" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n → i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"of_size/a n.
+
+axiom size_fst : ∀n. |a href="cic:/matita/Reverse_complexity/reverse/fst.dec"fst/a na title="size" href="cic:/fakeuri.def(1)"|/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a |na title="size" href="cic:/fakeuri.def(1)"|/a.
+
+axiom a : Max0.
+
+definition size_f ≝ λf,n.Max_{ifont class="Apple-style-span" color="#FF0000" < /fontS (of_size n) | eqb (|i|) n }|(f i)|.
+
+lemma size_f_def: ∀f,n. size_f f n = 
+  Max_{i < S (of_size n) | eqb (|i|) n}|(f i)|.
+// 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 //]
+  ]
+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 //]
+  ]
+qed.
+
+lemma size_f_fst : ∀n. size_f fst n ≤ n.
+#n @Max_le #a #lta #Ha <(eqb_true_to_eq  … 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.
+
+definition CF ≝ λs,f.∃i.code_for f i ∧ C s i.
+
+lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF 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.
+#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)
+qed. 
+
+(************************** The diagonal language *****************************)
+
+(* the diagonal language used for the hierarchy theorem *)
+
+definition diag ≝ λs,i. 
+  U 〈fst i,i〉 (s (|i|)) = Some ? 0. 
+
+lemma equiv_diag: ∀s,i. 
+  diag s i ↔ 〈fst i, i〉 ↓ s (|i|) ∧ ¬lang (fst i) i.
+#s #i %
+  [whd in ⊢ (%→?); #H % [%{0} //] % * #x * #y *
+   #H1 #Hy cut (0 = y) [@(unique_U … H H1)] #eqy /2/
+  |* * #y cases y //
+   #y0 #H * #H1 @False_ind @H1 -H1 whd %{(s (|i|))} %{(S 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)].
+
+lemma diag_cf_OK: ∀s,x. diag s x ↔ ∃y.diag_cf s x = Some ? y ∧ 0 < y.
+#s #x % 
+  [whd in ⊢ (%→?); #H %{1} % // whd in ⊢ (??%?); >H // 
+  |* #y * whd in ⊢ (??%?→?→%); 
+   cases (U 〈fst x,x〉 (s (|x|))) 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 //  
+      ]
+    ]
+  ]
+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
+qed. 
+
+(******************************************************************************)
+
+lemma absurd1: ∀P. iff P (¬ P) →False.
+#P * #H1 #H2 cut (¬P) [% #H2 @(absurd … H2) @H1 //] 
+#H3 @(absurd ?? 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.
+
+lemma not_included_ex: ∀s1,s2. not_O s2 s1 → ∀i. C s2 i →
+  ∃b.〈i, 〈i,b〉〉 ↓ s1 (|〈i,b〉|).
+#s1 #s2  #H #i * #c * #x0 #H1 
+cases (H c (max (S(|i|)) x0)) #x1 * #H2 #H3 cases (pad i x1 ?) 
+  [#b #H4 %{b}
+   cases (H1 〈i,b〉 ?)
+    [#z >H4 #H5 %{z} @(monotonic_U … H5) @lt_to_le //
+    |>H4 @(le_maxr … H2)
+    ]
+  |@(le_maxl … H2)
+  ]
+qed.
+
+lemma diag1_not_s1: ∀s1,s2. not_O s2 s1 → ¬ CF s2 (diag_cf 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 
+%[* #_ // |#H6 % // ]
+qed.
+
+(******************************************************************************)
+(* definition sumF ≝ λf,g:nat→nat.λn.f n + g n. *)
+
+definition to_Some ≝ λf.λx:nat. Some nat (f x).
+
+definition deopt ≝ λn. match n with 
+  [ None ⇒ 1
+  | Some n ⇒ n].
+  
+definition opt_comp ≝ λf,g:nat → option nat. λx.
+  match g x with 
+  [ None ⇒ None ?
+  | 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.
+
+(* 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|)).
+    
+axiom monotonic_sU: ∀a1,a2,b1,b2,c1,c2. a1 ≤ a2 → b1 ≤ b2 → c1 ≤c2 →
+  sU a1 b1 c1 ≤ sU 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).
+
+(*
+axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g → 
+  CF (λx.s2 x + s1 (size (deopt (g x)))) (opt_comp f g).
+
+(* axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g → 
+  CF (s1 ∘ (λx. size (deopt (g x)))) (opt_comp f 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.
+  match b x with 
+  [None ⇒ None ?
+  |Some n ⇒ if (eqb n 0) 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).
+
+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. 
+
+(* 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))).
+
+axiom CF_fst: ∀f,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (fst (f x))).
+
+definition minimal ≝ λs. CF s (λn. Some ? n) ∧ ∀c. CF s (λn. Some ? c).
+
+
+(*
+axiom le_snd: ∀n. |snd n| ≤ |n|.
+axiom daemon: ∀P:Prop.P. *)
+
+definition constructible ≝ λs. CF s (λx.Some ? (of_size (s (|x|)))).
+
+(*
+lemma compl1: ∀s. 
+  CF s (to_Some fst)  → CF s (to_Some (λx.x)) → CF s (to_Some (λx.(s (|x|)))) → 
+  CF (λx. s x + s x + s x + sU (size_f fst x) (size_f (λx.x) x) (size_f (λx.(s (|x|))) x)) 
+    (λx.U 〈fst x,x〉 (|s (|x|)|)).
+#s #H1 #H2 #H3 @CFU //
+qed.  
+
+lemma compl1: ∀s. 
+  CF s (to_Some fst)  → CF s (to_Some (λx.x)) → CF s (to_Some (λx.(s (|x|)))) → 
+  CF (λx. s x + s x + s x + sU (size_f fst x) (size_f (λx.x) x) (|(s x)| ))
+    (λx.U 〈fst x,x〉 (|s (|x|)|)).
+#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).
+#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)) //
+  ]
+qed.
+
+  
+(*************************** The hierachy theorem *****************************)
+
+(*
+theorem hierarchy_theorem_right: ∀s1,s2:nat→nat. 
+  O s1 idN → constructible s1 →
+    not_O s2 s1 → ¬ CF s1 ⊆ CF s2.
+#s1 #s2 #Hs1 #monos1 #H % #H1 
+@(absurd … (CF s2 (diag_cf s1)))
+  [@H1 @diag_s // |@(diag1_not_s1 … H)]
+qed.
+*)
+
+theorem hierarchy_theorem_left: ∀s1,s2:nat→nat.
+   O(s1) ⊆ O(s2) → CF s1 ⊆ CF 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)
+qed.
\ No newline at end of file