matita/matita/lib/reverse_complexity/hierarchy.ma

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