X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Farithmetics%2Fminimization.ma;h=afa47f76b700025399bce6426a55a890e8f9beeb;hb=268e7f336d036f77ffc9663358e9afda92b97730;hp=eda9d016618d1031be5b126b65b35ca105b9ee11;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git diff --git a/weblib/arithmetics/minimization.ma b/weblib/arithmetics/minimization.ma index eda9d0166..afa47f76b 100644 --- a/weblib/arithmetics/minimization.ma +++ b/weblib/arithmetics/minimization.ma @@ -13,7 +13,7 @@ include "arithmetics/nat.ma". (* maximization *) -let rec max' i f d ≝ +img class="anchor" src="icons/tick.png" id="max'"let rec max' i f d ≝ match i with [ O ⇒ d | S j ⇒ @@ -21,123 +21,123 @@ let rec max' i f d ≝ [ true ⇒ j | false ⇒ max' j f d]]. -definition max ≝ λn.λf.max' n f O. +img class="anchor" src="icons/tick.png" id="max"definition max ≝ λn.λf.a href="cic:/matita/arithmetics/minimization/max'.fix(0,0,1)"max'/a n f a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. -theorem max_O: ∀f. max O f = O. +img class="anchor" src="icons/tick.png" id="max_O"theorem max_O: ∀f. a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. // qed. -theorem max_cases: ∀f.∀n. - (f n = true ∧ max (S n) f = n) ∨ - (f n = false ∧ max (S n) f = max n f). -#f #n normalize cases (f n) normalize /3/ qed. +img class="anchor" src="icons/tick.png" id="max_cases"theorem max_cases: ∀f.∀n. + (f n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n) a title="logical or" href="cic:/fakeuri.def(1)"∨/a + (f n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f). +#f #n normalize cases (f n) normalize /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed. -theorem le_max_n: ∀f.∀n. max n f ≤ n. +img class="anchor" src="icons/tick.png" id="le_max_n"theorem le_max_n: ∀f.∀n. a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"max/a n f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n. #f #n (elim n) // #m #Hind -normalize (cases (f m)) normalize @le_S // +normalize (cases (f m)) normalize @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a // (* non trova Hind *) @Hind qed. -theorem lt_max_n : ∀f.∀n. O < n → max n f < n. -#f #n #posn @(lt_O_n_elim ? posn) #m -normalize (cases (f m)) normalize apply le_S_S // +img class="anchor" src="icons/tick.png" id="lt_max_n"theorem lt_max_n : ∀f.∀n. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"max/a n f a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n. +#f #n #posn @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"lt_O_n_elim/a ? posn) #m +normalize (cases (f m)) normalize font class="Apple-style-span" color="#FF0000"@/fonta href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a // @le_max_n qed. -theorem le_to_le_max : ∀f.∀n,m. -n ≤ m → max n f ≤ max m f. +img class="anchor" src="icons/tick.png" id="le_to_le_max"theorem le_to_le_max : ∀f.∀n,m. +n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/max.def(2)" title="null"max/a m f. #f #n #m #H (elim H) // -#i #leni #Hind @(transitive_le … Hind) -(cases (max_cases f i)) * #_ /2/ +#i #leni #Hind @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … Hind) +(cases (a href="cic:/matita/arithmetics/minimization/max_cases.def(3)"max_cases/a f i)) * #_ /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed. -theorem true_to_le_max: ∀f.∀n,m. - m < n → f m = true → m ≤ max n f. +img class="anchor" src="icons/tick.png" id="true_to_le_max"theorem true_to_le_max: ∀f.∀n,m. + m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f. #f #n (elim n) - [#m #ltmO @False_ind /2/ + [#m #ltmO @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ |#i #Hind #m #ltm - (cases (le_to_or_lt_eq … (le_S_S_to_le … ltm))) - [#ltm #fm @(transitive_le ? (max i f)) - [@Hind /2/ | @le_to_le_max //] + (cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … (a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a … ltm))) + [#ltm #fm @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a i f)) + [@Hind /span class="autotactic"2span class="autotrace" trace /span/span/ | @a href="cic:/matita/arithmetics/minimization/le_to_le_max.def(4)"le_to_le_max/a //] |#eqm >eqm #eqf normalize >eqf // ] qed. -theorem lt_max_to_false: ∀f.∀n,m. - m < n → max n f < m → f m = false. -#f #n #m #ltnm #eqf cases(true_or_false (f m)) // -#fm @False_ind @(absurd … eqf) @(le_to_not_lt) @true_to_le_max // +img class="anchor" src="icons/tick.png" id="lt_max_to_false"theorem lt_max_to_false: ∀f.∀n,m. + m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. +#f #n #m #ltnm #eqf cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f m)) // +#fm @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … eqf) @(a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a) @a href="cic:/matita/arithmetics/minimization/true_to_le_max.def(6)"true_to_le_max/a // qed. -lemma max_exists: ∀f.∀n,m.m < n → f m =true → - (∀i. m < i → i < n → f i = false) → max n f = m. +img class="anchor" src="icons/tick.png" id="max_exists"lemma max_exists: ∀f.∀n,m.m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → + (∀i. m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m. #f #n (elim n) #m - [#ltO @False_ind /2/ + [#ltO @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ |#Hind #max #ltmax #fmax #ismax - cases (le_to_or_lt_eq …(le_S_S_to_le …(ltmax …))) + cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a …(a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a …(ltmax …))) #ltm normalize [>(ismax m …) // normalize @(Hind max ltm fmax) - #i #Hl #Hr @ismax // @le_S // + #i #Hl #Hr @ismax // @a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a // |fmax // ] ] qed. -lemma max_not_exists: ∀f.∀n. - (∀i. i < n → f i = false) → max n f = O. -#f #n #ffalse @(le_gen ? n) #i (elim i) // #j #Hind #ltj -normalize >ffalse // @Hind /2/ +img class="anchor" src="icons/tick.png" id="max_not_exists"lemma max_not_exists: ∀f.∀n. + (∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. +#f #n #ffalse @(a href="cic:/matita/arithmetics/nat/le_gen.def(1)"le_gen/a ? n) #i (elim i) // #j #Hind #ltj +normalize >ffalse // @Hind /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ qed. -lemma fmax_false: ∀f.∀n,m.max n f = m → f m = false → m = O. +img class="anchor" src="icons/tick.png" id="fmax_false"lemma fmax_false: ∀f.∀n,m.a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. #f #n #m (elim n) // -#i #Hind normalize cases(true_or_false … (f i)) #fi >fi +#i #Hind normalize cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (f i)) #fi >fi normalize - [#eqm #fm @False_ind @(absurd … fi) // |@Hind] + [#eqm #fm @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … fi) // |@Hind] qed. -inductive max_spec (n:nat) (f:nat→bool) : nat→Prop ≝ - | found : ∀m:nat.m < n → f m =true → - (∀i. m < i → i < n → f i = false) → max_spec n f m - | not_found: (∀i.i < n → f i = false) → max_spec n f O. +img class="anchor" src="icons/tick.png" id="max_spec"inductive max_spec (n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→Prop ≝ + | found : ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → + (∀i. m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → max_spec n f m + | not_found: (∀i.i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → max_spec n f a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a. -theorem max_spec_to_max: ∀f.∀n,m. - max_spec n f m → max n f = m. +img class="anchor" src="icons/tick.png" id="max_spec_to_max"theorem max_spec_to_max: ∀f.∀n,m. + a href="cic:/matita/arithmetics/minimization/max_spec.ind(1,0,2)"max_spec/a n f m → a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m. #f #n #m #spec (cases spec) - [#max #ltmax #fmax #ismax @max_exists // @ismax - |#ffalse @max_not_exists @ffalse + [#max #ltmax #fmax #ismax @a href="cic:/matita/arithmetics/minimization/max_exists.def(6)"max_exists/a // @ismax + |#ffalse @a href="cic:/matita/arithmetics/minimization/max_not_exists.def(9)"max_not_exists/a @ffalse ] qed. -theorem max_to_max_spec: ∀f.∀n,m. - max n f = m → max_spec n f m. +img class="anchor" src="icons/tick.png" id="max_to_max_spec"theorem max_to_max_spec: ∀f.∀n,m. + a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m → a href="cic:/matita/arithmetics/minimization/max_spec.ind(1,0,2)"max_spec/a n f m. #f #n #m (cases n) - [#eqm eqmO - %2 #i (cases i) // #j #ltj @(lt_max_to_false … ltj) // + [%1 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/minimization/lt_max_n.def(5)"lt_max_n/a, a href="cic:/matita/arithmetics/minimization/lt_max_to_false.def(9)"lt_max_to_false/a/span/span/ + |lapply (a href="cic:/matita/arithmetics/minimization/fmax_false.def(4)"fmax_false/a ??? eqm fm) #eqmO >eqmO + %2 #i (cases i) // #j #ltj @(a href="cic:/matita/arithmetics/minimization/lt_max_to_false.def(9)"lt_max_to_false/a … ltj) // qed. -theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) → - max n f = max n g. +img class="anchor" src="icons/tick.png" id="max_f_g"theorem max_f_g: ∀f,g,n.(∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g i) → + a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n g. #f #g #n (elim n) // -#m #Hind #ext normalize >ext >Hind // -#i #ltim @ext /2/ +#m #Hind #ext whd in ⊢(??%%); >ext // normalize in Hind; >Hind // +# i #ltim @ext /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a/span/span/ qed. -theorem le_max_f_max_g: ∀f,g,n. (∀i. i < n → f i = true → g i =true) → -max n f ≤ max n g. +img class="anchor" src="icons/tick.png" id="le_max_f_max_g"theorem le_max_f_max_g: ∀f,g,n. (∀i. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → g i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → +a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n g. #f #g #n (elim n) // -#m #Hind #ext normalize (cases (true_or_false (f m))) #Heq >Heq +#m #Hind #ext normalize (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f m))) #Heq >Heq [>ext // - |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext /2/ + |(cases (g m)) normalize [@a href="cic:/matita/arithmetics/minimization/le_max_n.def(3)"le_max_n/a] @Hind #i #ltim @ext /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/transitive_lt.def(3)"transitive_lt/a/span/span/ qed. -theorem f_max_true : ∀ f.∀n. -(∃i:nat. i < n ∧ f i = true) → f (max n f) = true. -#f #n cases(max_to_max_spec f n (max n f) (refl …)) // -#Hall * #x * #ltx #fx @False_ind @(absurd … fx) >Hall /2/ +img class="anchor" src="icons/tick.png" id="f_max_true"theorem f_max_true : ∀ f.∀n. +(∃i:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/aa title="exists" href="cic:/fakeuri.def(1)"./a i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="logical and" href="cic:/fakeuri.def(1)"∧/a f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → f (a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. +#f #n cases(a href="cic:/matita/arithmetics/minimization/max_to_max_spec.def(10)"max_to_max_spec/a f n (a href="cic:/matita/arithmetics/minimization/max.def(2)"max/a n f) (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a …)) // +#Hall * #x * #ltx #fx @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … fx) >Hall /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a/span/span/ qed. (* minimization *) @@ -145,26 +145,26 @@ qed. (* min k b f is the minimun i, b ≤ i < b + k s.t. f i; returns b + k otherwise *) -let rec min k b f ≝ +img class="anchor" src="icons/tick.png" id="min"let rec min k b f ≝ match k with [ O ⇒ b | S p ⇒ match f b with [ true ⇒ b - | false ⇒ min p (S b) f]]. + | false ⇒ min p (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b) f]]. -definition min0 ≝ λn.λf. min n 0 f. +img class="anchor" src="icons/tick.png" id="min0"definition min0 ≝ λn.λf. a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n a title="natural number" href="cic:/fakeuri.def(1)"0/a f. -theorem min_O_f : ∀f.∀b. min O b f = b. +img class="anchor" src="icons/tick.png" id="min_O_f"theorem min_O_f : ∀f.∀b. a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b. // qed. -theorem true_min: ∀f.∀b. - f b = true → ∀n.min n b f = b. +img class="anchor" src="icons/tick.png" id="true_min"theorem true_min: ∀f.∀b. + f b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → ∀n.a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b. #f #b #fb #n (cases n) // #n normalize >fb normalize // qed. -theorem false_min: ∀f.∀n,b. - f b = false → min (S n) b f = min n (S b) f. +img class="anchor" src="icons/tick.png" id="false_min"theorem false_min: ∀f.∀n,b. + f b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b) f. #f #n #b #fb normalize >fb normalize // qed. @@ -174,131 +174,139 @@ b1 ≤ b2 → min n b1 f ≤ min n b2 f. #f #n #b1 #b2 #leb (elim n) // #m #Hind normalize (cases (f m)) normalize *) -theorem le_min_r: ∀f.∀n,b. min n b f ≤ n + b. +img class="anchor" src="icons/tick.png" id="le_min_r"theorem le_min_r: ∀f.∀n,b. a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b. #f #n normalize (elim n) // #m #Hind #b normalize (cases (f b)) normalize // qed. -theorem le_min_l: ∀f.∀n,b. b ≤ min n b f. +img class="anchor" src="icons/tick.png" id="le_min_l"theorem le_min_l: ∀f.∀n,b. b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f. #f #n normalize (elim n) // #m #Hind #b -normalize (cases (f b)) normalize /2/ +normalize (cases (f b)) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a, a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ qed. -theorem le_to_le_min : ∀f.∀n,m. -n ≤ m → ∀b.min n b f ≤ min m b f. -#f @nat_elim2 // - [#n #leSO @False_ind /2/ +img class="anchor" src="icons/tick.png" id="le_to_le_min"theorem le_to_le_min : ∀f.∀n,m. +n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → ∀b.a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a m b f. +#f @a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a // + [#n #leSO @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ |#n #m #Hind #leSS #b - (cases (true_or_false (f b))) #fb - [lapply (true_min …fb) #H >H >H // - |>false_min // >false_min // @Hind /2/ + (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f b))) #fb + [lapply (a href="cic:/matita/arithmetics/minimization/true_min.def(4)"true_min/a …fb) #H >H >H // + |>a href="cic:/matita/arithmetics/minimization/false_min.def(3)"false_min/a // >a href="cic:/matita/arithmetics/minimization/false_min.def(3)"false_min/a // @Hind /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_pred.def(4)"monotonic_pred/a/span/span/ ] ] qed. -theorem true_to_le_min: ∀f.∀n,m,b. - b ≤ m → f m = true → min n b f ≤ m. +img class="anchor" src="icons/tick.png" id="true_to_le_min"theorem true_to_le_min: ∀f.∀n,m,b. + b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m. #f #n (elim n) // -#i #Hind #m #b #leb (cases (le_to_or_lt_eq … leb)) +#i #Hind #m #b #leb (cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … leb)) [#ltm #fm normalize (cases (f b)) normalize // @Hind // |#eqm eqb normalize // ] qed. -theorem lt_min_to_false: ∀f.∀n,m,b. - b ≤ m → m < min n b f → f m = false. -#f #n #m #b #lebm #ltm cases(true_or_false (f m)) // -#fm @False_ind @(absurd … ltm) @(le_to_not_lt) @true_to_le_min // +img class="anchor" src="icons/tick.png" id="lt_min_to_false"theorem lt_min_to_false: ∀f.∀n,m,b. + b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a. +#f #n #m #b #lebm #ltm cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f m)) // +#fm @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … ltm) @(a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a) @a href="cic:/matita/arithmetics/minimization/true_to_le_min.def(6)"true_to_le_min/a // qed. -theorem fmin_true: ∀f.∀n,m,b. - m = min n b f → m < n + b → f m = true. +img class="anchor" src="icons/tick.png" id="fmin_true"theorem fmin_true: ∀f.∀n,m,b. + m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f → m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #f #n (elim n) - [#m #b normalize #eqmb >eqmb #leSb @(False_ind) - @(absurd … leSb) // - |#n #Hind #m #b (cases (true_or_false (f b))) #caseb - [>true_min // - |>false_min // #eqm #ltm @(Hind m (S b)) /2/ + [#m #b normalize #eqmb >eqmb #leSb @(a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a) + @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … leSb) // + |#n #Hind #m #b (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f b))) #caseb + [>a href="cic:/matita/arithmetics/minimization/true_min.def(4)"true_min/a // + |>a href="cic:/matita/arithmetics/minimization/false_min.def(3)"false_min/a // #eqm #ltm @(Hind m (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a b)) /span class="autotactic"2span class="autotrace" trace /span/span/ ] ] qed. -lemma min_exists: ∀f.∀t,m. m < t → f m = true → -∀k,b.b ≤ m → (∀i. b ≤ i → i < m → f i = false) → t = k + b → - min k b f = m. +img class="anchor" src="icons/tick.png" id="min_exists"lemma min_exists: ∀f.∀t,m. m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a t → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → +∀k,b.b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → (∀i. b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → t a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a k a title="natural plus" href="cic:/fakeuri.def(1)"+/a b → + a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a k b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m. #f #t #m #ltmt #fm #k (elim k) - [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) false_min /2/ @Hind // - [#i #H #H1 @ismin /2/ | >eqt normalize //] - |#eqbm >true_min // + [#b #lebm #ismin #eqtb @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … lebm) a href="cic:/matita/arithmetics/minimization/false_min.def(3)"false_min/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a/span/span/ @Hind // + [#i #H #H1 @ismin /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ | >eqt normalize //] + |#eqbm >a href="cic:/matita/arithmetics/minimization/true_min.def(4)"true_min/a // ] ] qed. -lemma min_not_exists: ∀f.∀n,b. - (∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b. +img class="anchor" src="icons/tick.png" id="min_not_exists"lemma min_not_exists: ∀f.∀n,b. + (∀i. b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b. #f #n (elim n) // -#p #Hind #b #ffalse >false_min - [>Hind // #i #H #H1 @ffalse /2/ +#p #Hind #b #ffalse >a href="cic:/matita/arithmetics/minimization/false_min.def(3)"false_min/a + [>Hind // #i #H #H1 @ffalse /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ |@ffalse // ] qed. -lemma fmin_false: ∀f.∀n,b.let m ≝ min n b f in - f m = false → m = n+b. +img class="anchor" src="icons/tick.png" id="fmin_false"lemma fmin_false: ∀f.∀n,b.let m ≝ a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f in + f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a na title="natural plus" href="cic:/fakeuri.def(1)"+/ab. #f #n (elim n) // -#i #Hind #b normalize cases(true_or_false … (f b)) #fb >fb +#i #Hind #b normalize cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (f b)) #fb >fb normalize - [#eqm @False_ind @(absurd … fb) // - |>plus_n_Sm @Hind] + [#eqm @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … fb) // + |>a href="cic:/matita/arithmetics/nat/plus_n_Sm.def(4)"plus_n_Sm/a @Hind] qed. -inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝ - | found : ∀m:nat. b ≤ m → m < n + b → f m =true → - (∀i. b ≤ i → i < m → f i = false) → min_spec n b f m - | not_found: (∀i.b ≤ i → i < (n + b) → f i = false) → min_spec n b f (n+b). +img class="anchor" src="icons/tick.png" id="min_spec"inductive min_spec (n,b:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a) (f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) : a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a→Prop ≝ + | found : ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b → f m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → + (∀i. b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → min_spec n b f m + | not_found: (∀i.b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a (n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b) → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a) → + min_spec n b f (na title="natural plus" href="cic:/fakeuri.def(1)"+/ab). -theorem min_spec_to_min: ∀f.∀n,b,m. - min_spec n b f m → min n b f = m. +img class="anchor" src="icons/tick.png" id="min_spec_to_min"theorem min_spec_to_min: ∀f.∀n,b,m. + a href="cic:/matita/arithmetics/minimization/min_spec.ind(1,0,3)"min_spec/a n b f m → a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m. #f #n #b #m #spec (cases spec) - [#m #lem #ltm #fm #ismin @(min_exists f (n+b)) // @ismin - |#ffalse @min_not_exists @ffalse + [#m #lem #ltm #fm #ismin @(a href="cic:/matita/arithmetics/minimization/min_exists.def(9)"min_exists/a f (na title="natural plus" href="cic:/fakeuri.def(1)"+/ab)) // @ismin + |#ffalse @a href="cic:/matita/arithmetics/minimization/min_not_exists.def(9)"min_not_exists/a @ffalse ] qed. -theorem min_to_min_spec: ∀f.∀n,b,m. - min n b f = m → min_spec n b f m. +img class="anchor" src="icons/tick.png" id="min_to_min_spec"theorem min_to_min_spec: ∀f.∀n,b,m. + a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a m → a href="cic:/matita/arithmetics/minimization/min_spec.ind(1,0,3)"min_spec/a n b f m. #f #n #b #m (cases n) - [#eqm eqm #lem - (cases (le_to_or_lt_eq … lem)) #mcase - [%1 /2/ #i #H #H1 @(lt_min_to_false f (S n) i b) // - |>mcase %2 #i #lebi #lti @(lt_min_to_false f (S n) i b) // + lapply (a href="cic:/matita/arithmetics/minimization/le_min_r.def(9)"le_min_r/a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) b) >eqm #lem + (cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … lem)) #mcase + [%1 /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/minimization/fmin_true.def(7)"fmin_true/a/span/span/ #i #H #H1 @(a href="cic:/matita/arithmetics/minimization/lt_min_to_false.def(9)"lt_min_to_false/a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) i b) // + |>mcase %2 #i #lebi #lti @(a href="cic:/matita/arithmetics/minimization/lt_min_to_false.def(9)"lt_min_to_false/a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n) i b) // ] ] qed. -theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) → - min n b f = min n b g. +img class="anchor" src="icons/tick.png" id="min_f_g"theorem min_f_g: ∀f,g,n,b.(∀i. b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g i) → + a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b g. #f #g #n (elim n) // -#m #Hind #b #ext normalize >(ext b (le_n b) ?) // >Hind // -#i #ltib #ltim @ext /2/ +#m #Hind #b #ext normalize >(ext b (a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"le_n/a b) ?) // >Hind // +#i #ltib #ltim @ext /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ qed. -theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) → -min n b g ≤ min n b f. +img class="anchor" src="icons/tick.png" id="le_min_f_min_g"theorem le_min_f_min_g: ∀f,g,n,b. + (∀i. b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/ab → f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → g i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → + a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b g a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f. #f #g #n (elim n) // -#m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq +#m #Hind #b #ext normalize (cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f b))) #Heq >Heq [>ext // - |(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi - @ext /2/ + |(cases (g b)) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ @Hind #i #ltb #ltim #fi + @ext /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_b.def(8)"le_plus_b/a/span/span/ qed. -theorem f_min_true : ∀ f.∀n,b. -(∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → f (min n b f) = true. -#f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) // -#Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/ +img class="anchor" src="icons/tick.png" id="f_min_true"theorem f_min_true : ∀ f.∀n,b. +(∃i:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/aa title="exists" href="cic:/fakeuri.def(1)"./a b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i a title="logical and" href="cic:/fakeuri.def(1)"∧/a i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="logical and" href="cic:/fakeuri.def(1)"∧/a f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → f (a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. +#f #n #b cases(a href="cic:/matita/arithmetics/minimization/min_to_min_spec.def(10)"min_to_min_spec/a f n b (a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f) (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a …)) // +#Hall * #x * * #leb #ltx #fx @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … fx) >Hall /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a/span/span/ +qed. + +img class="anchor" src="icons/tick.png" id="lt_min"theorem lt_min : ∀ f.∀n,b. +(∃i:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/aa title="exists" href="cic:/fakeuri.def(1)"./a b a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i a title="logical and" href="cic:/fakeuri.def(1)"∧/a i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="logical and" href="cic:/fakeuri.def(1)"∧/a f i a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → a href="cic:/matita/arithmetics/minimization/min.fix(0,0,1)"min/a n b f a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="natural plus" href="cic:/fakeuri.def(1)"+/a b. +#f #n #b #H cases H #i * * #lebi #ltin #fi_true +@(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a … ltin) @a href="cic:/matita/arithmetics/minimization/true_to_le_min.def(6)"true_to_le_min/a // qed.