helm/software/matita/contribs/CoRN-Procedural/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 alias id "a" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a.var".
  43
  44 alias id "n" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/n.var".
  45
  46 alias id "gt_n_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/gt_n_0.var".
  47
  48 alias id "eps" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps.var".
  49
  50 alias id "eps_pos" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_pos.var".
  51
  52 alias id "a_nonneg" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_nonneg.var".
  53
  54 alias id "a_n_1" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_n_1.var".
  55
  56 alias id "a_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/a_0.var".
  57
  58 alias id "eps_le_a_0" = "cic:/CoRN/fta/KeyLemma/Key_Lemma/eps_le_a_0.var".
  59
  60 inline procedural "cic:/CoRN/fta/KeyLemma/a_0_eps_nonneg.con" as lemma.
  61
  62 inline procedural "cic:/CoRN/fta/KeyLemma/a_0_eps_fuzz.con" as lemma.
  63
  64 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1a.con" as lemma.
  65
  66 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1b.con" as lemma.
  67
  68 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1c.con" as lemma.
  69
  70 inline procedural "cic:/CoRN/fta/KeyLemma/lem_1.con" as lemma.
  71
  72 inline procedural "cic:/CoRN/fta/KeyLemma/p3m.con" as definition.
  73
  74 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_pos.con" as lemma.
  75
  76 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_S.con" as lemma.
  77
  78 (* UNEXPORTED
  79 Hint Resolve p3m_S: algebra.
  80 *)
  81
  82 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_P.con" as lemma.
  83
  84 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_aux.con" as lemma.
  85
  86 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_pow.con" as lemma.
  87
  88 (* UNEXPORTED
  89 Hint Resolve p3m_aux: algebra.
  90 *)
  91
  92 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_0.con" as lemma.
  93
  94 (* UNEXPORTED
  95 Hint Resolve p3m_0: algebra.
  96 *)
  97
  98 inline procedural "cic:/CoRN/fta/KeyLemma/third_pos.con" as lemma.
  99
 100 (* UNEXPORTED
 101 Hint Resolve third_pos: algebra.
 102 *)
 103
 104 inline procedural "cic:/CoRN/fta/KeyLemma/third_less_one.con" as lemma.
 105
 106 (* UNEXPORTED
 107 Hint Resolve third_less_one: algebra.
 108 *)
 109
 110 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_mon.con" as lemma.
 111
 112 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_mon'.con" as lemma.
 113
 114 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_small.con" as lemma.
 115
 116 inline procedural "cic:/CoRN/fta/KeyLemma/p3m_smaller.con" as lemma.
 117
 118 inline procedural "cic:/CoRN/fta/KeyLemma/chfun.con" as definition.
 119
 120 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_1.con" as lemma.
 121
 122 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_2.con" as lemma.
 123
 124 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_3.con" as lemma.
 125
 126 inline procedural "cic:/CoRN/fta/KeyLemma/chfun_4.con" as lemma.
 127
 128 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps.con" as definition.
 129
 130 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_pos.con" as lemma.
 131
 132 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_Halfeps.con" as lemma.
 133
 134 (* UNEXPORTED
 135 Hint Resolve Halfeps_Halfeps: algebra.
 136 *)
 137
 138 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_eps.con" as lemma.
 139
 140 inline procedural "cic:/CoRN/fta/KeyLemma/Halfeps_trans.con" as lemma.
 141
 142 inline procedural "cic:/CoRN/fta/KeyLemma/Key_1a.con" as lemma.
 143
 144 (* UNEXPORTED
 145 Hint Resolve Key_1a: algebra.
 146 *)
 147
 148 inline procedural "cic:/CoRN/fta/KeyLemma/Key_1b.con" as lemma.
 149
 150 inline procedural "cic:/CoRN/fta/KeyLemma/Key_1.con" as lemma.
 151
 152 inline procedural "cic:/CoRN/fta/KeyLemma/Key_2.con" as lemma.
 153
 154 inline procedural "cic:/CoRN/fta/KeyLemma/Key.con" as lemma.
 155
 156 (* end hide *)
 157
 158 (* UNEXPORTED
 159 End Key_Lemma
 160 *)
 161
 162 (* UNEXPORTED
 163 Hint Resolve p3m_S p3m_P p3m_pow: algebra.
 164 *)
 165