helm/software/matita/contribs/procedural/CoRN/fta/KeyLemma.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: KeyLemma.v,v 1.5 2004/04/23 10:00:57 lcf Exp $ *)
  20
  21 include "reals/NRootIR.ma".
  22
  23 (*#* printing p3m %\ensuremath{\frac13\hat{\ }}% *)
  24
  25 (*#* printing Halfeps %\ensuremath{\frac\varepsilon2}% *)
  26
  27 (*#* * Technical lemmas for the FTA
  28 ** Key Lemma
  29 *)
  30
  31 (* UNEXPORTED
  32 Section Key_Lemma
  33 *)
  34
  35 (*#*
  36 %\begin{convention}% Let [a:nat->IR] and [n:nat] such that [0 < n],
  37 [forall (k : nat) (Zero [<=] (a k))], [(a n) [=] One] and [a_0 : IR],
  38 and [eps : IR] such that [(Zero [<] eps)] and [(eps [<=] a_0)].
  39 %\end{convention}%
  40 *)
  41
  42 (* UNEXPORTED
  43 cic:/CoRN/fta/KeyLemma/Key_Lemma/a.var
  44 *)
  45
  46 (* UNEXPORTED
  47 cic:/CoRN/fta/KeyLemma/Key_Lemma/n.var
  48 *)
  49
  50 (* UNEXPORTED
  51 cic:/CoRN/fta/KeyLemma/Key_Lemma/gt_n_0.var
  52 *)
  53
  54 (* UNEXPORTED
  55 cic:/CoRN/fta/KeyLemma/Key_Lemma/eps.var
  56 *)
  57
  58 (* UNEXPORTED
  59 cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_pos.var
  60 *)
  61
  62 (* UNEXPORTED
  63 cic:/CoRN/fta/KeyLemma/Key_Lemma/a_nonneg.var
  64 *)
  65
  66 (* UNEXPORTED
  67 cic:/CoRN/fta/KeyLemma/Key_Lemma/a_n_1.var
  68 *)
  69
  70 (* UNEXPORTED
  71 cic:/CoRN/fta/KeyLemma/Key_Lemma/a_0.var
  72 *)
  73
  74 (* UNEXPORTED
  75 cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_le_a_0.var
  76 *)
  77
  78 inline procedural "cic:/CoRN/fta/KeyLemma/a_0_eps_nonneg.con" as lemma.
  79
  80 inline procedural "cic:/CoRN/fta/KeyLemma/a_0_eps_fuzz.con" as lemma.
  81
  82 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1a.con" as lemma.
  83
  84 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1b.con" as lemma.
  85
  86 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1c.con" as lemma.
  87
  88 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1.con" as lemma.
  89
  90 inline procedural "cic:/CoRN/fta/KeyLemma/p3m.con" as definition.
  91
  92 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_pos.con" as lemma.
  93
  94 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_S.con" as lemma.
  95
  96 (* UNEXPORTED
  97 Hint Resolve p3m_S: algebra.
  98 *)
  99
 100 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_P.con" as lemma.
 101
 102 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_aux.con" as lemma.
 103
 104 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_pow.con" as lemma.
 105
 106 (* UNEXPORTED
 107 Hint Resolve p3m_aux: algebra.
 108 *)
 109
 110 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_0.con" as lemma.
 111
 112 (* UNEXPORTED
 113 Hint Resolve p3m_0: algebra.
 114 *)
 115
 116 inline procedural "cic:/CoRN/fta/KeyLemma/third_pos.con" as lemma.
 117
 118 (* UNEXPORTED
 119 Hint Resolve third_pos: algebra.
 120 *)
 121
 122 inline procedural "cic:/CoRN/fta/KeyLemma/third_less_one.con" as lemma.
 123
 124 (* UNEXPORTED
 125 Hint Resolve third_less_one: algebra.
 126 *)
 127
 128 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_mon.con" as lemma.
 129
 130 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_mon'.con" as lemma.
 131
 132 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_small.con" as lemma.
 133
 134 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_smaller.con" as lemma.
 135
 136 inline procedural "cic:/CoRN/fta/KeyLemma/chfun.con" as definition.
 137
 138 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_1.con" as lemma.
 139
 140 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_2.con" as lemma.
 141
 142 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_3.con" as lemma.
 143
 144 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_4.con" as lemma.
 145
 146 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps.con" as definition.
 147
 148 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_pos.con" as lemma.
 149
 150 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_Halfeps.con" as lemma.
 151
 152 (* UNEXPORTED
 153 Hint Resolve Halfeps_Halfeps: algebra.
 154 *)
 155
 156 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_eps.con" as lemma.
 157
 158 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_trans.con" as lemma.
 159
 160 inline procedural "cic:/CoRN/fta/KeyLemma/Key_1a.con" as lemma.
 161
 162 (* UNEXPORTED
 163 Hint Resolve Key_1a: algebra.
 164 *)
 165
 166 inline procedural "cic:/CoRN/fta/KeyLemma/Key_1b.con" as lemma.
 167
 168 inline procedural "cic:/CoRN/fta/KeyLemma/Key_1.con" as lemma.
 169
 170 inline procedural "cic:/CoRN/fta/KeyLemma/Key_2.con" as lemma.
 171
 172 inline procedural "cic:/CoRN/fta/KeyLemma/Key.con" as lemma.
 173
 174 (* end hide *)
 175
 176 (* UNEXPORTED
 177 End Key_Lemma
 178 *)
 179
 180 (* UNEXPORTED
 181 Hint Resolve p3m_S p3m_P p3m_pow: algebra.
 182 *)
 183