matita/contribs/CoRN-Decl/fta/MainLemma.ma

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