weblib/arithmetics/minimization.ma

   1 (*
   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.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/nat.ma".
  13
  14 (* maximization *)
  15
  16 \ 5img class="anchor" src="icons/tick.png" id="max'"\ 6let rec max' i f d ≝
  17   match i with
  18   [ O ⇒ d
  19   | S j ⇒
  20       match (f j) with
  21       [ true ⇒ j
  22       | false ⇒ max' j f d]].
  23
  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.
  25
  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.
  27 // qed.
  28
  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.
  33
  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 //
  37 (* non trova Hind *)
  38 @Hind
  39 qed.
  40
  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 //
  44 @le_max_n qed.
  45
  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/
  51 qed.
  52
  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.
  55 #f #n (elim n)
  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/
  57   |#i #Hind #m #ltm
  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 //
  62  ]
  63 qed.
  64
  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 //
  69 qed.
  70
  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.
  73 #f #n (elim n) #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 …)))
  77    #ltm normalize
  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 //
  80      |<ltm >fmax //
  81      ]
  82    ]
  83 qed.
  84
  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/
  89 qed.
  90
  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.
  92 #f #n #m (elim n) //
  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
  94 normalize
  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]
  96 qed.
  97
  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.
 102
 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
 108   ]
 109 qed.
 110
 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.
 113 #f #n #m (cases n)
 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) //
 120 qed.
 121
 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.
 124 #f #g #n (elim n) //
 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/
 127 qed.
 128
 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.
 131 #f #g #n (elim n) //
 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
 133   [>ext //
 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/
 135 qed.
 136
 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/
 141 qed.
 142
 143 (* minimization *)
 144
 145 (* min k b f is the minimun i, b ≤ i < b + k s.t. f i;
 146    returns  b + k otherwise *)
 147
 148 \ 5img class="anchor" src="icons/tick.png" id="min"\ 6let rec min k b f ≝
 149   match k with
 150   [ O ⇒ b
 151   | S p ⇒
 152     match f b with
 153    [ true ⇒ b
 154    | false ⇒ min p (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b) f]].
 155
 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.
 157
 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.
 159 // qed.
 160
 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 //
 164 qed.
 165
 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 //
 169 qed.
 170
 171 (*
 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 *)
 176
 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 //
 180 qed.
 181
 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/
 185 qed.
 186
 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/
 195     ]
 196   ]
 197 qed.
 198
 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.
 201 #f #n (elim n) //
 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 //
 205   ]
 206 qed.
 207
 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 //
 212 qed.
 213
 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.
 216 #f #n (elim n)
 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/
 222     ]
 223   ]
 224 qed.
 225
 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 //
 236     ]
 237   ]
 238 qed.
 239
 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.
 242 #f #n (elim n) //
 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/
 245   |@ffalse //
 246   ]
 247 qed.
 248
 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.
 251 #f #n (elim n) //
 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
 253 normalize
 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]
 256 qed.
 257
 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).
 263
 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
 269   ]
 270 qed.
 271
 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) //
 281     ]
 282   ]
 283 qed.
 284
 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.
 287 #f #g #n (elim n) //
 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/
 290 qed.
 291
 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.
 295 #f #g #n (elim n) //
 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
 297   [>ext //
 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/
 300 qed.
 301
 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/
 306 qed.
 307
 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 //
 312 qed.