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 "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 ex3 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to
  42 Prop): Prop \def
  43 | ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0
  44 P0 P1 P2)))).
  45
  46 inductive ex4 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to Prop)
  47 (P3: A0 \to Prop): Prop \def
  48 | ex4_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to ((P3 x0)
  49 \to (ex4 A0 P0 P1 P2 P3))))).
  50
  51 inductive ex_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)): Prop \def
  52 | ex_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to (ex_2 A0 A1
  53 P0))).
  54
  55 inductive ex2_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to
  56 (A1 \to Prop)): Prop \def
  57 | ex2_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
  58 \to (ex2_2 A0 A1 P0 P1)))).
  59
  60 inductive ex3_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to
  61 (A1 \to Prop)) (P2: A0 \to (A1 \to Prop)): Prop \def
  62 | ex3_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
  63 \to ((P2 x0 x1) \to (ex3_2 A0 A1 P0 P1 P2))))).
  64
  65 inductive ex4_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to
  66 (A1 \to Prop)) (P2: A0 \to (A1 \to Prop)) (P3: A0 \to (A1 \to Prop)): Prop
  67 \def
  68 | ex4_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1)
  69 \to ((P2 x0 x1) \to ((P3 x0 x1) \to (ex4_2 A0 A1 P0 P1 P2 P3)))))).
  70
  71 inductive ex_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
  72 Prop))): Prop \def
  73 | ex_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1
  74 x2) \to (ex_3 A0 A1 A2 P0)))).
  75
  76 inductive ex2_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
  77 Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))): Prop \def
  78 | ex2_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
  79 x1 x2) \to ((P1 x0 x1 x2) \to (ex2_3 A0 A1 A2 P0 P1))))).
  80
  81 inductive ex3_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
  82 Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to
  83 Prop))): Prop \def
  84 | ex3_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
  85 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to (ex3_3 A0 A1 A2 P0 P1
  86 P2)))))).
  87
  88 inductive ex4_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to
  89 Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to
  90 Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def
  91 | ex4_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0
  92 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0
  93 A1 A2 P0 P1 P2 P3))))))).
  94
  95 inductive ex3_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to
  96 (A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0
  97 \to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def
  98 | ex3_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
  99 (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
 100 (ex3_4 A0 A1 A2 A3 P0 P1 P2))))))).
 101
 102 inductive ex4_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to
 103 (A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0
 104 \to (A1 \to (A2 \to (A3 \to Prop)))) (P3: A0 \to (A1 \to (A2 \to (A3 \to
 105 Prop)))): Prop \def
 106 | ex4_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
 107 (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to
 108 ((P3 x0 x1 x2 x3) \to (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)))))))).
 109
 110 inductive ex4_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to
 111 (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to
 112 (A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:
 113 A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def
 114 | ex4_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
 115 (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to
 116 ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to (ex4_5 A0 A1 A2 A3 A4 P0 P1
 117 P2 P3))))))))).
 118
 119 inductive ex5_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to
 120 (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to
 121 (A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:
 122 A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4: A0 \to (A1 \to (A2 \to
 123 (A3 \to (A4 \to Prop))))): Prop \def
 124 | ex5_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
 125 (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to
 126 ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1 x2 x3 x4) \to
 127 (ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4)))))))))).
 128
 129 inductive ex6_6 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set)
 130 (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P1: A0 \to
 131 (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P2: A0 \to (A1 \to (A2
 132 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to
 133 (A4 \to (A5 \to Prop)))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5
 134 \to Prop)))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to
 135 Prop)))))): Prop \def
 136 | ex6_6_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
 137 (x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1
 138 x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5)
 139 \to ((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to (ex6_6 A0 A1 A2
 140 A3 A4 A5 P0 P1 P2 P3 P4 P5)))))))))))).
 141
 142 inductive ex6_7 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set)
 143 (A6: Set) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
 144 Prop))))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
 145 Prop))))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
 146 Prop))))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
 147 Prop))))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
 148 Prop))))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to
 149 Prop))))))): Prop \def
 150 | ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall
 151 (x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2
 152 x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6)
 153 \to ((P3 x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6) \to ((P5 x0 x1
 154 x2 x3 x4 x5 x6) \to (ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4
 155 P5))))))))))))).
 156