helm/software/matita/contribs/CoRN-Procedural/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 alias id "a" = "cic:/CoRN/fta/MainLemma/Main_Lemma/a.var".
  47
  48 alias id "n" = "cic:/CoRN/fta/MainLemma/Main_Lemma/n.var".
  49
  50 alias id "gt_n_0" = "cic:/CoRN/fta/MainLemma/Main_Lemma/gt_n_0.var".
  51
  52 alias id "eps" = "cic:/CoRN/fta/MainLemma/Main_Lemma/eps.var".
  53
  54 alias id "eps_pos" = "cic:/CoRN/fta/MainLemma/Main_Lemma/eps_pos.var".
  55
  56 alias id "a_nonneg" = "cic:/CoRN/fta/MainLemma/Main_Lemma/a_nonneg.var".
  57
  58 alias id "a_n_1" = "cic:/CoRN/fta/MainLemma/Main_Lemma/a_n_1.var".
  59
  60 alias id "a_0" = "cic:/CoRN/fta/MainLemma/Main_Lemma/a_0.var".
  61
  62 alias id "eps_le_a_0" = "cic:/CoRN/fta/MainLemma/Main_Lemma/eps_le_a_0.var".
  63
  64 inline procedural "cic:/CoRN/fta/MainLemma/a_0_pos.con" as lemma.
  65
  66 (*#*
  67 %\begin{convention}% We define the following local abbreviations:
  68  - [two_n := 2 * n]
  69  - [Small := p3m n]
  70  - [Smaller := p3m (two_n * n)]
  71
  72 %\end{convention}%
  73 *)
  74
  75 (* begin hide *)
  76
  77 inline procedural "cic:/CoRN/fta/MainLemma/Main_Lemma/two_n.con" "Main_Lemma__" as definition.
  78
  79 inline procedural "cic:/CoRN/fta/MainLemma/Main_Lemma/Small.con" "Main_Lemma__" as definition.
  80
  81 inline procedural "cic:/CoRN/fta/MainLemma/Main_Lemma/Smaller.con" "Main_Lemma__" as definition.
  82
  83 (* end hide *)
  84
  85 inline procedural "cic:/CoRN/fta/MainLemma/Main_1a'.con" as lemma.
  86
  87 (* end hide *)
  88
  89 inline procedural "cic:/CoRN/fta/MainLemma/Main_1b'.con" as lemma.
  90
  91 (* end hide *)
  92
  93 inline procedural "cic:/CoRN/fta/MainLemma/Main_1a.con" as lemma.
  94
  95 (* end hide *)
  96
  97 inline procedural "cic:/CoRN/fta/MainLemma/Main_1b.con" as lemma.
  98
  99 (* end hide *)
 100
 101 inline procedural "cic:/CoRN/fta/MainLemma/Main_1.con" as lemma.
 102
 103 (* end hide *)
 104
 105 inline procedural "cic:/CoRN/fta/MainLemma/Main_2'.con" as lemma.
 106
 107 inline procedural "cic:/CoRN/fta/MainLemma/Main_2.con" as lemma.
 108
 109 (* end hide *)
 110
 111 inline procedural "cic:/CoRN/fta/MainLemma/Main_3a.con" as lemma.
 112
 113 (* end hide *)
 114
 115 inline procedural "cic:/CoRN/fta/MainLemma/Main_3.con" as lemma.
 116
 117 (* end hide *)
 118
 119 inline procedural "cic:/CoRN/fta/MainLemma/Main.con" as lemma.
 120
 121 (* end hide *)
 122
 123 (* UNEXPORTED
 124 End Main_Lemma
 125 *)
 126