]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_1A/pc1/props.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / basic_1A / pc1 / 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 include "basic_1A/pc1/defs.ma".
18
19 include "basic_1A/pr1/pr1.ma".
20
21 lemma pc1_pr0_r:
22  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (pc1 t1 t2)))
23 \def
24  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(ex_intro2 T 
25 (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t2 (pr1_pr0 t1 t2 H) 
26 (pr1_refl t2)))).
27
28 lemma pc1_pr0_x:
29  \forall (t1: T).(\forall (t2: T).((pr0 t2 t1) \to (pc1 t1 t2)))
30 \def
31  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t2 t1)).(ex_intro2 T 
32 (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t1 (pr1_refl t1) 
33 (pr1_pr0 t2 t1 H)))).
34
35 lemma pc1_refl:
36  \forall (t: T).(pc1 t t)
37 \def
38  \lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr1 t t0)) (\lambda (t0: 
39 T).(pr1 t t0)) t (pr1_refl t) (pr1_refl t)).
40
41 lemma pc1_pr0_u:
42  \forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3: T).((pc1 t2 
43 t3) \to (pc1 t1 t3)))))
44 \def
45  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pr0 t1 t2)).(\lambda (t3: 
46 T).(\lambda (H0: (pc1 t2 t3)).(let H1 \def H0 in (ex2_ind T (\lambda (t: 
47 T).(pr1 t2 t)) (\lambda (t: T).(pr1 t3 t)) (pc1 t1 t3) (\lambda (x: 
48 T).(\lambda (H2: (pr1 t2 x)).(\lambda (H3: (pr1 t3 x)).(ex_intro2 T (\lambda 
49 (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x (pr1_sing t2 t1 H x H2) 
50 H3)))) H1)))))).
51
52 lemma pc1_s:
53  \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (pc1 t2 t1)))
54 \def
55  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pc1 t1 t2)).(let H0 \def H in 
56 (ex2_ind T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) (pc1 t2 
57 t1) (\lambda (x: T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2 
58 x)).(ex_intro2 T (\lambda (t: T).(pr1 t2 t)) (\lambda (t: T).(pr1 t1 t)) x H2 
59 H1)))) H0)))).
60
61 lemma pc1_head_1:
62  \forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t: T).(\forall 
63 (k: K).(pc1 (THead k u1 t) (THead k u2 t))))))
64 \def
65  \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pc1 u1 u2)).(\lambda (t: 
66 T).(\lambda (k: K).(let H0 \def H in (ex2_ind T (\lambda (t0: T).(pr1 u1 t0)) 
67 (\lambda (t0: T).(pr1 u2 t0)) (pc1 (THead k u1 t) (THead k u2 t)) (\lambda 
68 (x: T).(\lambda (H1: (pr1 u1 x)).(\lambda (H2: (pr1 u2 x)).(ex_intro2 T 
69 (\lambda (t0: T).(pr1 (THead k u1 t) t0)) (\lambda (t0: T).(pr1 (THead k u2 
70 t) t0)) (THead k x t) (pr1_head_1 u1 x H1 t k) (pr1_head_1 u2 x H2 t k))))) 
71 H0)))))).
72
73 lemma pc1_head_2:
74  \forall (t1: T).(\forall (t2: T).((pc1 t1 t2) \to (\forall (u: T).(\forall 
75 (k: K).(pc1 (THead k u t1) (THead k u t2))))))
76 \def
77  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pc1 t1 t2)).(\lambda (u: 
78 T).(\lambda (k: K).(let H0 \def H in (ex2_ind T (\lambda (t: T).(pr1 t1 t)) 
79 (\lambda (t: T).(pr1 t2 t)) (pc1 (THead k u t1) (THead k u t2)) (\lambda (x: 
80 T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2 x)).(ex_intro2 T (\lambda 
81 (t: T).(pr1 (THead k u t1) t)) (\lambda (t: T).(pr1 (THead k u t2) t)) (THead 
82 k u x) (pr1_head_2 t1 x H1 u k) (pr1_head_2 t2 x H2 u k))))) H0)))))).
83
84 theorem pc1_t:
85  \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (\forall (t3: T).((pc1 t2 
86 t3) \to (pc1 t1 t3)))))
87 \def
88  \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pc1 t1 t2)).(\lambda (t3: 
89 T).(\lambda (H0: (pc1 t2 t3)).(let H1 \def H0 in (ex2_ind T (\lambda (t: 
90 T).(pr1 t2 t)) (\lambda (t: T).(pr1 t3 t)) (pc1 t1 t3) (\lambda (x: 
91 T).(\lambda (H2: (pr1 t2 x)).(\lambda (H3: (pr1 t3 x)).(let H4 \def H in 
92 (ex2_ind T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) (pc1 t1 
93 t3) (\lambda (x0: T).(\lambda (H5: (pr1 t1 x0)).(\lambda (H6: (pr1 t2 
94 x0)).(ex2_ind T (\lambda (t: T).(pr1 x0 t)) (\lambda (t: T).(pr1 x t)) (pc1 
95 t1 t3) (\lambda (x1: T).(\lambda (H7: (pr1 x0 x1)).(\lambda (H8: (pr1 x 
96 x1)).(ex_intro2 T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x1 
97 (pr1_t x0 t1 H5 x1 H7) (pr1_t x t3 H3 x1 H8))))) (pr1_confluence t2 x0 H6 x 
98 H2))))) H4))))) H1)))))).
99
100 lemma pc1_pr0_u2:
101  \forall (t0: T).(\forall (t1: T).((pr0 t0 t1) \to (\forall (t2: T).((pc1 t0 
102 t2) \to (pc1 t1 t2)))))
103 \def
104  \lambda (t0: T).(\lambda (t1: T).(\lambda (H: (pr0 t0 t1)).(\lambda (t2: 
105 T).(\lambda (H0: (pc1 t0 t2)).(pc1_t t0 t1 (pc1_pr0_x t1 t0 H) t2 H0))))).
106
107 theorem pc1_head:
108  \forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t1: T).(\forall 
109 (t2: T).((pc1 t1 t2) \to (\forall (k: K).(pc1 (THead k u1 t1) (THead k u2 
110 t2))))))))
111 \def
112  \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pc1 u1 u2)).(\lambda (t1: 
113 T).(\lambda (t2: T).(\lambda (H0: (pc1 t1 t2)).(\lambda (k: K).(pc1_t (THead 
114 k u2 t1) (THead k u1 t1) (pc1_head_1 u1 u2 H t1 k) (THead k u2 t2) 
115 (pc1_head_2 t1 t2 H0 u2 k)))))))).
116