matita/contribs/LAMBDA-TYPES/Level-1/Base.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/LAMBDA-TYPES/Level-1/Base".
  18
  19 include "legacy/coq.ma".
  20
  21 axiom insert_eq: \forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G: Prop).(((\forall (y: S).((P y) \to ((eq S y x) \to G)))) \to ((P x) \to G))))) .
  22
  23 axiom unintro: \forall (A: Set).(\forall (a: A).(\forall (P: ((A \to Prop))).(((\forall (x: A).(P x))) \to (P a)))) .
  24
  25 axiom xinduction: \forall (A: Set).(\forall (t: A).(\forall (P: ((A \to Prop))).(((\forall (x: A).((eq A t x) \to (P x)))) \to (P t)))) .
  26
  27 axiom nat_dec: \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to (\forall (P: Prop).P)))) .
  28
  29 axiom simpl_plus_r: \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n) (plus p n)) \to (eq nat m p)))) .
  30
  31 axiom minus_plus_r: \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m)) .
  32
  33 axiom plus_permute_2_in_3: \forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x y) z) (plus (plus x z) y)))) .
  34
  35 axiom plus_permute_2_in_3_assoc: \forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n h) k) (plus n (plus k h))))) .
  36
  37 axiom plus_O: \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat x O) (eq nat y O)))) .
  38
  39 axiom minus_Sx_SO: \forall (x: nat).(eq nat (minus (S x) (S O)) x) .
  40
  41 axiom eq_nat_dec: \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j))) .
  42
  43 axiom neq_eq_e: \forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j)) \to P)) \to ((((eq nat i j) \to P)) \to P)))) .
  44
  45 axiom le_false: \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S n) m) \to P)))) .
  46
  47 axiom le_Sx_x: \forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P)) .
  48
  49 axiom minus_le: \forall (x: nat).(\forall (y: nat).(le (minus x y) x)) .
  50
  51 axiom le_plus_minus_sym: \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n) n)))) .
  52
  53 axiom le_minus_minus: \forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z) \to (le (minus y x) (minus z x)))))) .
  54
  55 axiom le_minus_plus: \forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat (minus (plus x y) z) (plus (minus x z) y))))) .
  56
  57 axiom le_minus: \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to (le x (minus z y))))) .
  58
  59 axiom le_trans_plus_r: \forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to (le y z)))) .
  60
  61 axiom le_gen_S: \forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n: nat).(eq nat x (S n))) (\lambda (n: nat).(le m n))))) .
  62
  63 axiom lt_x_plus_x_Sy: \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y)))) .
  64
  65 axiom simpl_lt_plus_r: \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m p)) \to (lt n m)))) .
  66
  67 axiom minus_x_Sy: \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S (minus x (S y)))))) .
  68
  69 axiom lt_plus_minus: \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus y (S x))))))) .
  70
  71 axiom lt_plus_minus_r: \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y (S x)) x))))) .
  72
  73 axiom minus_x_SO: \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O))))) .
  74
  75 axiom le_x_pred_y: \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y)))) .
  76
  77 axiom lt_le_minus: \forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O))))) .
  78
  79 axiom lt_le_e: \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P)) \to ((((le d n) \to P)) \to P)))) .
  80
  81 axiom lt_eq_e: \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) \to ((((eq nat x y) \to P)) \to ((le x y) \to P))))) .
  82
  83 axiom lt_eq_gt_e: \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) \to ((((eq nat x y) \to P)) \to ((((lt y x) \to P)) \to P))))) .
  84
  85 axiom lt_gen_xS: \forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2 nat (\lambda (m: nat).(eq nat x (S m))) (\lambda (m: nat).(lt m n)))))) .
  86
  87 axiom le_lt_false: \forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P: Prop).P)))) .
  88
  89 axiom lt_neq: \forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y)))) .
  90
  91 axiom arith0: \forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n) \to (\forall (h1: nat).(le (plus d2 h1) (minus (plus n h1) h2)))))) .
  92
  93 axiom O_minus: \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O))) .
  94
  95 axiom minus_minus: \forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y) \to ((eq nat (minus x z) (minus y z)) \to (eq nat x y)))))) .
  96
  97 axiom plus_plus: \forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 z) \to ((le x2 z) \to ((eq nat (plus (minus z x1) y1) (plus (minus z x2) y2)) \to (eq nat (plus x1 y2) (plus x2 y1))))))))) .
  98
  99 axiom ex2_sym: \forall (A: Set).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to Prop))).((ex2 A (\lambda (x: A).(P x)) (\lambda (x: A).(Q x))) \to (ex2 A (\lambda (x: A).(Q x)) (\lambda (x: A).(P x)))))) .
 100
 101 inductive and3 (P0:Prop) (P1:Prop) (P2:Prop): Prop \def
 102 | and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))).
 103
 104 inductive or3 (P0:Prop) (P1:Prop) (P2:Prop): Prop \def
 105 | or3_intro0: P0 \to (or3 P0 P1 P2)
 106 | or3_intro1: P1 \to (or3 P0 P1 P2)
 107 | or3_intro2: P2 \to (or3 P0 P1 P2).
 108
 109 inductive or4 (P0:Prop) (P1:Prop) (P2:Prop) (P3:Prop): Prop \def
 110 | or4_intro0: P0 \to (or4 P0 P1 P2 P3)
 111 | or4_intro1: P1 \to (or4 P0 P1 P2 P3)
 112 | or4_intro2: P2 \to (or4 P0 P1 P2 P3)
 113 | or4_intro3: P3 \to (or4 P0 P1 P2 P3).
 114
 115 inductive ex3 (A0:Set) (P0:A0 \to Prop) (P1:A0 \to Prop) (P2:A0 \to Prop): Prop \def
 116 | ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0 P0 P1 P2)))).
 117
 118 inductive ex4 (A0:Set) (P0:A0 \to Prop) (P1:A0 \to Prop) (P2:A0 \to Prop) (P3:A0 \to Prop): Prop \def
 119 | ex4_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to ((P3 x0) \to (ex4 A0 P0 P1 P2 P3))))).
 120
 121 inductive ex_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)): Prop \def
 122 | ex_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to (ex_2 A0 A1 P0))).
 123
 124 inductive ex2_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)) (P1:A0 \to (A1 \to Prop)): Prop \def
 125 | ex2_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to (ex2_2 A0 A1 P0 P1)))).
 126
 127 inductive ex3_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)) (P1:A0 \to (A1 \to Prop)) (P2:A0 \to (A1 \to Prop)): Prop \def
 128 | ex3_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to ((P2 x0 x1) \to (ex3_2 A0 A1 P0 P1 P2))))).
 129
 130 inductive ex4_2 (A0:Set) (A1:Set) (P0:A0 \to (A1 \to Prop)) (P1:A0 \to (A1 \to Prop)) (P2:A0 \to (A1 \to Prop)) (P3:A0 \to (A1 \to Prop)): Prop \def
 131 | ex4_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) \to ((P2 x0 x1) \to ((P3 x0 x1) \to (ex4_2 A0 A1 P0 P1 P2 P3)))))).
 132
 133 inductive ex_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop))): Prop \def
 134 | ex_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to (ex_3 A0 A1 A2 P0)))).
 135
 136 inductive ex2_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop))) (P1:A0 \to (A1 \to (A2 \to Prop))): Prop \def
 137 | ex2_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to (ex2_3 A0 A1 A2 P0 P1))))).
 138
 139 inductive ex3_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop))) (P1:A0 \to (A1 \to (A2 \to Prop))) (P2:A0 \to (A1 \to (A2 \to Prop))): Prop \def
 140 | ex3_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to (ex3_3 A0 A1 A2 P0 P1 P2)))))).
 141
 142 inductive ex4_3 (A0:Set) (A1:Set) (A2:Set) (P0:A0 \to (A1 \to (A2 \to Prop))) (P1:A0 \to (A1 \to (A2 \to Prop))) (P2:A0 \to (A1 \to (A2 \to Prop))) (P3:A0 \to (A1 \to (A2 \to Prop))): Prop \def
 143 | ex4_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0 A1 A2 P0 P1 P2 P3))))))).
 144
 145 inductive ex3_4 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P1:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2:A0 \to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def
 146 | ex3_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to (ex3_4 A0 A1 A2 A3 P0 P1 P2))))))).
 147
 148 inductive ex4_4 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P1:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2:A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P3:A0 \to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def
 149 | ex4_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to ((P3 x0 x1 x2 x3) \to (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)))))))).
 150
 151 inductive ex4_5 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def
 152 | ex4_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to (ex4_5 A0 A1 A2 A3 A4 P0 P1 P2 P3))))))))).
 153
 154 inductive ex5_5 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def
 155 | ex5_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to ((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1 x2 x3 x4) \to (ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4)))))))))).
 156
 157 inductive ex6_6 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (A5:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P1:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P3:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P4:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P5:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))): Prop \def
 158 | ex6_6_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1 x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5) \to ((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to (ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4 P5)))))))))))).
 159
 160 inductive ex6_7 (A0:Set) (A1:Set) (A2:Set) (A3:Set) (A4:Set) (A5:Set) (A6:Set) (P0:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))) (P1:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))) (P2:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))) (P3:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))) (P4:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))) (P5:A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to Prop))))))): Prop \def
 161 | ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall (x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2 x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6) \to ((P3 x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6) \to ((P5 x0 x1 x2 x3 x4 x5 x6) \to (ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5))))))))))))).
 162
 163 definition blt: nat \to (nat \to bool) \def let rec blt (m: nat) (n: nat): bool \def (match n with [O \Rightarrow false | (S n0) \Rightarrow (match m with [O \Rightarrow true | (S m0) \Rightarrow (blt m0 n0)])]) in blt.
 164
 165 axiom lt_blt: \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq bool (blt y x) true))) .
 166
 167 axiom le_bge: \forall (x: nat).(\forall (y: nat).((le x y) \to (eq bool (blt y x) false))) .
 168
 169 axiom blt_lt: \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) true) \to (lt y x))) .
 170
 171 axiom bge_le: \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y))) .
 172