matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/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/cimp/props".
  18
  19 include "cimp/defs.ma".
  20
  21 include "getl/getl.ma".
  22
  23 theorem cimp_flat_sx:
  24  \forall (f: F).(\forall (c: C).(\forall (v: T).(cimp (CHead c (Flat f) v)
  25 c)))
  26 \def
  27  \lambda (f: F).(\lambda (c: C).(\lambda (v: T).(\lambda (b: B).(\lambda (d1:
  28 C).(\lambda (w: T).(\lambda (h: nat).(\lambda (H: (getl h (CHead c (Flat f)
  29 v) (CHead d1 (Bind b) w))).(nat_ind (\lambda (n: nat).((getl n (CHead c (Flat
  30 f) v) (CHead d1 (Bind b) w)) \to (ex C (\lambda (d2: C).(getl n c (CHead d2
  31 (Bind b) w)))))) (\lambda (H0: (getl O (CHead c (Flat f) v) (CHead d1 (Bind
  32 b) w))).(ex_intro C (\lambda (d2: C).(getl O c (CHead d2 (Bind b) w))) d1
  33 (getl_intro O c (CHead d1 (Bind b) w) c (drop_refl c) (clear_gen_flat f c
  34 (CHead d1 (Bind b) w) v (getl_gen_O (CHead c (Flat f) v) (CHead d1 (Bind b)
  35 w) H0))))) (\lambda (h0: nat).(\lambda (_: (((getl h0 (CHead c (Flat f) v)
  36 (CHead d1 (Bind b) w)) \to (ex C (\lambda (d2: C).(getl h0 c (CHead d2 (Bind
  37 b) w))))))).(\lambda (H0: (getl (S h0) (CHead c (Flat f) v) (CHead d1 (Bind
  38 b) w))).(ex_intro C (\lambda (d2: C).(getl (S h0) c (CHead d2 (Bind b) w)))
  39 d1 (getl_gen_S (Flat f) c (CHead d1 (Bind b) w) v h0 H0))))) h H)))))))).
  40
  41 theorem cimp_flat_dx:
  42  \forall (f: F).(\forall (c: C).(\forall (v: T).(cimp c (CHead c (Flat f)
  43 v))))
  44 \def
  45  \lambda (f: F).(\lambda (c: C).(\lambda (v: T).(\lambda (b: B).(\lambda (d1:
  46 C).(\lambda (w: T).(\lambda (h: nat).(\lambda (H: (getl h c (CHead d1 (Bind
  47 b) w))).(ex_intro C (\lambda (d2: C).(getl h (CHead c (Flat f) v) (CHead d2
  48 (Bind b) w))) d1 (getl_flat c (CHead d1 (Bind b) w) h H f v))))))))).
  49
  50 theorem cimp_bind:
  51  \forall (c1: C).(\forall (c2: C).((cimp c1 c2) \to (\forall (b: B).(\forall
  52 (v: T).(cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v))))))
  53 \def
  54  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: ((\forall (b: B).(\forall (d1:
  55 C).(\forall (w: T).(\forall (h: nat).((getl h c1 (CHead d1 (Bind b) w)) \to
  56 (ex C (\lambda (d2: C).(getl h c2 (CHead d2 (Bind b) w))))))))))).(\lambda
  57 (b: B).(\lambda (v: T).(\lambda (b0: B).(\lambda (d1: C).(\lambda (w:
  58 T).(\lambda (h: nat).(\lambda (H0: (getl h (CHead c1 (Bind b) v) (CHead d1
  59 (Bind b0) w))).(nat_ind (\lambda (n: nat).((getl n (CHead c1 (Bind b) v)
  60 (CHead d1 (Bind b0) w)) \to (ex C (\lambda (d2: C).(getl n (CHead c2 (Bind b)
  61 v) (CHead d2 (Bind b0) w)))))) (\lambda (H1: (getl O (CHead c1 (Bind b) v)
  62 (CHead d1 (Bind b0) w))).(let H2 \def (f_equal C C (\lambda (e: C).(match e
  63 in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d1 | (CHead c _ _)
  64 \Rightarrow c])) (CHead d1 (Bind b0) w) (CHead c1 (Bind b) v) (clear_gen_bind
  65 b c1 (CHead d1 (Bind b0) w) v (getl_gen_O (CHead c1 (Bind b) v) (CHead d1
  66 (Bind b0) w) H1))) in ((let H3 \def (f_equal C B (\lambda (e: C).(match e in
  67 C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b0 | (CHead _ k _)
  68 \Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b1)
  69 \Rightarrow b1 | (Flat _) \Rightarrow b0])])) (CHead d1 (Bind b0) w) (CHead
  70 c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1 (Bind b0) w) v (getl_gen_O
  71 (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1))) in ((let H4 \def (f_equal
  72 C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
  73 \Rightarrow w | (CHead _ _ t) \Rightarrow t])) (CHead d1 (Bind b0) w) (CHead
  74 c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1 (Bind b0) w) v (getl_gen_O
  75 (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1))) in (\lambda (H5: (eq B b0
  76 b)).(\lambda (_: (eq C d1 c1)).(eq_ind_r T v (\lambda (t: T).(ex C (\lambda
  77 (d2: C).(getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b0) t))))) (eq_ind_r B
  78 b (\lambda (b1: B).(ex C (\lambda (d2: C).(getl O (CHead c2 (Bind b) v)
  79 (CHead d2 (Bind b1) v))))) (ex_intro C (\lambda (d2: C).(getl O (CHead c2
  80 (Bind b) v) (CHead d2 (Bind b) v))) c2 (getl_refl b c2 v)) b0 H5) w H4))))
  81 H3)) H2))) (\lambda (h0: nat).(\lambda (_: (((getl h0 (CHead c1 (Bind b) v)
  82 (CHead d1 (Bind b0) w)) \to (ex C (\lambda (d2: C).(getl h0 (CHead c2 (Bind
  83 b) v) (CHead d2 (Bind b0) w))))))).(\lambda (H1: (getl (S h0) (CHead c1 (Bind
  84 b) v) (CHead d1 (Bind b0) w))).(let H_x \def (H b0 d1 w (r (Bind b) h0)
  85 (getl_gen_S (Bind b) c1 (CHead d1 (Bind b0) w) v h0 H1)) in (let H2 \def H_x
  86 in (ex_ind C (\lambda (d2: C).(getl (r (Bind b) h0) c2 (CHead d2 (Bind b0)
  87 w))) (ex C (\lambda (d2: C).(getl (S h0) (CHead c2 (Bind b) v) (CHead d2
  88 (Bind b0) w)))) (\lambda (x: C).(\lambda (H3: (getl (r (Bind b) h0) c2 (CHead
  89 x (Bind b0) w))).(ex_intro C (\lambda (d2: C).(getl (S h0) (CHead c2 (Bind b)
  90 v) (CHead d2 (Bind b0) w))) x (getl_head (Bind b) h0 c2 (CHead x (Bind b0) w)
  91 H3 v)))) H2)))))) h H0)))))))))).
  92
  93 theorem cimp_getl_conf:
  94  \forall (c1: C).(\forall (c2: C).((cimp c1 c2) \to (\forall (b: B).(\forall
  95 (d1: C).(\forall (w: T).(\forall (i: nat).((getl i c1 (CHead d1 (Bind b) w))
  96 \to (ex2 C (\lambda (d2: C).(cimp d1 d2)) (\lambda (d2: C).(getl i c2 (CHead
  97 d2 (Bind b) w)))))))))))
  98 \def
  99  \lambda (c1: C).(\lambda (c2: C).(\lambda (H: ((\forall (b: B).(\forall (d1:
 100 C).(\forall (w: T).(\forall (h: nat).((getl h c1 (CHead d1 (Bind b) w)) \to
 101 (ex C (\lambda (d2: C).(getl h c2 (CHead d2 (Bind b) w))))))))))).(\lambda
 102 (b: B).(\lambda (d1: C).(\lambda (w: T).(\lambda (i: nat).(\lambda (H0: (getl
 103 i c1 (CHead d1 (Bind b) w))).(let H_x \def (H b d1 w i H0) in (let H1 \def
 104 H_x in (ex_ind C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind b) w))) (ex2 C
 105 (\lambda (d2: C).(\forall (b0: B).(\forall (d3: C).(\forall (w0: T).(\forall
 106 (h: nat).((getl h d1 (CHead d3 (Bind b0) w0)) \to (ex C (\lambda (d4:
 107 C).(getl h d2 (CHead d4 (Bind b0) w0)))))))))) (\lambda (d2: C).(getl i c2
 108 (CHead d2 (Bind b) w)))) (\lambda (x: C).(\lambda (H2: (getl i c2 (CHead x
 109 (Bind b) w))).(ex_intro2 C (\lambda (d2: C).(\forall (b0: B).(\forall (d3:
 110 C).(\forall (w0: T).(\forall (h: nat).((getl h d1 (CHead d3 (Bind b0) w0))
 111 \to (ex C (\lambda (d4: C).(getl h d2 (CHead d4 (Bind b0) w0))))))))))
 112 (\lambda (d2: C).(getl i c2 (CHead d2 (Bind b) w))) x (\lambda (b0:
 113 B).(\lambda (d0: C).(\lambda (w0: T).(\lambda (h: nat).(\lambda (H3: (getl h
 114 d1 (CHead d0 (Bind b0) w0))).(let H_y \def (getl_trans (S h) c1 (CHead d1
 115 (Bind b) w) i H0) in (let H_x0 \def (H b0 d0 w0 (plus (S h) i) (H_y (CHead d0
 116 (Bind b0) w0) (getl_head (Bind b) h d1 (CHead d0 (Bind b0) w0) H3 w))) in
 117 (let H4 \def H_x0 in (ex_ind C (\lambda (d2: C).(getl (plus (S h) i) c2
 118 (CHead d2 (Bind b0) w0))) (ex C (\lambda (d2: C).(getl h x (CHead d2 (Bind
 119 b0) w0)))) (\lambda (x0: C).(\lambda (H5: (getl (plus (S h) i) c2 (CHead x0
 120 (Bind b0) w0))).(let H_y0 \def (getl_conf_le (plus (S h) i) (CHead x0 (Bind
 121 b0) w0) c2 H5 (CHead x (Bind b) w) i H2) in (let H6 \def (eq_ind nat (minus
 122 (plus (S h) i) i) (\lambda (n: nat).(getl n (CHead x (Bind b) w) (CHead x0
 123 (Bind b0) w0))) (H_y0 (le_plus_r (S h) i)) (S h) (minus_plus_r (S h) i)) in
 124 (ex_intro C (\lambda (d2: C).(getl h x (CHead d2 (Bind b0) w0))) x0
 125 (getl_gen_S (Bind b) x (CHead x0 (Bind b0) w0) w h H6)))))) H4))))))))) H2)))
 126 H1)))))))))).
 127