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/getl/props.ma".
19 include "Basic-1/clear/drop.ma".
21 theorem clear_getl_trans:
22 \forall (i: nat).(\forall (c2: C).(\forall (c3: C).((getl i c2 c3) \to
23 (\forall (c1: C).((clear c1 c2) \to (getl i c1 c3))))))
25 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c2: C).(\forall (c3:
26 C).((getl n c2 c3) \to (\forall (c1: C).((clear c1 c2) \to (getl n c1
27 c3))))))) (\lambda (c2: C).(\lambda (c3: C).(\lambda (H: (getl O c2
28 c3)).(\lambda (c1: C).(\lambda (H0: (clear c1 c2)).(getl_intro O c1 c3 c1
29 (drop_refl c1) (clear_trans c1 c2 H0 c3 (getl_gen_O c2 c3 H)))))))) (\lambda
30 (n: nat).(\lambda (_: ((\forall (c2: C).(\forall (c3: C).((getl n c2 c3) \to
31 (\forall (c1: C).((clear c1 c2) \to (getl n c1 c3)))))))).(\lambda (c2:
32 C).(C_ind (\lambda (c: C).(\forall (c3: C).((getl (S n) c c3) \to (\forall
33 (c1: C).((clear c1 c) \to (getl (S n) c1 c3)))))) (\lambda (n0: nat).(\lambda
34 (c3: C).(\lambda (H0: (getl (S n) (CSort n0) c3)).(\lambda (c1: C).(\lambda
35 (_: (clear c1 (CSort n0))).(getl_gen_sort n0 (S n) c3 H0 (getl (S n) c1
36 c3))))))) (\lambda (c: C).(\lambda (_: ((\forall (c3: C).((getl (S n) c c3)
37 \to (\forall (c1: C).((clear c1 c) \to (getl (S n) c1 c3))))))).(\lambda (k:
38 K).(\lambda (t: T).(\lambda (c3: C).(\lambda (H1: (getl (S n) (CHead c k t)
39 c3)).(\lambda (c1: C).(\lambda (H2: (clear c1 (CHead c k t))).(K_ind (\lambda
40 (k0: K).((getl (S n) (CHead c k0 t) c3) \to ((clear c1 (CHead c k0 t)) \to
41 (getl (S n) c1 c3)))) (\lambda (b: B).(\lambda (H3: (getl (S n) (CHead c
42 (Bind b) t) c3)).(\lambda (H4: (clear c1 (CHead c (Bind b) t))).(let H5 \def
43 (getl_gen_all c c3 (r (Bind b) n) (getl_gen_S (Bind b) c c3 t n H3)) in
44 (ex2_ind C (\lambda (e: C).(drop n O c e)) (\lambda (e: C).(clear e c3))
45 (getl (S n) c1 c3) (\lambda (x: C).(\lambda (H6: (drop n O c x)).(\lambda
46 (H7: (clear x c3)).(getl_intro (S n) c1 c3 x (drop_clear_O b c1 c t H4 x n
47 H6) H7)))) H5))))) (\lambda (f: F).(\lambda (_: (getl (S n) (CHead c (Flat f)
48 t) c3)).(\lambda (H4: (clear c1 (CHead c (Flat f) t))).(clear_gen_flat_r f c1
49 c t H4 (getl (S n) c1 c3))))) k H1 H2))))))))) c2)))) i).
54 theorem getl_clear_trans:
55 \forall (i: nat).(\forall (c1: C).(\forall (c2: C).((getl i c1 c2) \to
56 (\forall (c3: C).((clear c2 c3) \to (getl i c1 c3))))))
58 \lambda (i: nat).(\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (getl i c1
59 c2)).(\lambda (c3: C).(\lambda (H0: (clear c2 c3)).(let H1 \def (getl_gen_all
60 c1 c2 i H) in (ex2_ind C (\lambda (e: C).(drop i O c1 e)) (\lambda (e:
61 C).(clear e c2)) (getl i c1 c3) (\lambda (x: C).(\lambda (H2: (drop i O c1
62 x)).(\lambda (H3: (clear x c2)).(let H4 \def (clear_gen_all x c2 H3) in
63 (ex_3_ind B C T (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(eq C c2
64 (CHead e (Bind b) u))))) (getl i c1 c3) (\lambda (x0: B).(\lambda (x1:
65 C).(\lambda (x2: T).(\lambda (H5: (eq C c2 (CHead x1 (Bind x0) x2))).(let H6
66 \def (eq_ind C c2 (\lambda (c: C).(clear x c)) H3 (CHead x1 (Bind x0) x2) H5)
67 in (let H7 \def (eq_ind C c2 (\lambda (c: C).(clear c c3)) H0 (CHead x1 (Bind
68 x0) x2) H5) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c: C).(getl i c1
69 c)) (getl_intro i c1 (CHead x1 (Bind x0) x2) x H2 H6) c3 (clear_gen_bind x0
70 x1 c3 x2 H7)))))))) H4))))) H1))))))).
75 theorem getl_clear_bind:
76 \forall (b: B).(\forall (c: C).(\forall (e1: C).(\forall (v: T).((clear c
77 (CHead e1 (Bind b) v)) \to (\forall (e2: C).(\forall (n: nat).((getl n e1 e2)
78 \to (getl (S n) c e2))))))))
80 \lambda (b: B).(\lambda (c: C).(C_ind (\lambda (c0: C).(\forall (e1:
81 C).(\forall (v: T).((clear c0 (CHead e1 (Bind b) v)) \to (\forall (e2:
82 C).(\forall (n: nat).((getl n e1 e2) \to (getl (S n) c0 e2)))))))) (\lambda
83 (n: nat).(\lambda (e1: C).(\lambda (v: T).(\lambda (H: (clear (CSort n)
84 (CHead e1 (Bind b) v))).(\lambda (e2: C).(\lambda (n0: nat).(\lambda (_:
85 (getl n0 e1 e2)).(clear_gen_sort (CHead e1 (Bind b) v) n H (getl (S n0)
86 (CSort n) e2))))))))) (\lambda (c0: C).(\lambda (H: ((\forall (e1:
87 C).(\forall (v: T).((clear c0 (CHead e1 (Bind b) v)) \to (\forall (e2:
88 C).(\forall (n: nat).((getl n e1 e2) \to (getl (S n) c0 e2))))))))).(\lambda
89 (k: K).(\lambda (t: T).(\lambda (e1: C).(\lambda (v: T).(\lambda (H0: (clear
90 (CHead c0 k t) (CHead e1 (Bind b) v))).(\lambda (e2: C).(\lambda (n:
91 nat).(\lambda (H1: (getl n e1 e2)).(K_ind (\lambda (k0: K).((clear (CHead c0
92 k0 t) (CHead e1 (Bind b) v)) \to (getl (S n) (CHead c0 k0 t) e2))) (\lambda
93 (b0: B).(\lambda (H2: (clear (CHead c0 (Bind b0) t) (CHead e1 (Bind b)
94 v))).(let H3 \def (f_equal C C (\lambda (e: C).(match e in C return (\lambda
95 (_: C).C) with [(CSort _) \Rightarrow e1 | (CHead c1 _ _) \Rightarrow c1]))
96 (CHead e1 (Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1
97 (Bind b) v) t H2)) in ((let H4 \def (f_equal C B (\lambda (e: C).(match e in
98 C return (\lambda (_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k0 _)
99 \Rightarrow (match k0 in K return (\lambda (_: K).B) with [(Bind b1)
100 \Rightarrow b1 | (Flat _) \Rightarrow b])])) (CHead e1 (Bind b) v) (CHead c0
101 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b) v) t H2)) in ((let H5
102 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T)
103 with [(CSort _) \Rightarrow v | (CHead _ _ t0) \Rightarrow t0])) (CHead e1
104 (Bind b) v) (CHead c0 (Bind b0) t) (clear_gen_bind b0 c0 (CHead e1 (Bind b)
105 v) t H2)) in (\lambda (H6: (eq B b b0)).(\lambda (H7: (eq C e1 c0)).(let H8
106 \def (eq_ind C e1 (\lambda (c1: C).(getl n c1 e2)) H1 c0 H7) in (eq_ind B b
107 (\lambda (b1: B).(getl (S n) (CHead c0 (Bind b1) t) e2)) (getl_head (Bind b)
108 n c0 e2 H8 t) b0 H6))))) H4)) H3)))) (\lambda (f: F).(\lambda (H2: (clear
109 (CHead c0 (Flat f) t) (CHead e1 (Bind b) v))).(getl_flat c0 e2 (S n) (H e1 v
110 (clear_gen_flat f c0 (CHead e1 (Bind b) v) t H2) e2 n H1) f t))) k
116 theorem getl_clear_conf:
117 \forall (i: nat).(\forall (c1: C).(\forall (c3: C).((getl i c1 c3) \to
118 (\forall (c2: C).((clear c1 c2) \to (getl i c2 c3))))))
120 \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (c3:
121 C).((getl n c1 c3) \to (\forall (c2: C).((clear c1 c2) \to (getl n c2
122 c3))))))) (\lambda (c1: C).(\lambda (c3: C).(\lambda (H: (getl O c1
123 c3)).(\lambda (c2: C).(\lambda (H0: (clear c1 c2)).(eq_ind C c3 (\lambda (c:
124 C).(getl O c c3)) (let H1 \def (clear_gen_all c1 c3 (getl_gen_O c1 c3 H)) in
125 (ex_3_ind B C T (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(eq C c3
126 (CHead e (Bind b) u))))) (getl O c3 c3) (\lambda (x0: B).(\lambda (x1:
127 C).(\lambda (x2: T).(\lambda (H2: (eq C c3 (CHead x1 (Bind x0) x2))).(let H3
128 \def (eq_ind C c3 (\lambda (c: C).(clear c1 c)) (getl_gen_O c1 c3 H) (CHead
129 x1 (Bind x0) x2) H2) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c:
130 C).(getl O c c)) (getl_refl x0 x1 x2) c3 H2)))))) H1)) c2 (clear_mono c1 c3
131 (getl_gen_O c1 c3 H) c2 H0))))))) (\lambda (n: nat).(\lambda (_: ((\forall
132 (c1: C).(\forall (c3: C).((getl n c1 c3) \to (\forall (c2: C).((clear c1 c2)
133 \to (getl n c2 c3)))))))).(\lambda (c1: C).(C_ind (\lambda (c: C).(\forall
134 (c3: C).((getl (S n) c c3) \to (\forall (c2: C).((clear c c2) \to (getl (S n)
135 c2 c3)))))) (\lambda (n0: nat).(\lambda (c3: C).(\lambda (H0: (getl (S n)
136 (CSort n0) c3)).(\lambda (c2: C).(\lambda (_: (clear (CSort n0)
137 c2)).(getl_gen_sort n0 (S n) c3 H0 (getl (S n) c2 c3))))))) (\lambda (c:
138 C).(\lambda (H0: ((\forall (c3: C).((getl (S n) c c3) \to (\forall (c2:
139 C).((clear c c2) \to (getl (S n) c2 c3))))))).(\lambda (k: K).(\lambda (t:
140 T).(\lambda (c3: C).(\lambda (H1: (getl (S n) (CHead c k t) c3)).(\lambda
141 (c2: C).(\lambda (H2: (clear (CHead c k t) c2)).(K_ind (\lambda (k0:
142 K).((getl (S n) (CHead c k0 t) c3) \to ((clear (CHead c k0 t) c2) \to (getl
143 (S n) c2 c3)))) (\lambda (b: B).(\lambda (H3: (getl (S n) (CHead c (Bind b)
144 t) c3)).(\lambda (H4: (clear (CHead c (Bind b) t) c2)).(eq_ind_r C (CHead c
145 (Bind b) t) (\lambda (c0: C).(getl (S n) c0 c3)) (getl_head (Bind b) n c c3
146 (getl_gen_S (Bind b) c c3 t n H3) t) c2 (clear_gen_bind b c c2 t H4)))))
147 (\lambda (f: F).(\lambda (H3: (getl (S n) (CHead c (Flat f) t) c3)).(\lambda
148 (H4: (clear (CHead c (Flat f) t) c2)).(H0 c3 (getl_gen_S (Flat f) c c3 t n
149 H3) c2 (clear_gen_flat f c c2 t H4))))) k H1 H2))))))))) c1)))) i).