matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.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/LambdaDelta-1/ty3/arity_props".
  18
  19 include "ty3/arity.ma".
  20
  21 include "ty3/fwd.ma".
  22
  23 include "sc3/arity.ma".
  24
  25 theorem ty3_predicative:
  26  \forall (g: G).(\forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (u:
  27 T).((ty3 g c (THead (Bind Abst) v t) u) \to ((pc3 c u v) \to (\forall (P:
  28 Prop).P)))))))
  29 \def
  30  \lambda (g: G).(\lambda (c: C).(\lambda (v: T).(\lambda (t: T).(\lambda (u:
  31 T).(\lambda (H: (ty3 g c (THead (Bind Abst) v t) u)).(\lambda (H0: (pc3 c u
  32 v)).(\lambda (P: Prop).(let H1 \def H in (ex4_3_ind T T T (\lambda (t2:
  33 T).(\lambda (_: T).(\lambda (_: T).(pc3 c (THead (Bind Abst) v t2) u))))
  34 (\lambda (_: T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c v t0)))) (\lambda
  35 (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) v) t
  36 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t1: T).(ty3 g (CHead c
  37 (Bind Abst) v) t2 t1)))) P (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2:
  38 T).(\lambda (_: (pc3 c (THead (Bind Abst) v x0) u)).(\lambda (H3: (ty3 g c v
  39 x1)).(\lambda (_: (ty3 g (CHead c (Bind Abst) v) t x0)).(\lambda (_: (ty3 g
  40 (CHead c (Bind Abst) v) x0 x2)).(let H_y \def (ty3_conv g c v x1 H3 (THead
  41 (Bind Abst) v t) u H H0) in (let H_x \def (ty3_arity g c (THead (Bind Abst) v
  42 t) v H_y) in (let H6 \def H_x in (ex2_ind A (\lambda (a1: A).(arity g c
  43 (THead (Bind Abst) v t) a1)) (\lambda (a1: A).(arity g c v (asucc g a1))) P
  44 (\lambda (x: A).(\lambda (H7: (arity g c (THead (Bind Abst) v t) x)).(\lambda
  45 (H8: (arity g c v (asucc g x))).(let H9 \def (arity_gen_abst g c v t x H7) in
  46 (ex3_2_ind A A (\lambda (a1: A).(\lambda (a2: A).(eq A x (AHead a1 a2))))
  47 (\lambda (a1: A).(\lambda (_: A).(arity g c v (asucc g a1)))) (\lambda (_:
  48 A).(\lambda (a2: A).(arity g (CHead c (Bind Abst) v) t a2))) P (\lambda (x3:
  49 A).(\lambda (x4: A).(\lambda (H10: (eq A x (AHead x3 x4))).(\lambda (H11:
  50 (arity g c v (asucc g x3))).(\lambda (_: (arity g (CHead c (Bind Abst) v) t
  51 x4)).(let H13 \def (eq_ind A x (\lambda (a: A).(arity g c v (asucc g a))) H8
  52 (AHead x3 x4) H10) in (leq_ahead_asucc_false g x3 (asucc g x4) (arity_mono g
  53 c v (asucc g (AHead x3 x4)) H13 (asucc g x3) H11) P))))))) H9)))))
  54 H6))))))))))) (ty3_gen_bind g Abst c v t u H1)))))))))).
  55
  56 theorem ty3_repellent:
  57  \forall (g: G).(\forall (c: C).(\forall (w: T).(\forall (t: T).(\forall (u1:
  58 T).((ty3 g c (THead (Bind Abst) w t) u1) \to (\forall (u2: T).((ty3 g (CHead
  59 c (Bind Abst) w) t (lift (S O) O u2)) \to ((pc3 c u1 u2) \to (\forall (P:
  60 Prop).P)))))))))
  61 \def
  62  \lambda (g: G).(\lambda (c: C).(\lambda (w: T).(\lambda (t: T).(\lambda (u1:
  63 T).(\lambda (H: (ty3 g c (THead (Bind Abst) w t) u1)).(\lambda (u2:
  64 T).(\lambda (H0: (ty3 g (CHead c (Bind Abst) w) t (lift (S O) O
  65 u2))).(\lambda (H1: (pc3 c u1 u2)).(\lambda (P: Prop).(ex_ind T (\lambda (t0:
  66 T).(ty3 g (CHead c (Bind Abst) w) (lift (S O) O u2) t0)) P (\lambda (x:
  67 T).(\lambda (H2: (ty3 g (CHead c (Bind Abst) w) (lift (S O) O u2) x)).(let H3
  68 \def (ty3_gen_lift g (CHead c (Bind Abst) w) u2 x (S O) O H2 c (drop_drop
  69 (Bind Abst) O c c (drop_refl c) w)) in (ex2_ind T (\lambda (t2: T).(pc3
  70 (CHead c (Bind Abst) w) (lift (S O) O t2) x)) (\lambda (t2: T).(ty3 g c u2
  71 t2)) P (\lambda (x0: T).(\lambda (_: (pc3 (CHead c (Bind Abst) w) (lift (S O)
  72 O x0) x)).(\lambda (H5: (ty3 g c u2 x0)).(let H_y \def (ty3_conv g c u2 x0 H5
  73 (THead (Bind Abst) w t) u1 H H1) in (let H_x \def (ty3_arity g (CHead c (Bind
  74 Abst) w) t (lift (S O) O u2) H0) in (let H6 \def H_x in (ex2_ind A (\lambda
  75 (a1: A).(arity g (CHead c (Bind Abst) w) t a1)) (\lambda (a1: A).(arity g
  76 (CHead c (Bind Abst) w) (lift (S O) O u2) (asucc g a1))) P (\lambda (x1:
  77 A).(\lambda (H7: (arity g (CHead c (Bind Abst) w) t x1)).(\lambda (H8: (arity
  78 g (CHead c (Bind Abst) w) (lift (S O) O u2) (asucc g x1))).(let H_x0 \def
  79 (ty3_arity g c (THead (Bind Abst) w t) u2 H_y) in (let H9 \def H_x0 in
  80 (ex2_ind A (\lambda (a1: A).(arity g c (THead (Bind Abst) w t) a1)) (\lambda
  81 (a1: A).(arity g c u2 (asucc g a1))) P (\lambda (x2: A).(\lambda (H10: (arity
  82 g c (THead (Bind Abst) w t) x2)).(\lambda (H11: (arity g c u2 (asucc g
  83 x2))).(arity_repellent g c w t x1 H7 x2 H10 (asucc_inj g x1 x2 (arity_mono g
  84 c u2 (asucc g x1) (arity_gen_lift g (CHead c (Bind Abst) w) u2 (asucc g x1)
  85 (S O) O H8 c (drop_drop (Bind Abst) O c c (drop_refl c) w)) (asucc g x2)
  86 H11)) P)))) H9)))))) H6))))))) H3)))) (ty3_correct g (CHead c (Bind Abst) w)
  87 t (lift (S O) O u2) H0))))))))))).
  88
  89 theorem ty3_acyclic:
  90  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t
  91 u) \to ((pc3 c u t) \to (\forall (P: Prop).P))))))
  92 \def
  93  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (u: T).(\lambda (H:
  94 (ty3 g c t u)).(\lambda (H0: (pc3 c u t)).(\lambda (P: Prop).(let H_y \def
  95 (ty3_conv g c t u H t u H H0) in (let H_x \def (ty3_arity g c t t H_y) in
  96 (let H1 \def H_x in (ex2_ind A (\lambda (a1: A).(arity g c t a1)) (\lambda
  97 (a1: A).(arity g c t (asucc g a1))) P (\lambda (x: A).(\lambda (H2: (arity g
  98 c t x)).(\lambda (H3: (arity g c t (asucc g x))).(leq_asucc_false g x
  99 (arity_mono g c t (asucc g x) H3 x H2) P)))) H1)))))))))).
 100
 101 theorem ty3_sn3:
 102  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t
 103 u) \to (sn3 c t)))))
 104 \def
 105  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (u: T).(\lambda (H:
 106 (ty3 g c t u)).(let H_x \def (ty3_arity g c t u H) in (let H0 \def H_x in
 107 (ex2_ind A (\lambda (a1: A).(arity g c t a1)) (\lambda (a1: A).(arity g c u
 108 (asucc g a1))) (sn3 c t) (\lambda (x: A).(\lambda (H1: (arity g c t
 109 x)).(\lambda (_: (arity g c u (asucc g x))).(sc3_sn3 g x c t (sc3_arity g c t
 110 x H1))))) H0))))))).
 111