matita/matita/lib/reverse_complexity/hierarchy.ma

   1
   2 include "arithmetics/nat.ma".
   3 include "arithmetics/log.ma".
   4 (* include "arithmetics/ord.ma". *)
   5 include "arithmetics/bigops.ma".
   6 include "basics/sets.ma".
   7 include "basics/types.ma".
   8
   9 (************************************ MAX *************************************)
  10 notation "Max_{ ident i < n | p } f"
  11   with precedence 80
  12 for @{'bigop $n max 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
  13
  14 notation "Max_{ ident i < n } f"
  15   with precedence 80
  16 for @{'bigop $n max 0 (λ${ident i}.true) (λ${ident i}. $f)}.
  17
  18 notation "Max_{ ident j ∈ [a,b[ } f"
  19   with precedence 80
  20 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
  21   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  22
  23 notation "Max_{ ident j ∈ [a,b[ | p } f"
  24   with precedence 80
  25 for @{'bigop ($b-$a) max 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
  26   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  27
  28 lemma Max_assoc: ∀a,b,c. max (max a b) c = max a (max b c).
  29 #a #b #c normalize cases (true_or_false (leb a b)) #leab >leab normalize
  30   [cases (true_or_false (leb b c )) #lebc >lebc normalize
  31     [>(le_to_leb_true a c) // @(transitive_le ? b) @leb_true_to_le //
  32     |>leab //
  33     ]
  34   |cases (true_or_false (leb b c )) #lebc >lebc normalize //
  35    >leab normalize >(not_le_to_leb_false a c) // @lt_to_not_le
  36    @(transitive_lt ? b) @not_le_to_lt @leb_false_to_not_le //
  37   ]
  38 qed.
  39
  40 lemma Max0 : ∀n. max 0 n = n.
  41 // qed.
  42
  43 lemma Max0r : ∀n. max n 0 = n.
  44 #n >commutative_max //
  45 qed.
  46
  47 definition MaxA ≝
  48   mk_Aop nat 0 max Max0 Max0r (λa,b,c.sym_eq … (Max_assoc a b c)).
  49
  50 definition MaxAC ≝ mk_ACop nat 0 MaxA commutative_max.
  51
  52 lemma le_Max: ∀f,p,n,a. a < n → p a = true →
  53   f a ≤  Max_{i < n | p i}(f i).
  54 #f #p #n #a #ltan #pa
  55 >(bigop_diff p ? 0 MaxAC f a n) // @(le_maxl … (le_n ?))
  56 qed.
  57
  58 lemma Max_le: ∀f,p,n,b.
  59   (∀a.a < n → p a = true → f a ≤ b) → Max_{i < n | p i}(f i) ≤ b.
  60 #f #p #n elim n #b #H //
  61 #b0 #H1 cases (true_or_false (p b)) #Hb
  62   [>bigop_Strue [2:@Hb] @to_max [@H1 // | @H #a #ltab #pa @H1 // @le_S //]
  63   |>bigop_Sfalse [2:@Hb] @H #a #ltab #pa @H1 // @le_S //
  64   ]
  65 qed.
  66
  67 (******************************** big O notation ******************************)
  68
  69 (*  O f g means g ∈ O(f) *)
  70 definition O: relation (nat→nat) ≝
  71   λf,g. ∃c.∃n0.∀n. n0 ≤ n → g n ≤ c* (f n).
  72
  73 lemma O_refl: ∀s. O s s.
  74 #s %{1} %{0} #n #_ >commutative_times <times_n_1 @le_n qed.
  75
  76 lemma O_trans: ∀s1,s2,s3. O s2 s1 → O s3 s2 → O s3 s1.
  77 #s1 #s2 #s3 * #c1 * #n1 #H1 * #c2 * # n2 #H2 %{(c1*c2)}
  78 %{(max n1 n2)} #n #Hmax
  79 @(transitive_le … (H1 ??)) [@(le_maxl … Hmax)]
  80 >associative_times @le_times [//|@H2 @(le_maxr … Hmax)]
  81 qed.
  82
  83 lemma sub_O_to_O: ∀s1,s2. O s1 ⊆ O s2 → O s2 s1.
  84 #s1 #s2 #H @H // qed.
  85
  86 lemma O_to_sub_O: ∀s1,s2. O s2 s1 → O s1 ⊆ O s2.
  87 #s1 #s2 #H #g #Hg @(O_trans … H) // qed.
  88
  89 definition sum_f ≝ λf,g:nat→nat.λn.f n + g n.
  90 interpretation "function sum" 'plus f g = (sum_f f g).
  91
  92 lemma O_plus: ∀f,g,s. O s f → O s g → O s (f+g).
  93 #f #g #s * #cf * #nf #Hf * #cg * #ng #Hg
  94 %{(cf+cg)} %{(max nf ng)} #n #Hmax normalize
  95 >distributive_times_plus_r @le_plus
  96   [@Hf @(le_maxl … Hmax) |@Hg @(le_maxr … Hmax) ]
  97 qed.
  98
  99 lemma O_plus_l: ∀f,s1,s2. O s1 f → O (s1+s2) f.
 100 #f #s1 #s2 * #c * #a #Os1f %{c} %{a} #n #lean
 101 @(transitive_le … (Os1f n lean)) @le_times //
 102 qed.
 103
 104 lemma O_absorbl: ∀f,g,s. O s f → O f g → O s (g+f).
 105 #f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) //
 106 qed.
 107
 108 lemma O_absorbr: ∀f,g,s. O s f → O f g → O s (f+g).
 109 #f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) //
 110 qed.
 111
 112 (*
 113 lemma O_ff: ∀f,s. O s f → O s (f+f).
 114 #f #s #Osf /2/
 115 qed. *)
 116
 117 lemma O_ext2: ∀f,g,s. O s f → (∀x.f x = g x) → O s g.
 118 #f #g #s * #c * #a #Osf #eqfg %{c} %{a} #n #lean <eqfg @Osf //
 119 qed.
 120
 121
 122 definition not_O ≝ λf,g.∀c,n0.∃n. n0 ≤ n ∧ c* (f n) < g n .
 123
 124 (* this is the only classical result *)
 125 axiom not_O_def: ∀f,g. ¬ O f g → not_O f g.
 126
 127 (*********************************** pairing **********************************)
 128
 129 axiom pair: nat →nat →nat.
 130 axiom fst : nat → nat.
 131 axiom snd : nat → nat.
 132 axiom fst_pair: ∀a,b. fst (pair a b) = a.
 133 axiom snd_pair: ∀a,b. snd (pair a b) = b.
 134
 135 interpretation "abstract pair" 'pair f g = (pair f g).
 136
 137 (************************ basic complexity notions ****************************)
 138
 139 (* u is the deterministic configuration relation of the universal machine (one
 140    step) *)
 141
 142 axiom u: nat → option nat.
 143
 144 let rec U c n on n ≝
 145   match n with
 146   [ O ⇒ None ?
 147   | S m ⇒ match u c with
 148     [ None ⇒ Some ? c (* halting case *)
 149     | Some c1 ⇒ U c1 m
 150     ]
 151   ].
 152
 153 lemma halt_U: ∀i,n,y. u i = None ? → U i n = Some ? y → y = i.
 154 #i #n #y #H cases n
 155   [normalize #H1 destruct |#m normalize >H normalize #H1 destruct //]
 156 qed.
 157
 158 lemma Some_to_halt: ∀n,i,y. U i n = Some ? y → u y = None ? .
 159 #n elim n
 160   [#i #y normalize #H destruct (H)
 161   |#m #Hind #i #y normalize
 162    cut (u i = None ? ∨ ∃c. u i = Some ? c)
 163     [cases (u i) [/2/ | #c %2 /2/ ]]
 164    *[#H >H normalize #H1 destruct (H1) // |* #c #H >H normalize @Hind ]
 165   ]
 166 qed.
 167
 168 lemma monotonici_U: ∀y,n,m,i.
 169   U i m = Some ? y → U i (n+m) = Some ? y.
 170 #y #n #m elim m
 171   [#i normalize #H destruct
 172   |#p #Hind #i <plus_n_Sm normalize
 173     cut (u i = None ? ∨ ∃c. u i = Some ? c)
 174     [cases (u i) [/2/ | #c %2 /2/ ]]
 175    *[#H1 >H1 normalize // |* #c #H >H normalize #H1 @Hind //]
 176   ]
 177 qed.
 178
 179 lemma monotonic_U: ∀i,n,m,y.n ≤m →
 180   U i n = Some ? y → U i m = Some ? y.
 181 #i #n #m #y #lenm #H >(plus_minus_m_m m n) // @monotonici_U //
 182 qed.
 183
 184 (* axiom U: nat → nat → option nat. *)
 185 (* axiom monotonic_U: ∀i,n,m,y.n ≤m →
 186    U i n = Some ? y → U i m = Some ? y. *)
 187
 188 lemma unique_U: ∀i,n,m,yn,ym.
 189   U i n = Some ? yn → U i m = Some ? ym → yn = ym.
 190 #i #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
 191   [#lenm lapply (monotonic_U … lenm Hn) >Hm #HS destruct (HS) //
 192   |#ltmn lapply (monotonic_U … n … Hm) [@lt_to_le @not_le_to_lt //]
 193    >Hn #HS destruct (HS) //
 194   ]
 195 qed.
 196
 197 definition code_for ≝ λf,i.∀x.
 198   ∃n.∀m. n ≤ m → U 〈i,x〉 m = f x.
 199
 200 definition terminate ≝ λc,r. ∃y. U c r = Some ? y.
 201
 202 interpretation "termination" 'fintersects c r = (terminate c r).
 203
 204 definition lang ≝ λi,x.∃r,y. U 〈i,x〉 r = Some ? y ∧ 0  < y.
 205
 206 lemma lang_cf :∀f,i,x. code_for f i →
 207   lang i x ↔ ∃y.f x = Some ? y ∧ 0 < y.
 208 #f #i #x normalize #H %
 209   [* #n * #y * #H1 #posy %{y} % //
 210    cases (H x) -H #m #H <(H (max n m)) [2:@(le_maxr … n) //]
 211    @(monotonic_U … H1) @(le_maxl … m) //
 212   |cases (H x) -H #m #Hm * #y #Hy %{m} %{y} >Hm //
 213   ]
 214 qed.
 215
 216 (******************************* complexity classes ***************************)
 217
 218 axiom size: nat → nat.
 219 axiom of_size: nat → nat.
 220
 221 interpretation "size" 'card n = (size n).
 222
 223 axiom size_of_size: ∀n. |of_size n| = n.
 224 axiom of_size_max: ∀i,n. |i| = n → i ≤ of_size n.
 225
 226 axiom size_fst : ∀n. |fst n| ≤ |n|.
 227
 228 definition size_f ≝ λf,n.Max_{i < S (of_size n) | eqb (|i|) n}|(f i)|.
 229
 230 lemma size_f_def: ∀f,n. size_f f n =
 231   Max_{i < S (of_size n) | eqb (|i|) n}|(f i)|.
 232 // qed.
 233
 234 (*
 235 definition Max_const : ∀f,p,n,a. a < n → p a →
 236   ∀n. f n = g n →
 237   Max_{i < n | p n}(f n) = *)
 238
 239 lemma size_f_size : ∀f,n. size_f (f ∘ size) n = |(f n)|.
 240 #f #n @le_to_le_to_eq
 241   [@Max_le #a #lta #Ha normalize >(eqb_true_to_eq  … Ha) //
 242   |<(size_of_size n) in ⊢ (?%?); >size_f_def
 243    @(le_Max (λi.|f (|i|)|) ? (S (of_size n)) (of_size n) ??)
 244     [@le_S_S // | @eq_to_eqb_true //]
 245   ]
 246 qed.
 247
 248 lemma size_f_id : ∀n. size_f (λx.x) n = n.
 249 #n @le_to_le_to_eq
 250   [@Max_le #a #lta #Ha >(eqb_true_to_eq  … Ha) //
 251   |<(size_of_size n) in ⊢ (?%?); >size_f_def
 252    @(le_Max (λi.|i|) ? (S (of_size n)) (of_size n) ??)
 253     [@le_S_S // | @eq_to_eqb_true //]
 254   ]
 255 qed.
 256
 257 lemma size_f_fst : ∀n. size_f fst n ≤ n.
 258 #n @Max_le #a #lta #Ha <(eqb_true_to_eq  … Ha) //
 259 qed.
 260
 261 (* definition def ≝ λf:nat → option nat.λx.∃y. f x = Some ? y.*)
 262
 263 (* C s i means that the complexity of i is O(s) *)
 264
 265 definition C ≝ λs,i.∃c.∃a.∀x.a ≤ |x| → ∃y.
 266   U 〈i,x〉 (c*(s(|x|))) = Some ? y.
 267
 268 definition CF ≝ λs,f.∃i.code_for f i ∧ C s i.
 269
 270 lemma ext_CF : ∀f,g,s. (∀n. f n = g n) → CF s f → CF s g.
 271 #f #g #s #Hext * #i * #Hcode #HC %{i} %
 272   [#x cases (Hcode x) #a #H %{a} <Hext @H | //]
 273 qed.
 274
 275 lemma monotonic_CF: ∀s1,s2,f. O s2 s1 → CF s1 f → CF s2 f.
 276 #s1 #s2 #f * #c1 * #a #H * #i * #Hcodef #HCs1 %{i} % //
 277 cases HCs1 #c2 * #b #H2 %{(c2*c1)} %{(max a b)}
 278 #x #Hmax cases (H2 x ?) [2:@(le_maxr … Hmax)] #y #Hy
 279 %{y} @(monotonic_U …Hy) >associative_times @le_times // @H @(le_maxl … Hmax)
 280 qed.
 281
 282 (************************** The diagonal language *****************************)
 283
 284 (* the diagonal language used for the hierarchy theorem *)
 285
 286 definition diag ≝ λs,i.
 287   U 〈fst i,i〉 (s (|i|)) = Some ? 0.
 288
 289 lemma equiv_diag: ∀s,i.
 290   diag s i ↔ 〈fst i, i〉 ↓ s (|i|) ∧ ¬lang (fst i) i.
 291 #s #i %
 292   [whd in ⊢ (%→?); #H % [%{0} //] % * #x * #y *
 293    #H1 #Hy cut (0 = y) [@(unique_U … H H1)] #eqy /2/
 294   |* * #y cases y //
 295    #y0 #H * #H1 @False_ind @H1 -H1 whd %{(s (|i|))} %{(S y0)} % //
 296   ]
 297 qed.
 298
 299 (* Let us define the characteristic function diag_cf for diag, and prove
 300 it correctness *)
 301
 302 definition diag_cf ≝ λs,i.
 303   match U 〈fst i,i〉 (s (|i|)) with
 304   [ None ⇒ None ?
 305   | Some y ⇒ if (eqb y 0) then (Some ? 1) else (Some ? 0)].
 306
 307 lemma diag_cf_OK: ∀s,x. diag s x ↔ ∃y.diag_cf s x = Some ? y ∧ 0 < y.
 308 #s #x %
 309   [whd in ⊢ (%→?); #H %{1} % // whd in ⊢ (??%?); >H //
 310   |* #y * whd in ⊢ (??%?→?→%);
 311    cases (U 〈fst x,x〉 (s (|x|))) normalize
 312     [#H destruct
 313     |#x cases (true_or_false (eqb x 0)) #Hx >Hx
 314       [>(eqb_true_to_eq … Hx) //
 315       |normalize #H destruct #H @False_ind @(absurd ? H) @lt_to_not_le //
 316       ]
 317     ]
 318   ]
 319 qed.
 320
 321 lemma diag_spec: ∀s,i. code_for (diag_cf s) i → ∀x. lang i x ↔ diag s x.
 322 #s #i #Hcode #x @(iff_trans  … (lang_cf … Hcode)) @iff_sym @diag_cf_OK
 323 qed.
 324
 325 (******************************************************************************)
 326
 327 lemma absurd1: ∀P. iff P (¬ P) →False.
 328 #P * #H1 #H2 cut (¬P) [% #H2 @(absurd … H2) @H1 //]
 329 #H3 @(absurd ?? H3) @H2 @H3
 330 qed.
 331
 332 (* axiom weak_pad : ∀a,∃a0.∀n. a0 < n → ∃b. |〈a,b〉| = n. *)
 333 axiom pad : ∀a,n. |a| < n → ∃b. |〈a,b〉| = n.
 334
 335 lemma not_included_ex: ∀s1,s2. not_O s2 s1 → ∀i. C s2 i →
 336   ∃b.〈i, 〈i,b〉〉 ↓ s1 (|〈i,b〉|).
 337 #s1 #s2  #H #i * #c * #x0 #H1
 338 cases (H c (max (S(|i|)) x0)) #x1 * #H2 #H3 cases (pad i x1 ?)
 339   [#b #H4 %{b}
 340    cases (H1 〈i,b〉 ?)
 341     [#z >H4 #H5 %{z} @(monotonic_U … H5) @lt_to_le //
 342     |>H4 @(le_maxr … H2)
 343     ]
 344   |@(le_maxl … H2)
 345   ]
 346 qed.
 347
 348 lemma diag1_not_s1: ∀s1,s2. not_O s2 s1 → ¬ CF s2 (diag_cf s1).
 349 #s1 #s2 #H1 % * #i * #Hcode_i #Hs2_i
 350 cases (not_included_ex  … H1 ? Hs2_i) #b #H2
 351 lapply (diag_spec … Hcode_i) #H3
 352 @(absurd1 (lang i 〈i,b〉))
 353 @(iff_trans … (H3 〈i,b〉))
 354 @(iff_trans … (equiv_diag …)) >fst_pair
 355 %[* #_ // |#H6 % // ]
 356 qed.
 357
 358 (******************************************************************************)
 359 (* definition sumF ≝ λf,g:nat→nat.λn.f n + g n. *)
 360
 361 definition to_Some ≝ λf.λx:nat. Some nat (f x).
 362
 363 definition deopt ≝ λn. match n with
 364   [ None ⇒ 1
 365   | Some n ⇒ n].
 366
 367 definition opt_comp ≝ λf,g:nat → option nat. λx.
 368   match g x with
 369   [ None ⇒ None ?
 370   | Some y ⇒ f y ].
 371
 372 (* axiom CFU: ∀h,g,s. CF s (to_Some h)  → CF s (to_Some (of_size ∘ g)) →
 373   CF (Slow s) (λx.U (h x) (g x)). *)
 374
 375 axiom sU2: nat → nat → nat.
 376 axiom sU: nat → nat → nat → nat.
 377
 378 (* axiom CFU: CF sU (λx.U (fst x) (snd x)). *)
 379
 380 axiom CFU: ∀h,g,f,s1,s2,s3.
 381   CF s1 (to_Some h)  → CF s2 (to_Some g) → CF s3 (to_Some f) →
 382   CF (λx. s1 x + s2 x + s3 x + sU (size_f h x) (size_f g x) (size_f f x))
 383     (λx.U 〈h x,g x〉 (|f x|)).
 384
 385 axiom monotonic_sU: ∀a1,a2,b1,b2,c1,c2. a1 ≤ a2 → b1 ≤ b2 → c1 ≤c2 →
 386   sU a1 b1 c1 ≤ sU a2 b2 c2.
 387
 388 definition sU_space ≝ λi,x,r.i+x+r.
 389 definition sU_time ≝ λi,x,r.i+x+(i^2)*r*(log 2 r).
 390
 391 (*
 392 axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g →
 393   CF (λx.s2 x + s1 (size (deopt (g x)))) (opt_comp f g).
 394
 395 (* axiom CF_comp: ∀f,g,s1, s2. CF s1 f → CF s2 g →
 396   CF (s1 ∘ (λx. size (deopt (g x)))) (opt_comp f g). *)
 397
 398 axiom CF_comp_strong: ∀f,g,s1,s2. CF s1 f → CF s2 g →
 399   CF (s1 ∘ s2) (opt_comp f g). *)
 400
 401 definition IF ≝ λb,f,g:nat →option nat. λx.
 402   match b x with
 403   [None ⇒ None ?
 404   |Some n ⇒ if (eqb n 0) then f x else g x].
 405
 406 axiom IF_CF: ∀b,f,g,sb,sf,sg. CF sb b → CF sf f → CF sg g →
 407   CF (λn. sb n + sf n + sg n) (IF b f g).
 408
 409 lemma diag_cf_def : ∀s.∀i.
 410   diag_cf s i =
 411     IF (λi.U (pair (fst i) i) (|of_size (s (|i|))|)) (λi.Some ? 1) (λi.Some ? 0) i.
 412 #s #i normalize >size_of_size // qed.
 413
 414 (* and now ... *)
 415 axiom CF_pair: ∀f,g,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (g x)) →
 416   CF s (λx.Some ? (pair (f x) (g x))).
 417
 418 axiom CF_fst: ∀f,s. CF s (λx.Some ? (f x)) → CF s (λx.Some ? (fst (f x))).
 419
 420 definition minimal ≝ λs. CF s (λn. Some ? n) ∧ ∀c. CF s (λn. Some ? c).
 421
 422
 423 (*
 424 axiom le_snd: ∀n. |snd n| ≤ |n|.
 425 axiom daemon: ∀P:Prop.P. *)
 426
 427 definition constructible ≝ λs. CF s (λx.Some ? (of_size (s (|x|)))).
 428
 429 (*
 430 lemma compl1: ∀s.
 431   CF s (to_Some fst)  → CF s (to_Some (λx.x)) → CF s (to_Some (λx.(s (|x|)))) →
 432   CF (λx. s x + s x + s x + sU (size_f fst x) (size_f (λx.x) x) (size_f (λx.(s (|x|))) x))
 433     (λx.U 〈fst x,x〉 (|s (|x|)|)).
 434 #s #H1 #H2 #H3 @CFU //
 435 qed.
 436
 437 lemma compl1: ∀s.
 438   CF s (to_Some fst)  → CF s (to_Some (λx.x)) → CF s (to_Some (λx.(s (|x|)))) →
 439   CF (λx. s x + s x + s x + sU (size_f fst x) (size_f (λx.x) x) (|(s x)| ))
 440     (λx.U 〈fst x,x〉 (|s (|x|)|)).
 441 #s #H1 #H2 #H3 @monotonic_CF [3: @(CFU ??? s s s) @CFU //
 442 qed.  *)
 443
 444 lemma diag_s: ∀s. minimal s → constructible s →
 445   CF (λx.s x + sU x x (s x)) (diag_cf s).
 446 #s * #Hs_id #Hs_c #Hs_constr
 447 @ext_CF [2: #n @sym_eq @diag_cf_def | skip]
 448 @(monotonic_CF ???? (IF_CF (λi:ℕ.U (pair (fst i) i) (|of_size (s (|i|))|))
 449    … (λ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) … ))
 450   [2: @CFU [@CF_fst // | // |@Hs_constr]
 451   |@(O_ext2 (λn:ℕ.s n+sU (size_f fst n) n (s n) + (s n+s n+s n+s n)))
 452     [2: #i >size_f_size >size_of_size >size_f_id //]
 453    @O_absorbr
 454     [%{1} %{0} #n #_ >commutative_times <times_n_1 @le_plus //
 455      @monotonic_sU //
 456     |@O_plus_l @(O_plus … (O_refl s)) @(O_plus … (O_refl s))
 457      @(O_plus … (O_refl s)) //
 458   ]
 459 qed.
 460
 461
 462 (*************************** The hierachy theorem *****************************)
 463
 464 (*
 465 theorem hierarchy_theorem_right: ∀s1,s2:nat→nat.
 466   O s1 idN → constructible s1 →
 467     not_O s2 s1 → ¬ CF s1 ⊆ CF s2.
 468 #s1 #s2 #Hs1 #monos1 #H % #H1
 469 @(absurd … (CF s2 (diag_cf s1)))
 470   [@H1 @diag_s // |@(diag1_not_s1 … H)]
 471 qed.
 472 *)
 473
 474 theorem hierarchy_theorem_left: ∀s1,s2:nat→nat.
 475    O(s1) ⊆ O(s2) → CF s1 ⊆ CF s2.
 476 #s1 #s2 #HO #f * #i * #Hcode * #c * #a #Hs1_i %{i} % //
 477 cases (sub_O_to_O … HO) -HO #c1 * #b #Hs1s2
 478 %{(c*c1)} %{(max a b)} #x #lemax
 479 cases (Hs1_i x ?) [2: @(le_maxl …lemax)]
 480 #y #Hy %{y} @(monotonic_U … Hy) >associative_times
 481 @le_times // @Hs1s2 @(le_maxr … lemax)
 482 qed.
 483