1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "basic_1/cimp/defs.ma".
19 include "basic_1/getl/getl.ma".
22 \forall (f: F).(\forall (c: C).(\forall (v: T).(cimp (CHead c (Flat f) v)
25 \lambda (f: F).(\lambda (c: C).(\lambda (v: T).(\lambda (b: B).(\lambda (d1:
26 C).(\lambda (w: T).(\lambda (h: nat).(\lambda (H: (getl h (CHead c (Flat f)
27 v) (CHead d1 (Bind b) w))).(let TMP_4 \def (\lambda (n: nat).((getl n (CHead
28 c (Flat f) v) (CHead d1 (Bind b) w)) \to (let TMP_3 \def (\lambda (d2:
29 C).(let TMP_1 \def (Bind b) in (let TMP_2 \def (CHead d2 TMP_1 w) in (getl n
30 c TMP_2)))) in (ex C TMP_3)))) in (let TMP_20 \def (\lambda (H0: (getl O
31 (CHead c (Flat f) v) (CHead d1 (Bind b) w))).(let TMP_7 \def (\lambda (d2:
32 C).(let TMP_5 \def (Bind b) in (let TMP_6 \def (CHead d2 TMP_5 w) in (getl O
33 c TMP_6)))) in (let TMP_8 \def (Bind b) in (let TMP_9 \def (CHead d1 TMP_8 w)
34 in (let TMP_10 \def (drop_refl c) in (let TMP_11 \def (Bind b) in (let TMP_12
35 \def (CHead d1 TMP_11 w) in (let TMP_13 \def (Flat f) in (let TMP_14 \def
36 (CHead c TMP_13 v) in (let TMP_15 \def (Bind b) in (let TMP_16 \def (CHead d1
37 TMP_15 w) in (let TMP_17 \def (getl_gen_O TMP_14 TMP_16 H0) in (let TMP_18
38 \def (clear_gen_flat f c TMP_12 v TMP_17) in (let TMP_19 \def (getl_intro O c
39 TMP_9 c TMP_10 TMP_18) in (ex_intro C TMP_7 d1 TMP_19))))))))))))))) in (let
40 TMP_29 \def (\lambda (h0: nat).(\lambda (_: (((getl h0 (CHead c (Flat f) v)
41 (CHead d1 (Bind b) w)) \to (ex C (\lambda (d2: C).(getl h0 c (CHead d2 (Bind
42 b) w))))))).(\lambda (H0: (getl (S h0) (CHead c (Flat f) v) (CHead d1 (Bind
43 b) w))).(let TMP_24 \def (\lambda (d2: C).(let TMP_21 \def (S h0) in (let
44 TMP_22 \def (Bind b) in (let TMP_23 \def (CHead d2 TMP_22 w) in (getl TMP_21
45 c TMP_23))))) in (let TMP_25 \def (Flat f) in (let TMP_26 \def (Bind b) in
46 (let TMP_27 \def (CHead d1 TMP_26 w) in (let TMP_28 \def (getl_gen_S TMP_25 c
47 TMP_27 v h0 H0) in (ex_intro C TMP_24 d1 TMP_28))))))))) in (nat_ind TMP_4
48 TMP_20 TMP_29 h H))))))))))).
51 \forall (f: F).(\forall (c: C).(\forall (v: T).(cimp c (CHead c (Flat f)
54 \lambda (f: F).(\lambda (c: C).(\lambda (v: T).(\lambda (b: B).(\lambda (d1:
55 C).(\lambda (w: T).(\lambda (h: nat).(\lambda (H: (getl h c (CHead d1 (Bind
56 b) w))).(let TMP_5 \def (\lambda (d2: C).(let TMP_1 \def (Flat f) in (let
57 TMP_2 \def (CHead c TMP_1 v) in (let TMP_3 \def (Bind b) in (let TMP_4 \def
58 (CHead d2 TMP_3 w) in (getl h TMP_2 TMP_4)))))) in (let TMP_6 \def (Bind b)
59 in (let TMP_7 \def (CHead d1 TMP_6 w) in (let TMP_8 \def (getl_flat c TMP_7 h
60 H f v) in (ex_intro C TMP_5 d1 TMP_8)))))))))))).
63 \forall (c1: C).(\forall (c2: C).((cimp c1 c2) \to (\forall (b: B).(\forall
64 (v: T).(cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v))))))
66 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: ((\forall (b: B).(\forall (d1:
67 C).(\forall (w: T).(\forall (h: nat).((getl h c1 (CHead d1 (Bind b) w)) \to
68 (ex C (\lambda (d2: C).(getl h c2 (CHead d2 (Bind b) w))))))))))).(\lambda
69 (b: B).(\lambda (v: T).(\lambda (b0: B).(\lambda (d1: C).(\lambda (w:
70 T).(\lambda (h: nat).(\lambda (H0: (getl h (CHead c1 (Bind b) v) (CHead d1
71 (Bind b0) w))).(let TMP_6 \def (\lambda (n: nat).((getl n (CHead c1 (Bind b)
72 v) (CHead d1 (Bind b0) w)) \to (let TMP_5 \def (\lambda (d2: C).(let TMP_1
73 \def (Bind b) in (let TMP_2 \def (CHead c2 TMP_1 v) in (let TMP_3 \def (Bind
74 b0) in (let TMP_4 \def (CHead d2 TMP_3 w) in (getl n TMP_2 TMP_4)))))) in (ex
75 C TMP_5)))) in (let TMP_68 \def (\lambda (H1: (getl O (CHead c1 (Bind b) v)
76 (CHead d1 (Bind b0) w))).(let TMP_7 \def (\lambda (e: C).(match e with
77 [(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) in (let TMP_8 \def
78 (Bind b0) in (let TMP_9 \def (CHead d1 TMP_8 w) in (let TMP_10 \def (Bind b)
79 in (let TMP_11 \def (CHead c1 TMP_10 v) in (let TMP_12 \def (Bind b0) in (let
80 TMP_13 \def (CHead d1 TMP_12 w) in (let TMP_14 \def (Bind b) in (let TMP_15
81 \def (CHead c1 TMP_14 v) in (let TMP_16 \def (Bind b0) in (let TMP_17 \def
82 (CHead d1 TMP_16 w) in (let TMP_18 \def (getl_gen_O TMP_15 TMP_17 H1) in (let
83 TMP_19 \def (clear_gen_bind b c1 TMP_13 v TMP_18) in (let H2 \def (f_equal C
84 C TMP_7 TMP_9 TMP_11 TMP_19) in (let TMP_20 \def (\lambda (e: C).(match e
85 with [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k with
86 [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b0])])) in (let TMP_21 \def
87 (Bind b0) in (let TMP_22 \def (CHead d1 TMP_21 w) in (let TMP_23 \def (Bind
88 b) in (let TMP_24 \def (CHead c1 TMP_23 v) in (let TMP_25 \def (Bind b0) in
89 (let TMP_26 \def (CHead d1 TMP_25 w) in (let TMP_27 \def (Bind b) in (let
90 TMP_28 \def (CHead c1 TMP_27 v) in (let TMP_29 \def (Bind b0) in (let TMP_30
91 \def (CHead d1 TMP_29 w) in (let TMP_31 \def (getl_gen_O TMP_28 TMP_30 H1) in
92 (let TMP_32 \def (clear_gen_bind b c1 TMP_26 v TMP_31) in (let H3 \def
93 (f_equal C B TMP_20 TMP_22 TMP_24 TMP_32) in (let TMP_33 \def (\lambda (e:
94 C).(match e with [(CSort _) \Rightarrow w | (CHead _ _ t) \Rightarrow t])) in
95 (let TMP_34 \def (Bind b0) in (let TMP_35 \def (CHead d1 TMP_34 w) in (let
96 TMP_36 \def (Bind b) in (let TMP_37 \def (CHead c1 TMP_36 v) in (let TMP_38
97 \def (Bind b0) in (let TMP_39 \def (CHead d1 TMP_38 w) in (let TMP_40 \def
98 (Bind b) in (let TMP_41 \def (CHead c1 TMP_40 v) in (let TMP_42 \def (Bind
99 b0) in (let TMP_43 \def (CHead d1 TMP_42 w) in (let TMP_44 \def (getl_gen_O
100 TMP_41 TMP_43 H1) in (let TMP_45 \def (clear_gen_bind b c1 TMP_39 v TMP_44)
101 in (let H4 \def (f_equal C T TMP_33 TMP_35 TMP_37 TMP_45) in (let TMP_66 \def
102 (\lambda (H5: (eq B b0 b)).(\lambda (_: (eq C d1 c1)).(let TMP_51 \def
103 (\lambda (t: T).(let TMP_50 \def (\lambda (d2: C).(let TMP_46 \def (Bind b)
104 in (let TMP_47 \def (CHead c2 TMP_46 v) in (let TMP_48 \def (Bind b0) in (let
105 TMP_49 \def (CHead d2 TMP_48 t) in (getl O TMP_47 TMP_49)))))) in (ex C
106 TMP_50))) in (let TMP_57 \def (\lambda (b1: B).(let TMP_56 \def (\lambda (d2:
107 C).(let TMP_52 \def (Bind b) in (let TMP_53 \def (CHead c2 TMP_52 v) in (let
108 TMP_54 \def (Bind b1) in (let TMP_55 \def (CHead d2 TMP_54 v) in (getl O
109 TMP_53 TMP_55)))))) in (ex C TMP_56))) in (let TMP_62 \def (\lambda (d2:
110 C).(let TMP_58 \def (Bind b) in (let TMP_59 \def (CHead c2 TMP_58 v) in (let
111 TMP_60 \def (Bind b) in (let TMP_61 \def (CHead d2 TMP_60 v) in (getl O
112 TMP_59 TMP_61)))))) in (let TMP_63 \def (getl_refl b c2 v) in (let TMP_64
113 \def (ex_intro C TMP_62 c2 TMP_63) in (let TMP_65 \def (eq_ind_r B b TMP_57
114 TMP_64 b0 H5) in (eq_ind_r T v TMP_51 TMP_65 w H4))))))))) in (let TMP_67
115 \def (TMP_66 H3) in (TMP_67 H2))))))))))))))))))))))))))))))))))))))))))))))
116 in (let TMP_96 \def (\lambda (h0: nat).(\lambda (_: (((getl h0 (CHead c1
117 (Bind b) v) (CHead d1 (Bind b0) w)) \to (ex C (\lambda (d2: C).(getl h0
118 (CHead c2 (Bind b) v) (CHead d2 (Bind b0) w))))))).(\lambda (H1: (getl (S h0)
119 (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w))).(let TMP_69 \def (Bind b) in
120 (let TMP_70 \def (r TMP_69 h0) in (let TMP_71 \def (Bind b) in (let TMP_72
121 \def (Bind b0) in (let TMP_73 \def (CHead d1 TMP_72 w) in (let TMP_74 \def
122 (getl_gen_S TMP_71 c1 TMP_73 v h0 H1) in (let H_x \def (H b0 d1 w TMP_70
123 TMP_74) in (let H2 \def H_x in (let TMP_77 \def (\lambda (d2: C).(let TMP_75
124 \def (Bind b0) in (let TMP_76 \def (CHead d2 TMP_75 w) in (getl h0 c2
125 TMP_76)))) in (let TMP_83 \def (\lambda (d2: C).(let TMP_78 \def (S h0) in
126 (let TMP_79 \def (Bind b) in (let TMP_80 \def (CHead c2 TMP_79 v) in (let
127 TMP_81 \def (Bind b0) in (let TMP_82 \def (CHead d2 TMP_81 w) in (getl TMP_78
128 TMP_80 TMP_82))))))) in (let TMP_84 \def (ex C TMP_83) in (let TMP_95 \def
129 (\lambda (x: C).(\lambda (H3: (getl h0 c2 (CHead x (Bind b0) w))).(let TMP_90
130 \def (\lambda (d2: C).(let TMP_85 \def (S h0) in (let TMP_86 \def (Bind b) in
131 (let TMP_87 \def (CHead c2 TMP_86 v) in (let TMP_88 \def (Bind b0) in (let
132 TMP_89 \def (CHead d2 TMP_88 w) in (getl TMP_85 TMP_87 TMP_89))))))) in (let
133 TMP_91 \def (Bind b) in (let TMP_92 \def (Bind b0) in (let TMP_93 \def (CHead
134 x TMP_92 w) in (let TMP_94 \def (getl_head TMP_91 h0 c2 TMP_93 H3 v) in
135 (ex_intro C TMP_90 x TMP_94)))))))) in (ex_ind C TMP_77 TMP_84 TMP_95
136 H2)))))))))))))))) in (nat_ind TMP_6 TMP_68 TMP_96 h H0))))))))))))).
138 theorem cimp_getl_conf:
139 \forall (c1: C).(\forall (c2: C).((cimp c1 c2) \to (\forall (b: B).(\forall
140 (d1: C).(\forall (w: T).(\forall (i: nat).((getl i c1 (CHead d1 (Bind b) w))
141 \to (ex2 C (\lambda (d2: C).(cimp d1 d2)) (\lambda (d2: C).(getl i c2 (CHead
142 d2 (Bind b) w)))))))))))
144 \lambda (c1: C).(\lambda (c2: C).(\lambda (H: ((\forall (b: B).(\forall (d1:
145 C).(\forall (w: T).(\forall (h: nat).((getl h c1 (CHead d1 (Bind b) w)) \to
146 (ex C (\lambda (d2: C).(getl h c2 (CHead d2 (Bind b) w))))))))))).(\lambda
147 (b: B).(\lambda (d1: C).(\lambda (w: T).(\lambda (i: nat).(\lambda (H0: (getl
148 i c1 (CHead d1 (Bind b) w))).(let H_x \def (H b d1 w i H0) in (let H1 \def
149 H_x in (let TMP_3 \def (\lambda (d2: C).(let TMP_1 \def (Bind b) in (let
150 TMP_2 \def (CHead d2 TMP_1 w) in (getl i c2 TMP_2)))) in (let TMP_7 \def
151 (\lambda (d2: C).(\forall (b0: B).(\forall (d3: C).(\forall (w0: T).(\forall
152 (h: nat).((getl h d1 (CHead d3 (Bind b0) w0)) \to (let TMP_6 \def (\lambda
153 (d4: C).(let TMP_4 \def (Bind b0) in (let TMP_5 \def (CHead d4 TMP_4 w0) in
154 (getl h d2 TMP_5)))) in (ex C TMP_6)))))))) in (let TMP_10 \def (\lambda (d2:
155 C).(let TMP_8 \def (Bind b) in (let TMP_9 \def (CHead d2 TMP_8 w) in (getl i
156 c2 TMP_9)))) in (let TMP_11 \def (ex2 C TMP_7 TMP_10) in (let TMP_82 \def
157 (\lambda (x: C).(\lambda (H2: (getl i c2 (CHead x (Bind b) w))).(let TMP_15
158 \def (\lambda (d2: C).(\forall (b0: B).(\forall (d3: C).(\forall (w0:
159 T).(\forall (h: nat).((getl h d1 (CHead d3 (Bind b0) w0)) \to (let TMP_14
160 \def (\lambda (d4: C).(let TMP_12 \def (Bind b0) in (let TMP_13 \def (CHead
161 d4 TMP_12 w0) in (getl h d2 TMP_13)))) in (ex C TMP_14)))))))) in (let TMP_18
162 \def (\lambda (d2: C).(let TMP_16 \def (Bind b) in (let TMP_17 \def (CHead d2
163 TMP_16 w) in (getl i c2 TMP_17)))) in (let TMP_81 \def (\lambda (b0:
164 B).(\lambda (d0: C).(\lambda (w0: T).(\lambda (h: nat).(\lambda (H3: (getl h
165 d1 (CHead d0 (Bind b0) w0))).(let TMP_19 \def (S h) in (let TMP_20 \def (Bind
166 b) in (let TMP_21 \def (CHead d1 TMP_20 w) in (let H_y \def (getl_trans
167 TMP_19 c1 TMP_21 i H0) in (let TMP_22 \def (S h) in (let TMP_23 \def (plus
168 TMP_22 i) in (let TMP_24 \def (Bind b0) in (let TMP_25 \def (CHead d0 TMP_24
169 w0) in (let TMP_26 \def (Bind b) in (let TMP_27 \def (Bind b0) in (let TMP_28
170 \def (CHead d0 TMP_27 w0) in (let TMP_29 \def (getl_head TMP_26 h d1 TMP_28
171 H3 w) in (let TMP_30 \def (H_y TMP_25 TMP_29) in (let H_x0 \def (H b0 d0 w0
172 TMP_23 TMP_30) in (let H4 \def H_x0 in (let TMP_35 \def (\lambda (d2: C).(let
173 TMP_31 \def (plus h i) in (let TMP_32 \def (S TMP_31) in (let TMP_33 \def
174 (Bind b0) in (let TMP_34 \def (CHead d2 TMP_33 w0) in (getl TMP_32 c2
175 TMP_34)))))) in (let TMP_38 \def (\lambda (d2: C).(let TMP_36 \def (Bind b0)
176 in (let TMP_37 \def (CHead d2 TMP_36 w0) in (getl h x TMP_37)))) in (let
177 TMP_39 \def (ex C TMP_38) in (let TMP_80 \def (\lambda (x0: C).(\lambda (H5:
178 (getl (S (plus h i)) c2 (CHead x0 (Bind b0) w0))).(let TMP_40 \def (plus h i)
179 in (let TMP_41 \def (S TMP_40) in (let TMP_42 \def (Bind b0) in (let TMP_43
180 \def (CHead x0 TMP_42 w0) in (let TMP_44 \def (Bind b) in (let TMP_45 \def
181 (CHead x TMP_44 w) in (let H_y0 \def (getl_conf_le TMP_41 TMP_43 c2 H5 TMP_45
182 i H2) in (let TMP_46 \def (S h) in (let TMP_47 \def (plus TMP_46 i) in (let
183 H6 \def (refl_equal nat TMP_47) in (let TMP_48 \def (plus h i) in (let TMP_49
184 \def (S TMP_48) in (let TMP_55 \def (\lambda (n: nat).(let TMP_50 \def (minus
185 n i) in (let TMP_51 \def (Bind b) in (let TMP_52 \def (CHead x TMP_51 w) in
186 (let TMP_53 \def (Bind b0) in (let TMP_54 \def (CHead x0 TMP_53 w0) in (getl
187 TMP_50 TMP_52 TMP_54))))))) in (let TMP_56 \def (plus h i) in (let TMP_57
188 \def (le_plus_r h i) in (let TMP_58 \def (le_S i TMP_56 TMP_57) in (let
189 TMP_59 \def (H_y0 TMP_58) in (let TMP_60 \def (S h) in (let TMP_61 \def (plus
190 TMP_60 i) in (let H7 \def (eq_ind nat TMP_49 TMP_55 TMP_59 TMP_61 H6) in (let
191 TMP_62 \def (S h) in (let TMP_63 \def (plus TMP_62 i) in (let TMP_64 \def
192 (minus TMP_63 i) in (let TMP_69 \def (\lambda (n: nat).(let TMP_65 \def (Bind
193 b) in (let TMP_66 \def (CHead x TMP_65 w) in (let TMP_67 \def (Bind b0) in
194 (let TMP_68 \def (CHead x0 TMP_67 w0) in (getl n TMP_66 TMP_68)))))) in (let
195 TMP_70 \def (S h) in (let TMP_71 \def (S h) in (let TMP_72 \def (minus_plus_r
196 TMP_71 i) in (let H8 \def (eq_ind nat TMP_64 TMP_69 H7 TMP_70 TMP_72) in (let
197 TMP_75 \def (\lambda (d2: C).(let TMP_73 \def (Bind b0) in (let TMP_74 \def
198 (CHead d2 TMP_73 w0) in (getl h x TMP_74)))) in (let TMP_76 \def (Bind b) in
199 (let TMP_77 \def (Bind b0) in (let TMP_78 \def (CHead x0 TMP_77 w0) in (let
200 TMP_79 \def (getl_gen_S TMP_76 x TMP_78 w h H8) in (ex_intro C TMP_75 x0
201 TMP_79)))))))))))))))))))))))))))))))))))) in (ex_ind C TMP_35 TMP_39 TMP_80
202 H4))))))))))))))))))))))))) in (ex_intro2 C TMP_15 TMP_18 x TMP_81 H2))))))
203 in (ex_ind C TMP_3 TMP_11 TMP_82 H1))))))))))))))).