matita/matita/contribs/lambdadelta/ground_1A/types/defs.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 include "ground_1A/preamble.ma".
  18
  19 inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def
  20 | and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))).
  21
  22 inductive and4 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop): Prop \def
  23 | and4_intro: P0 \to (P1 \to (P2 \to (P3 \to (and4 P0 P1 P2 P3)))).
  24
  25 inductive and5 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop) (P4: Prop): Prop
  26 \def
  27 | and5_intro: P0 \to (P1 \to (P2 \to (P3 \to (P4 \to (and5 P0 P1 P2 P3
  28 P4))))).
  29
  30 inductive or3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def
  31 | or3_intro0: P0 \to (or3 P0 P1 P2)
  32 | or3_intro1: P1 \to (or3 P0 P1 P2)
  33 | or3_intro2: P2 \to (or3 P0 P1 P2).
  34
  35 inductive or4 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop): Prop \def
  36 | or4_intro0: P0 \to (or4 P0 P1 P2 P3)
  37 | or4_intro1: P1 \to (or4 P0 P1 P2 P3)
  38 | or4_intro2: P2 \to (or4 P0 P1 P2 P3)
  39 | or4_intro3: P3 \to (or4 P0 P1 P2 P3).
  40
  41 inductive or5 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop) (P4: Prop): Prop
  42 \def
  43 | or5_intro0: P0 \to (or5 P0 P1 P2 P3 P4)
  44 | or5_intro1: P1 \to (or5 P0 P1 P2 P3 P4)
  45 | or5_intro2: P2 \to (or5 P0 P1 P2 P3 P4)
  46 | or5_intro3: P3 \to (or5 P0 P1 P2 P3 P4)
  47 | or5_intro4: P4 \to (or5 P0 P1 P2 P3 P4).
  48
  49 inductive ex3 (A0: Type[0]) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to
  50 Prop): Prop \def
  51 | ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0
  52 P0 P1 P2)))).
  53
  54 inductive ex4 (A0: Type[0]) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to
  55 Prop) (P3: A0 \to Prop): Prop \def
  56 | ex4_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to ((P3 x0)
  57 \to (ex4 A0 P0 P1 P2 P3))))).
  58
  59 inductive ex_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)): Prop
  60 \def
  61 | ex_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to (ex_2 A0 A1
  62 P0))).
  63
  64 inductive ex2_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)) (P1:
  65 A0 \to (A1 \to Prop)): Prop \def
  66 | ex2_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
  67 \to (ex2_2 A0 A1 P0 P1)))).
  68
  69 inductive ex3_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)) (P1:
  70 A0 \to (A1 \to Prop)) (P2: A0 \to (A1 \to Prop)): Prop \def
  71 | ex3_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
  72 \to ((P2 x0 x1) \to (ex3_2 A0 A1 P0 P1 P2))))).
  73
  74 inductive ex4_2 (A0: Type[0]) (A1: Type[0]) (P0: A0 \to (A1 \to Prop)) (P1:
  75 A0 \to (A1 \to Prop)) (P2: A0 \to (A1 \to Prop)) (P3: A0 \to (A1 \to Prop)):
  76 Prop \def
  77 | ex4_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
  78 \to ((P2 x0 x1) \to ((P3 x0 x1) \to (ex4_2 A0 A1 P0 P1 P2 P3)))))).
  79
  80 inductive ex_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to
  81 (A2 \to Prop))): Prop \def
  82 | ex_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1
  83 x2) \to (ex_3 A0 A1 A2 P0)))).
  84
  85 inductive ex2_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to
  86 (A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))): Prop \def
  87 | ex2_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
  88 x1 x2) \to ((P1 x0 x1 x2) \to (ex2_3 A0 A1 A2 P0 P1))))).
  89
  90 inductive ex3_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to
  91 (A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2
  92 \to Prop))): Prop \def
  93 | ex3_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
  94 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to (ex3_3 A0 A1 A2 P0 P1
  95 P2)))))).
  96
  97 inductive ex4_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to
  98 (A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2
  99 \to Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def
 100 | ex4_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
 101 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0
 102 A1 A2 P0 P1 P2 P3))))))).
 103
 104 inductive ex5_3 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (P0: A0 \to (A1 \to
 105 (A2 \to Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2
 106 \to Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))) (P4: A0 \to (A1 \to (A2 \to
 107 Prop))): Prop \def
 108 | ex5_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
 109 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to ((P4 x0
 110 x1 x2) \to (ex5_3 A0 A1 A2 P0 P1 P2 P3 P4)))))))).
 111
 112 inductive ex3_4 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (P0:
 113 A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to
 114 Prop)))) (P2: A0 \to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def
 115 | ex3_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
 116 (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
 117 (ex3_4 A0 A1 A2 A3 P0 P1 P2))))))).
 118
 119 inductive ex4_4 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (P0:
 120 A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to
 121 Prop)))) (P2: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P3: A0 \to (A1 \to (A2
 122 \to (A3 \to Prop)))): Prop \def
 123 | ex4_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
 124 (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
 125 ((P3 x0 x1 x2 x3) \to (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)))))))).
 126
 127 inductive ex4_5 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4:
 128 Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to
 129 (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to
 130 (A4 \to Prop))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop
 131 \def
 132 | ex4_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
 133 (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to
 134 ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to (ex4_5 A0 A1 A2 A3 A4 P0 P1
 135 P2 P3))))))))).
 136
 137 inductive ex5_5 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4:
 138 Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to
 139 (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to
 140 (A4 \to Prop))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4:
 141 A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def
 142 | ex5_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
 143 (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to
 144 ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1 x2 x3 x4) \to
 145 (ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4)))))))))).
 146
 147 inductive ex6_6 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4:
 148 Type[0]) (A5: Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to
 149 Prop)))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop))))))
 150 (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P3: A0 \to
 151 (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P4: A0 \to (A1 \to (A2
 152 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to
 153 (A4 \to (A5 \to Prop)))))): Prop \def
 154 | ex6_6_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
 155 (x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1
 156 x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5)
 157 \to ((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to (ex6_6 A0 A1 A2
 158 A3 A4 A5 P0 P1 P2 P3 P4 P5)))))))))))).
 159
 160 inductive ex6_7 (A0: Type[0]) (A1: Type[0]) (A2: Type[0]) (A3: Type[0]) (A4:
 161 Type[0]) (A5: Type[0]) (A6: Type[0]) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4
 162 \to (A5 \to (A6 \to Prop))))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to
 163 (A5 \to (A6 \to Prop))))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5
 164 \to (A6 \to Prop))))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to
 165 (A6 \to Prop))))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6
 166 \to Prop))))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
 167 Prop))))))): Prop \def
 168 | ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
 169 (x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2
 170 x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6)
 171 \to ((P3 x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6) \to ((P5 x0 x1
 172 x2 x3 x4 x5 x6) \to (ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4
 173 P5))))))))))))).
 174