helm/software/matita/contribs/procedural/CoRN/fta/MainLemma.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: MainLemma.v,v 1.3 2004/04/23 10:00:57 lcf Exp $ *)
  20
  21 (*#* printing two_n %\ensuremath{2n}% #2n# *)
  22
  23 (*#* printing Small %\ensuremath{\frac13^n}% *)
  24
  25 (*#* printing Smaller %\ensuremath{\frac13^{2n^2}}% *)
  26
  27 include "reals/CSumsReals.ma".
  28
  29 include "fta/KeyLemma.ma".
  30
  31 (*#* ** Main Lemma
  32 *)
  33
  34 (* UNEXPORTED
  35 Section Main_Lemma
  36 *)
  37
  38 (*#*
  39 %\begin{convention}%
  40 Let [a : nat->IR], [n : nat], [a_0 : IR]  and [eps : IR] such that [0 < n],
  41 [(Zero [<] eps)], [forall (k : nat)(Zero [<=] (a k))], [(a n) [=] One], and
  42 [(eps [<=] a_0)].
  43 %\end{convention}%
  44 *)
  45
  46 (* UNEXPORTED
  47 cic:/CoRN/fta/MainLemma/Main_Lemma/a.var
  48 *)
  49
  50 (* UNEXPORTED
  51 cic:/CoRN/fta/MainLemma/Main_Lemma/n.var
  52 *)
  53
  54 (* UNEXPORTED
  55 cic:/CoRN/fta/MainLemma/Main_Lemma/gt_n_0.var
  56 *)
  57
  58 (* UNEXPORTED
  59 cic:/CoRN/fta/MainLemma/Main_Lemma/eps.var
  60 *)
  61
  62 (* UNEXPORTED
  63 cic:/CoRN/fta/MainLemma/Main_Lemma/eps_pos.var
  64 *)
  65
  66 (* UNEXPORTED
  67 cic:/CoRN/fta/MainLemma/Main_Lemma/a_nonneg.var
  68 *)
  69
  70 (* UNEXPORTED
  71 cic:/CoRN/fta/MainLemma/Main_Lemma/a_n_1.var
  72 *)
  73
  74 (* UNEXPORTED
  75 cic:/CoRN/fta/MainLemma/Main_Lemma/a_0.var
  76 *)
  77
  78 (* UNEXPORTED
  79 cic:/CoRN/fta/MainLemma/Main_Lemma/eps_le_a_0.var
  80 *)
  81
  82 inline procedural "cic:/CoRN/fta/MainLemma/a_0_pos.con" as lemma.
  83
  84 (*#*
  85 %\begin{convention}% We define the following local abbreviations:
  86  - [two_n := 2 * n]
  87  - [Small := p3m n]
  88  - [Smaller := p3m (two_n * n)]
  89
  90 %\end{convention}%
  91 *)
  92
  93 (* begin hide *)
  94
  95 inline procedural "cic:/CoRN/fta/MainLemma/Main_Lemma/two_n.con" "Main_Lemma__" as definition.
  96
  97 inline procedural "cic:/CoRN/fta/MainLemma/Main_Lemma/Small.con" "Main_Lemma__" as definition.
  98
  99 inline procedural "cic:/CoRN/fta/MainLemma/Main_Lemma/Smaller.con" "Main_Lemma__" as definition.
 100
 101 (* end hide *)
 102
 103 inline procedural "cic:/CoRN/fta/MainLemma/Main_1a'.con" as lemma.
 104
 105 (* end hide *)
 106
 107 inline procedural "cic:/CoRN/fta/MainLemma/Main_1b'.con" as lemma.
 108
 109 (* end hide *)
 110
 111 inline procedural "cic:/CoRN/fta/MainLemma/Main_1a.con" as lemma.
 112
 113 (* end hide *)
 114
 115 inline procedural "cic:/CoRN/fta/MainLemma/Main_1b.con" as lemma.
 116
 117 (* end hide *)
 118
 119 inline procedural "cic:/CoRN/fta/MainLemma/Main_1.con" as lemma.
 120
 121 (* end hide *)
 122
 123 inline procedural "cic:/CoRN/fta/MainLemma/Main_2'.con" as lemma.
 124
 125 inline procedural "cic:/CoRN/fta/MainLemma/Main_2.con" as lemma.
 126
 127 (* end hide *)
 128
 129 inline procedural "cic:/CoRN/fta/MainLemma/Main_3a.con" as lemma.
 130
 131 (* end hide *)
 132
 133 inline procedural "cic:/CoRN/fta/MainLemma/Main_3.con" as lemma.
 134
 135 (* end hide *)
 136
 137 inline procedural "cic:/CoRN/fta/MainLemma/Main.con" as lemma.
 138
 139 (* end hide *)
 140
 141 (* UNEXPORTED
 142 End Main_Lemma
 143 *)
 144