--- /dev/null
+
+include "arithmetics/nat.ma".
+include "basics/types.ma".
+include "arithmetics/min_max.ma".
+include "arithmetics/bigO.ma".
+
+(*********************************** pairing **********************************)
+
+axiom pair: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+axiom fst : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+axiom snd : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+axiom fst_pair: ∀a,b. \ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/pair.dec"\ 6pair\ 5/a\ 6 a b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a.
+axiom snd_pair: ∀a,b. \ 5a href="cic:/matita/Reverse_complexity/reverse/snd.dec"\ 6snd\ 5/a\ 6 (\ 5a href="cic:/matita/Reverse_complexity/reverse/pair.dec"\ 6pair\ 5/a\ 6 a b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"\ 6option\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+
+let rec U c n on n ≝
+ match n with
+ [ O ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
+ | S m ⇒ match \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 c with
+ [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? c (* halting case *)
+ | Some c1 ⇒ U c1 m
+ ]
+ ].
+
+lemma halt_U: ∀i,n,y. \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i.
+#i #n #y #H cases n
+ [normalize #H1 destruct |#m normalize >H normalize #H1 destruct //]
+qed.
+
+lemma Some_to_halt: ∀n,i,y. \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? .
+#n elim n
+ [#i #y normalize #H destruct (H)
+ |#m #Hind #i #y normalize
+ cut (\ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6c. \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? c)
+ [cases (\ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i) [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | #c %2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ ]]
+ *[#H >H normalize #H1 destruct (H1) // |* #c #H >H normalize @Hind ]
+ ]
+qed.
+
+lemma monotonici_U: ∀y,n,m,i.
+ \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y.
+#y #n #m elim m
+ [#i normalize #H destruct
+ |#p #Hind #i <\ 5a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"\ 6plus_n_Sm\ 5/a\ 6 normalize
+ cut (\ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ? \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6c. \ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? c)
+ [cases (\ 5a href="cic:/matita/Reverse_complexity/reverse/u.dec"\ 6u\ 5/a\ 6 i) [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | #c %2 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ ]]
+ *[#H1 >H1 normalize // |* #c #H >H normalize #H1 @Hind //]
+ ]
+qed.
+
+lemma monotonic_U: ∀i,n,m,y.n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6m →
+ \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y.
+#i #n #m #y #lenm #H >(\ 5a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"\ 6plus_minus_m_m\ 5/a\ 6 m n) // @\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonici_U.def(5)"\ 6monotonici_U\ 5/a\ 6 //
+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.
+ \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? yn → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 i m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? ym → yn \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 ym.
+#i #n #m #yn #ym #Hn #Hm cases (\ 5a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"\ 6decidable_le\ 5/a\ 6 n m)
+ [#lenm lapply (\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … lenm Hn) >Hm #HS destruct (HS) //
+ |#ltmn lapply (\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … n … Hm) [@\ 5a href="cic:/matita/arithmetics/nat/lt_to_le.def(6)"\ 6lt_to_le\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 //]
+ >Hn #HS destruct (HS) //
+ ]
+qed.
+
+definition code_for ≝ λf,i.∀x.
+ \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6n.∀m. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 〈i,x\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.
+
+definition terminate ≝ λc,r. \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6y. \ 5a href="cic:/matita/Reverse_complexity/reverse/U.fix(0,1,1)"\ 6U\ 5/a\ 6 c r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y.
+
+interpretation "termination" 'fintersects c r = (terminate c r).
+
+definition lang ≝ λi,x.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6r,y\ 5a title="exists" 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 〈i,x\ 5a title="abstract pair" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6 r \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 y.
+
+lemma lang_cf :∀f,i,x. \ 5a href="cic:/matita/Reverse_complexity/reverse/code_for.def(2)"\ 6code_for\ 5/a\ 6 f i →
+ \ 5a href="cic:/matita/Reverse_complexity/reverse/lang.def(2)"\ 6lang\ 5/a\ 6 i x \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6y.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? y \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 y.
+#f #i #x normalize #H %
+ [* #n * #y * #H1 #posy %{y} % //
+ cases (H x) -H #m #H <(H (\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 n m)) [2:@(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … n) //]
+ @(\ 5a href="cic:/matita/Reverse_complexity/reverse/monotonic_U.def(8)"\ 6monotonic_U\ 5/a\ 6 … H1) @(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … m) //
+ |cases (H x) -H #m #Hm * #y #Hy %{m} %{y} >Hm //
+ ]
+qed.
+
+(******************************* complexity classes ***************************)
+
+axiom size: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+axiom of_size: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+
+interpretation "size" 'card n = (size n).
+
+axiom size_of_size: ∀n. |\ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n.
+axiom of_size_max: ∀i,n. |i\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n → i \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/Reverse_complexity/reverse/of_size.dec"\ 6of_size\ 5/a\ 6 n.
+
+axiom size_fst : ∀n. |\ 5a href="cic:/matita/Reverse_complexity/reverse/fst.dec"\ 6fst\ 5/a\ 6 n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 |n\ 5a title="size" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
+
+axiom a : Max0.
+
+definition size_f ≝ λf,n.Max_{i\ 5font class="Apple-style-span" color="#FF0000"\ 6 < \ 5/font\ 6S (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
include "basics/relations.ma".
-inductive nat : Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="nat"\ 6inductive nat : Type[0] ≝
| O : nat
| S : nat → nat.
alias num (instance 0) = "natural number".
-definition pred ≝
+\ 5img class="anchor" src="icons/tick.png" id="pred"\ 6definition pred ≝
λn. match n with [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 | S p ⇒ p].
-theorem pred_Sn : ∀n.n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n).
+\ 5img class="anchor" src="icons/tick.png" id="pred_Sn"\ 6theorem pred_Sn : ∀n.n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n).
// qed.
-theorem injective_S : \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="injective_S"\ 6theorem injective_S : \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6.
// qed.
(*
theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
//. qed. *)
-theorem not_eq_S: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m.
+\ 5img class="anchor" src="icons/tick.png" id="not_eq_S"\ 6theorem not_eq_S: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m.
/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-definition not_zero: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝
+\ 5img class="anchor" src="icons/tick.png" id="not_zero"\ 6definition not_zero: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝
λn: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. match n with [ O ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 | (S p) ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 ].
-theorem not_eq_O_S : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n.
+\ 5img class="anchor" src="icons/tick.png" id="not_eq_O_S"\ 6theorem not_eq_O_S : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n.
#n @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #eqOS (change with (\ 5a href="cic:/matita/arithmetics/nat/not_zero.def(1)"\ 6not_zero\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6)) >eqOS // qed.
-theorem not_eq_n_Sn: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n.
+\ 5img class="anchor" src="icons/tick.png" id="not_eq_n_Sn"\ 6theorem not_eq_n_Sn: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n.
#n (elim n) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"\ 6not_eq_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-theorem nat_case:
+\ 5img class="anchor" src="icons/tick.png" id="nat_case"\ 6theorem nat_case:
∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.∀P:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop.
(n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 → P \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6) → (∀m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m → P (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) → P n.
#n #P (elim n) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ qed.
-theorem nat_elim2 :
+\ 5img class="anchor" src="icons/tick.png" id="nat_elim2"\ 6theorem nat_elim2 :
∀R:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop.
(∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. R \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 n)
→ (∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. R (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n) \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6)
→ ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. R n m.
#R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ qed.
-theorem decidable_eq_nat : ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6m).
+\ 5img class="anchor" src="icons/tick.png" id="decidable_eq_nat"\ 6theorem decidable_eq_nat : ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (n\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6m).
@\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"\ 6nat_elim2\ 5/a\ 6 #n [ (cases n) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"\ 6sym_not_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | #m #Hind (cases Hind) /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/nat/not_eq_S.def(4)"\ 6not_eq_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
qed.
(*************************** plus ******************************)
-let rec plus n m ≝
+\ 5img class="anchor" src="icons/tick.png" id="plus"\ 6let rec plus n m ≝
match n with [ O ⇒ m | S p ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (plus p m) ].
interpretation "natural plus" 'plus x y = (plus x y).
-theorem plus_O_n: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n.
+\ 5img class="anchor" src="icons/tick.png" id="plus_O_n"\ 6theorem plus_O_n: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n.
// qed.
(*
// qed.
*)
-theorem plus_n_O: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="plus_n_O"\ 6theorem plus_n_O: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6.
#n (elim n) normalize // qed.
-theorem plus_n_Sm : ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m.
+\ 5img class="anchor" src="icons/tick.png" id="plus_n_Sm"\ 6theorem plus_n_Sm : ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m.
#n (elim n) normalize // qed.
(*
// qed.
*)
-theorem commutative_plus: \ 5a href="cic:/matita/basics/relations/commutative.def(1)"\ 6commutative\ 5/a\ 6 ? \ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="commutative_plus"\ 6theorem commutative_plus: \ 5a href="cic:/matita/basics/relations/commutative.def(1)"\ 6commutative\ 5/a\ 6 ? \ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6.
#n (elim n) normalize // qed.
-theorem associative_plus : \ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="associative_plus"\ 6theorem associative_plus : \ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6.
#n (elim n) normalize // qed.
-theorem assoc_plus1: ∀a,b,c. c \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (b \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 a) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 c \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 a.
+\ 5img class="anchor" src="icons/tick.png" id="assoc_plus1"\ 6theorem assoc_plus1: ∀a,b,c. c \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (b \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 a) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 c \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 a.
// qed.
-theorem injective_plus_r: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 (λm.n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m).
+\ 5img class="anchor" src="icons/tick.png" id="injective_plus_r"\ 6theorem injective_plus_r: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.\ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 (λm.n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m).
#n (elim n) normalize /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"\ 6injective_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
(* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
(*************************** times *****************************)
-let rec times n m ≝
+\ 5img class="anchor" src="icons/tick.png" id="times"\ 6let rec times n m ≝
match n with [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 | S p ⇒ m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(times p m) ].
interpretation "natural times" 'times x y = (times x y).
-theorem times_Sn_m: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m.
+\ 5img class="anchor" src="icons/tick.png" id="times_Sn_m"\ 6theorem times_Sn_m: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. m\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m.
// qed.
-theorem times_O_n: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n.
+\ 5img class="anchor" src="icons/tick.png" id="times_O_n"\ 6theorem times_O_n: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6n.
// qed.
-theorem times_n_O: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="times_n_O"\ 6theorem times_n_O: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
#n (elim n) // qed.
-theorem times_n_Sm : ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m).
+\ 5img class="anchor" src="icons/tick.png" id="times_n_Sm"\ 6theorem times_n_Sm : ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m).
#n (elim n) normalize // qed.
-theorem commutative_times : \ 5a href="cic:/matita/basics/relations/commutative.def(1)"\ 6commutative\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"\ 6times\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="commutative_times"\ 6theorem commutative_times : \ 5a href="cic:/matita/basics/relations/commutative.def(1)"\ 6commutative\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"\ 6times\ 5/a\ 6.
#n (elim n) normalize // qed.
(* variant sym_times : \forall n,m:nat. n*m = m*n \def
symmetric_times. *)
-theorem distributive_times_plus : \ 5a href="cic:/matita/basics/relations/distributive.def(1)"\ 6distributive\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"\ 6times\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="distributive_times_plus"\ 6theorem distributive_times_plus : \ 5a href="cic:/matita/basics/relations/distributive.def(1)"\ 6distributive\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"\ 6times\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/plus.fix(0,0,1)"\ 6plus\ 5/a\ 6.
#n (elim n) normalize // qed.
-theorem distributive_times_plus_r :
+\ 5img class="anchor" src="icons/tick.png" id="distributive_times_plus_r"\ 6theorem distributive_times_plus_r :
∀a,b,c:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. (b\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6c)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6a.
// qed.
-theorem associative_times: \ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"\ 6times\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="associative_times"\ 6theorem associative_times: \ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"\ 6times\ 5/a\ 6.
#n (elim n) normalize // qed.
-lemma times_times: ∀x,y,z. x\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(y\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(x\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6z).
+\ 5img class="anchor" src="icons/tick.png" id="times_times"\ 6lemma times_times: ∀x,y,z. x\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(y\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(x\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6z).
// qed.
-theorem times_n_1 : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="times_n_1"\ 6theorem times_n_1 : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6.
#n // qed.
(* ci servono questi risultati?
(******************** ordering relations ************************)
-inductive le (n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝
+\ 5img class="anchor" src="icons/tick.png" id="le"\ 6inductive le (n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝
| le_n : le n n
| le_S : ∀ m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. le n m → le n (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m).
interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
-definition lt: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝ λn,m. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
+\ 5img class="anchor" src="icons/tick.png" id="lt"\ 6definition lt: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝ λn,m. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
interpretation "natural 'less than'" 'lt x y = (lt x y).
interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
(* lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m).
// qed. *)
-definition ge: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝ λn,m.m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
+\ 5img class="anchor" src="icons/tick.png" id="ge"\ 6definition ge: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝ λn,m.m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
-definition gt: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝ λn,m.m\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6n.
+\ 5img class="anchor" src="icons/tick.png" id="gt"\ 6definition gt: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → Prop ≝ λn,m.m\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6n.
interpretation "natural 'greater than'" 'gt x y = (gt x y).
interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
-theorem transitive_le : \ 5a href="cic:/matita/basics/relations/transitive.def(2)"\ 6transitive\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"\ 6le\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="transitive_le"\ 6theorem transitive_le : \ 5a href="cic:/matita/basics/relations/transitive.def(2)"\ 6transitive\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"\ 6le\ 5/a\ 6.
#a #b #c #leab #lebc (elim lebc) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
\def transitive_le. *)
-theorem transitive_lt: \ 5a href="cic:/matita/basics/relations/transitive.def(2)"\ 6transitive\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"\ 6lt\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="transitive_lt"\ 6theorem transitive_lt: \ 5a href="cic:/matita/basics/relations/transitive.def(2)"\ 6transitive\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"\ 6lt\ 5/a\ 6.
#a #b #c #ltab #ltbc (elim ltbc) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/qed.
(*
theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
\def transitive_lt. *)
-theorem le_S_S: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m.
+\ 5img class="anchor" src="icons/tick.png" id="le_S_S"\ 6theorem le_S_S: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m.
#n #m #lenm (elim lenm) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-theorem le_O_n : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
+\ 5img class="anchor" src="icons/tick.png" id="le_O_n"\ 6theorem le_O_n : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
#n (elim n) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-theorem le_n_Sn : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n.
+\ 5img class="anchor" src="icons/tick.png" id="le_n_Sn"\ 6theorem le_n_Sn : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n.
/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-theorem le_pred_n : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
+\ 5img class="anchor" src="icons/tick.png" id="le_pred_n"\ 6theorem le_pred_n : ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
#n (elim n) // qed.
-theorem monotonic_pred: \ 5a href="cic:/matita/basics/relations/monotonic.def(1)"\ 6monotonic\ 5/a\ 6 ? \ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"\ 6le\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="monotonic_pred"\ 6theorem monotonic_pred: \ 5a href="cic:/matita/basics/relations/monotonic.def(1)"\ 6monotonic\ 5/a\ 6 ? \ 5a href="cic:/matita/arithmetics/nat/le.ind(1,0,1)"\ 6le\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/pred.def(1)"\ 6pred\ 5/a\ 6.
#n #m #lenm (elim lenm) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-theorem le_S_S_to_le: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m → n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
+\ 5img class="anchor" src="icons/tick.png" id="le_S_S_to_le"\ 6theorem le_S_S_to_le: ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m → n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
(* demo *)
/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"\ 6monotonic_pred\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
/2/ qed. *)
-theorem lt_to_not_zero : ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/nat/not_zero.def(1)"\ 6not_zero\ 5/a\ 6 m.
+\ 5img class="anchor" src="icons/tick.png" id="lt_to_not_zero"\ 6theorem lt_to_not_zero : ∀n,m:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → \ 5a href="cic:/matita/arithmetics/nat/not_zero.def(1)"\ 6not_zero\ 5/a\ 6 m.
#n #m #Hlt (elim Hlt) // qed.
(* lt vs. le *)
+
+\ 5img class="anchor" src="icons/tick.png" id="lt_to_le"\ 6lemma lt_to_le: ∀n,m. n \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 m → n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m.
+#n #m #H @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 @H qed-.
+
theorem not_le_Sn_O: ∀ n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n \ 5a title="natural 'neither less nor equal to'" href="cic:/fakeuri.def(1)"\ 6≰\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
#n @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Hlen0 @(\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_zero.def(2)"\ 6lt_to_not_zero\ 5/a\ 6 ?? Hlen0) qed.
projects / helm.git / commitdiff