-@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)) //
+@\ 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]
+@(\ 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))
+ … (λ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) … ))
+ [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]
+ |@(\ 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)))
+ [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 //]
+ @\ 5a href="cic:/matita/arithmetics/bigO/O_absorbr.def(12)"\ 6O_absorbr\ 5/a\ 6
+ [%{\ 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 //
+ @\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_sU.dec"\ 6monotonic_sU\ 5/a\ 6 //
+ |@\ 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))
+ @(\ 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)) //