2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/nat.ma".
16 \ 5img class="anchor" src="icons/tick.png" id="max'"
\ 6let rec max' i f d ≝
22 | false ⇒ max' j f d]].
24 \ 5img class="anchor" src="icons/tick.png" id="max"
\ 6definition max ≝ λn.λf.
\ 5a href="cic:/matita/arithmetics/minimization/max'.fix(0,0,1)"
\ 6max'
\ 5/a
\ 6 n f
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6.
26 \ 5img class="anchor" src="icons/tick.png" id="max_O"
\ 6theorem max_O: ∀f.
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 f
\ 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.
29 \ 5img class="anchor" src="icons/tick.png" id="max_cases"
\ 6theorem max_cases: ∀f.∀n.
30 (f n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n) f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n)
\ 5a title="logical or" href="cic:/fakeuri.def(1)"
\ 6∨
\ 5/a
\ 6
31 (f n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n) f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f).
32 #f #n normalize cases (f n) normalize /
\ 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/basics/logic/And.con(0,1,2)"
\ 6conj
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ qed.
34 \ 5img class="anchor" src="icons/tick.png" id="le_max_n"
\ 6theorem le_max_n: ∀f.∀n.
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"
\ 6max
\ 5/a
\ 6 n f
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n.
35 #f #n (elim n) // #m #Hind
36 normalize (cases (f m)) normalize @
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6 //
41 \ 5img class="anchor" src="icons/tick.png" id="lt_max_n"
\ 6theorem lt_max_n : ∀f.∀n.
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n →
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"
\ 6max
\ 5/a
\ 6 n f
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n.
42 #f #n #posn @(
\ 5a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"
\ 6lt_O_n_elim
\ 5/a
\ 6 ? posn) #m
43 normalize (cases (f m)) normalize
\ 5font class="Apple-style-span" color="#FF0000"
\ 6@
\ 5/font
\ 6\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6 //
46 \ 5img class="anchor" src="icons/tick.png" id="le_to_le_max"
\ 6theorem le_to_le_max : ∀f.∀n,m.
47 n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"
\ 6max
\ 5/a
\ 6 m f.
48 #f #n #m #H (elim H) //
49 #i #leni #Hind @(
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6 … Hind)
50 (cases (
\ 5a href="cic:/matita/arithmetics/minimization/max_cases.def(3)"
\ 6max_cases
\ 5/a
\ 6 f i)) * #_ /
\ 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\ 5/span
\ 6\ 5/span
\ 6/
53 \ 5img class="anchor" src="icons/tick.png" id="true_to_le_max"
\ 6theorem true_to_le_max: ∀f.∀n,m.
54 m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → f m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 → m
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f.
56 [#m #ltmO @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
58 (cases (
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 … ltm)))
59 [#ltm #fm @(
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 i f))
60 [@Hind /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/ | @
\ 5a href="cic:/matita/arithmetics/minimization/le_to_le_max.def(4)"
\ 6le_to_le_max
\ 5/a
\ 6 //]
61 |#eqm >eqm #eqf normalize >eqf //
65 \ 5img class="anchor" src="icons/tick.png" id="lt_max_to_false"
\ 6theorem lt_max_to_false: ∀f.∀n,m.
66 m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n →
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m → f m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6.
67 #f #n #m #ltnm #eqf cases(
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (f m)) //
68 #fm @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … eqf) @(
\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"
\ 6le_to_not_lt
\ 5/a
\ 6) @
\ 5a href="cic:/matita/arithmetics/minimization/true_to_le_max.def(6)"
\ 6true_to_le_max
\ 5/a
\ 6 //
71 \ 5img class="anchor" src="icons/tick.png" id="max_exists"
\ 6lemma max_exists: ∀f.∀n,m.m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → f m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 →
72 (∀i. m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 i → i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6) →
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m.
74 [#ltO @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
75 |#Hind #max #ltmax #fmax #ismax
76 cases (
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 …(
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 …(ltmax …)))
78 [>(ismax m …) // normalize @(Hind max ltm fmax)
79 #i #Hl #Hr @ismax // @
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6 //
85 \ 5img class="anchor" src="icons/tick.png" id="max_not_exists"
\ 6lemma max_not_exists: ∀f.∀n.
86 (∀i. i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6) →
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f
\ 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.
87 #f #n #ffalse @(
\ 5a href="cic:/matita/arithmetics/nat/le_gen.def(1)"
\ 6le_gen
\ 5/a
\ 6 ? n) #i (elim i) // #j #Hind #ltj
88 normalize >ffalse // @Hind /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"
\ 6le_plus_b
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
91 \ 5img class="anchor" src="icons/tick.png" id="fmax_false"
\ 6lemma fmax_false: ∀f.∀n,m.
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m → f m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 → m
\ 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.
93 #i #Hind normalize cases(
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 … (f i)) #fi >fi
95 [#eqm #fm @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … fi) // |@Hind]
98 \ 5img class="anchor" src="icons/tick.png" id="max_spec"
\ 6inductive max_spec (n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6) (f:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6→
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6) :
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6→Prop ≝
99 | found : ∀m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → f m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 →
100 (∀i. m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 i → i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6) → max_spec n f m
101 | not_found: (∀i.i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6) → max_spec n f
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6.
103 \ 5img class="anchor" src="icons/tick.png" id="max_spec_to_max"
\ 6theorem max_spec_to_max: ∀f.∀n,m.
104 \ 5a href="cic:/matita/arithmetics/minimization/max_spec.ind(1,0,2)"
\ 6max_spec
\ 5/a
\ 6 n f m →
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m.
105 #f #n #m #spec (cases spec)
106 [#max #ltmax #fmax #ismax @
\ 5a href="cic:/matita/arithmetics/minimization/max_exists.def(6)"
\ 6max_exists
\ 5/a
\ 6 // @ismax
107 |#ffalse @
\ 5a href="cic:/matita/arithmetics/minimization/max_not_exists.def(9)"
\ 6max_not_exists
\ 5/a
\ 6 @ffalse
111 \ 5img class="anchor" src="icons/tick.png" id="max_to_max_spec"
\ 6theorem max_to_max_spec: ∀f.∀n,m.
112 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/minimization/max_spec.ind(1,0,2)"
\ 6max_spec
\ 5/a
\ 6 n f m.
114 [#eqm <eqm %2 #i #ltiO @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
115 |#n #eqm cases(
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (f m)) #fm
116 (* non trova max_to_false *)
117 [%1 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/minimization/lt_max_n.def(5)"
\ 6lt_max_n
\ 5/a
\ 6,
\ 5a href="cic:/matita/arithmetics/minimization/lt_max_to_false.def(9)"
\ 6lt_max_to_false
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
118 |lapply (
\ 5a href="cic:/matita/arithmetics/minimization/fmax_false.def(4)"
\ 6fmax_false
\ 5/a
\ 6 ??? eqm fm) #eqmO >eqmO
119 %2 #i (cases i) // #j #ltj @(
\ 5a href="cic:/matita/arithmetics/minimization/lt_max_to_false.def(9)"
\ 6lt_max_to_false
\ 5/a
\ 6 … ltj) //
122 \ 5img class="anchor" src="icons/tick.png" id="max_f_g"
\ 6theorem max_f_g: ∀f,g,n.(∀i. i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 g i) →
123 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n g.
125 #m #Hind #ext whd in ⊢(??%%); >ext // normalize in Hind; >Hind //
126 # i #ltim @ext /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"
\ 6transitive_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
129 \ 5img class="anchor" src="icons/tick.png" id="le_max_f_max_g"
\ 6theorem le_max_f_max_g: ∀f,g,n. (∀i. i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 → g i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6) →
130 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n g.
132 #m #Hind #ext normalize (cases (
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (f m))) #Heq >Heq
134 |(cases (g m)) normalize [@
\ 5a href="cic:/matita/arithmetics/minimization/le_max_n.def(3)"
\ 6le_max_n
\ 5/a
\ 6] @Hind #i #ltim @ext /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"
\ 6transitive_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
137 \ 5img class="anchor" src="icons/tick.png" id="f_max_true"
\ 6theorem f_max_true : ∀ f.∀n.
138 (∃i:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6\ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6.
\ 5/a
\ 6 i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6) → f (
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6.
139 #f #n cases(
\ 5a href="cic:/matita/arithmetics/minimization/max_to_max_spec.def(10)"
\ 6max_to_max_spec
\ 5/a
\ 6 f n (
\ 5a href="cic:/matita/arithmetics/minimization/max.def(2)"
\ 6max
\ 5/a
\ 6 n f) (
\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"
\ 6refl
\ 5/a
\ 6 …)) //
140 #Hall * #x * #ltx #fx @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … fx) >Hall /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"
\ 6eqnot_to_noteq
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
145 (* min k b f is the minimun i, b ≤ i < b + k s.t. f i;
146 returns b + k otherwise *)
148 \ 5img class="anchor" src="icons/tick.png" id="min"
\ 6let rec min k b f ≝
154 | false ⇒ min p (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 b) f]].
156 \ 5img class="anchor" src="icons/tick.png" id="min0"
\ 6definition min0 ≝ λn.λf.
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n
\ 5a title="natural number" href="cic:/fakeuri.def(1)"
\ 60
\ 5/a
\ 6 f.
158 \ 5img class="anchor" src="icons/tick.png" id="min_O_f"
\ 6theorem min_O_f : ∀f.∀b.
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 b f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 b.
161 \ 5img class="anchor" src="icons/tick.png" id="true_min"
\ 6theorem true_min: ∀f.∀b.
162 f b
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 → ∀n.
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 b.
163 #f #b #fb #n (cases n) // #n normalize >fb normalize //
166 \ 5img class="anchor" src="icons/tick.png" id="false_min"
\ 6theorem false_min: ∀f.∀n,b.
167 f b
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n) b f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 b) f.
168 #f #n #b #fb normalize >fb normalize //
172 theorem leb_to_le_min : ∀f.∀n,b1,b2.
173 b1 ≤ b2 → min n b1 f ≤ min n b2 f.
174 #f #n #b1 #b2 #leb (elim n) //
175 #m #Hind normalize (cases (f m)) normalize *)
177 \ 5img class="anchor" src="icons/tick.png" id="le_min_r"
\ 6theorem le_min_r: ∀f.∀n,b.
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b.
178 #f #n normalize (elim n) // #m #Hind #b
179 normalize (cases (f b)) normalize //
182 \ 5img class="anchor" src="icons/tick.png" id="le_min_l"
\ 6theorem le_min_l: ∀f.∀n,b. b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f.
183 #f #n normalize (elim n) // #m #Hind #b
184 normalize (cases (f b)) normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"
\ 6le_plus_b
\ 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/
187 \ 5img class="anchor" src="icons/tick.png" id="le_to_le_min"
\ 6theorem le_to_le_min : ∀f.∀n,m.
188 n
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → ∀b.
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 m b f.
189 #f @
\ 5a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"
\ 6nat_elim2
\ 5/a
\ 6 //
190 [#n #leSO @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
191 |#n #m #Hind #leSS #b
192 (cases (
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (f b))) #fb
193 [lapply (
\ 5a href="cic:/matita/arithmetics/minimization/true_min.def(4)"
\ 6true_min
\ 5/a
\ 6 …fb) #H >H >H //
194 |>
\ 5a href="cic:/matita/arithmetics/minimization/false_min.def(3)"
\ 6false_min
\ 5/a
\ 6 // >
\ 5a href="cic:/matita/arithmetics/minimization/false_min.def(3)"
\ 6false_min
\ 5/a
\ 6 // @Hind /
\ 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/
199 \ 5img class="anchor" src="icons/tick.png" id="true_to_le_min"
\ 6theorem true_to_le_min: ∀f.∀n,m,b.
200 b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → f m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 →
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m.
202 #i #Hind #m #b #leb (cases (
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … leb))
203 [#ltm #fm normalize (cases (f b)) normalize // @Hind //
204 |#eqm <eqm #eqb normalize >eqb normalize //
208 \ 5img class="anchor" src="icons/tick.png" id="lt_min_to_false"
\ 6theorem lt_min_to_false: ∀f.∀n,m,b.
209 b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f → f m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6.
210 #f #n #m #b #lebm #ltm cases(
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (f m)) //
211 #fm @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … ltm) @(
\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"
\ 6le_to_not_lt
\ 5/a
\ 6) @
\ 5a href="cic:/matita/arithmetics/minimization/true_to_le_min.def(6)"
\ 6true_to_le_min
\ 5/a
\ 6 //
214 \ 5img class="anchor" src="icons/tick.png" id="fmin_true"
\ 6theorem fmin_true: ∀f.∀n,m,b.
215 m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f → m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b → f m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6.
217 [#m #b normalize #eqmb >eqmb #leSb @(
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6)
218 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … leSb) //
219 |#n #Hind #m #b (cases (
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (f b))) #caseb
220 [>
\ 5a href="cic:/matita/arithmetics/minimization/true_min.def(4)"
\ 6true_min
\ 5/a
\ 6 //
221 |>
\ 5a href="cic:/matita/arithmetics/minimization/false_min.def(3)"
\ 6false_min
\ 5/a
\ 6 // #eqm #ltm @(Hind m (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 b)) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
226 \ 5img class="anchor" src="icons/tick.png" id="min_exists"
\ 6lemma min_exists: ∀f.∀t,m. m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 t → f m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 →
227 ∀k,b.b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → (∀i. b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i → i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6) → t
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 k
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b →
228 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 k b f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m.
229 #f #t #m #ltmt #fm #k (elim k)
230 [#b #lebm #ismin #eqtb @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … lebm) <eqtb
231 @
\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"
\ 6lt_to_not_le
\ 5/a
\ 6 //
232 |#d #Hind #b #lebm #ismin #eqt cases(
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 …lebm)
233 [#ltbm >
\ 5a href="cic:/matita/arithmetics/minimization/false_min.def(3)"
\ 6false_min
\ 5/a
\ 6 /
\ 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\ 5/span
\ 6\ 5/span
\ 6/ @Hind //
234 [#i #H #H1 @ismin /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"
\ 6le_plus_b
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ | >eqt normalize //]
235 |#eqbm >
\ 5a href="cic:/matita/arithmetics/minimization/true_min.def(4)"
\ 6true_min
\ 5/a
\ 6 //
240 \ 5img class="anchor" src="icons/tick.png" id="min_not_exists"
\ 6lemma min_not_exists: ∀f.∀n,b.
241 (∀i. b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i → i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6) →
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f
\ 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 b.
243 #p #Hind #b #ffalse >
\ 5a href="cic:/matita/arithmetics/minimization/false_min.def(3)"
\ 6false_min
\ 5/a
\ 6
244 [>Hind // #i #H #H1 @ffalse /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"
\ 6le_plus_b
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
249 \ 5img class="anchor" src="icons/tick.png" id="fmin_false"
\ 6lemma fmin_false: ∀f.∀n,b.let m ≝
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f in
250 f m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 → m
\ 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
\ 6b.
252 #i #Hind #b normalize cases(
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 … (f b)) #fb >fb
254 [#eqm @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … fb) //
255 |>
\ 5a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"
\ 6plus_n_Sm
\ 5/a
\ 6 @Hind]
258 \ 5img class="anchor" src="icons/tick.png" id="min_spec"
\ 6inductive min_spec (n,b:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6) (f:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6→
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6) :
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6→Prop ≝
259 | found : ∀m:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6. b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m → m
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b → f m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 →
260 (∀i. b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i → i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 m → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6) → min_spec n b f m
261 | not_found: (∀i.b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i → i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 (n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b) → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6) →
262 min_spec n b f (n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6b).
264 \ 5img class="anchor" src="icons/tick.png" id="min_spec_to_min"
\ 6theorem min_spec_to_min: ∀f.∀n,b,m.
265 \ 5a href="cic:/matita/arithmetics/minimization/min_spec.ind(1,0,3)"
\ 6min_spec
\ 5/a
\ 6 n b f m →
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m.
266 #f #n #b #m #spec (cases spec)
267 [#m #lem #ltm #fm #ismin @(
\ 5a href="cic:/matita/arithmetics/minimization/min_exists.def(9)"
\ 6min_exists
\ 5/a
\ 6 f (n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6b)) // @ismin
268 |#ffalse @
\ 5a href="cic:/matita/arithmetics/minimization/min_not_exists.def(9)"
\ 6min_not_exists
\ 5/a
\ 6 @ffalse
272 \ 5img class="anchor" src="icons/tick.png" id="min_to_min_spec"
\ 6theorem min_to_min_spec: ∀f.∀n,b,m.
273 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 m →
\ 5a href="cic:/matita/arithmetics/minimization/min_spec.ind(1,0,3)"
\ 6min_spec
\ 5/a
\ 6 n b f m.
274 #f #n #b #m (cases n)
275 [#eqm <eqm %2 #i #lei #lti @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … lti) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"
\ 6le_to_not_lt
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
276 |#n #eqm (* (cases (le_to_or_lt_eq … (le_min_r …))) Stack overflow! *)
277 lapply (
\ 5a href="cic:/matita/arithmetics/minimization/le_min_r.def(9)"
\ 6le_min_r
\ 5/a
\ 6 f (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n) b) >eqm #lem
278 (cases (
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … lem)) #mcase
279 [%1 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/minimization/fmin_true.def(7)"
\ 6fmin_true
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ #i #H #H1 @(
\ 5a href="cic:/matita/arithmetics/minimization/lt_min_to_false.def(9)"
\ 6lt_min_to_false
\ 5/a
\ 6 f (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n) i b) //
280 |>mcase %2 #i #lebi #lti @(
\ 5a href="cic:/matita/arithmetics/minimization/lt_min_to_false.def(9)"
\ 6lt_min_to_false
\ 5/a
\ 6 f (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n) i b) //
285 \ 5img class="anchor" src="icons/tick.png" id="min_f_g"
\ 6theorem min_f_g: ∀f,g,n,b.(∀i. b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i → i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 g i) →
286 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b g.
288 #m #Hind #b #ext normalize >(ext b (
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"
\ 6le_n
\ 5/a
\ 6 b) ?) // >Hind //
289 #i #ltib #ltim @ext /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"
\ 6le_plus_b
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
292 \ 5img class="anchor" src="icons/tick.png" id="le_min_f_min_g"
\ 6theorem le_min_f_min_g: ∀f,g,n,b.
293 (∀i. b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i → i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6b → f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 → g i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6) →
294 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b g
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f.
296 #m #Hind #b #ext normalize (cases (
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (f b))) #Heq >Heq
298 |(cases (g b)) normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"
\ 6le_plus_b
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ @Hind #i #ltb #ltim #fi
299 @ext /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"
\ 6le_plus_b
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
302 \ 5img class="anchor" src="icons/tick.png" id="f_min_true"
\ 6theorem f_min_true : ∀ f.∀n,b.
303 (∃i:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6\ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6.
\ 5/a
\ 6 b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6) → f (
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6.
304 #f #n #b cases(
\ 5a href="cic:/matita/arithmetics/minimization/min_to_min_spec.def(10)"
\ 6min_to_min_spec
\ 5/a
\ 6 f n b (
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f) (
\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"
\ 6refl
\ 5/a
\ 6 …)) //
305 #Hall * #x * * #leb #ltx #fx @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … fx) >Hall /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"
\ 6eqnot_to_noteq
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
308 \ 5img class="anchor" src="icons/tick.png" id="lt_min"
\ 6theorem lt_min : ∀ f.∀n,b.
309 (∃i:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6\ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6.
\ 5/a
\ 6 b
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 i
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 f i
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6) →
\ 5a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"
\ 6min
\ 5/a
\ 6 n b f
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 b.
310 #f #n #b #H cases H #i * * #lebi #ltin #fi_true
311 @(
\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"
\ 6le_to_lt_to_lt
\ 5/a
\ 6 … ltin) @
\ 5a href="cic:/matita/arithmetics/minimization/true_to_le_min.def(6)"
\ 6true_to_le_min
\ 5/a
\ 6 //