-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]
-@IF_CF_new [2,3:@(monotonic_CF … (Hs_c ?)) @O_plus_l //]
-@CFU_new
- [@CF_fst @(monotonic_CF … Hs_id) @O_plus_l //
- |@(monotonic_CF … Hs_id) @O_plus_l //
- |@(monotonic_CF … Hs_constr) @O_plus_l //
- |@O_plus_r %{1} %{0} #n #_ >commutative_times <times_n_1
- @monotonic_sU // >size_f_size >size_of_size //
- ]
-qed. *)
-
-(* proof with old axioms
-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.
-