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/pc1/defs.ma".
19 include "Basic-1/pr1/pr1.ma".
22 \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (pc1 t1 t2)))
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)
32 \forall (t1: T).(\forall (t2: T).((pr0 t2 t1) \to (pc1 t1 t2)))
34 \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t2 t1)).(ex_intro2 T
35 (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t1 (pr1_refl t1)
42 \forall (t: T).(pc1 t t)
44 \lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr1 t t0)) (\lambda (t0:
45 T).(pr1 t t0)) t (pr1_refl t) (pr1_refl t)).
51 \forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3: T).((pc1 t2
52 t3) \to (pc1 t1 t3)))))
54 \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pr0 t1 t2)).(\lambda (t3:
55 T).(\lambda (H0: (pc1 t2 t3)).(let H1 \def H0 in (ex2_ind T (\lambda (t:
56 T).(pr1 t2 t)) (\lambda (t: T).(pr1 t3 t)) (pc1 t1 t3) (\lambda (x:
57 T).(\lambda (H2: (pr1 t2 x)).(\lambda (H3: (pr1 t3 x)).(ex_intro2 T (\lambda
58 (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x (pr1_sing t2 t1 H x H2)
65 \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (pc1 t2 t1)))
67 \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pc1 t1 t2)).(let H0 \def H in
68 (ex2_ind T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) (pc1 t2
69 t1) (\lambda (x: T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2
70 x)).(ex_intro2 T (\lambda (t: T).(pr1 t2 t)) (\lambda (t: T).(pr1 t1 t)) x H2
77 \forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t: T).(\forall
78 (k: K).(pc1 (THead k u1 t) (THead k u2 t))))))
80 \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pc1 u1 u2)).(\lambda (t:
81 T).(\lambda (k: K).(let H0 \def H in (ex2_ind T (\lambda (t0: T).(pr1 u1 t0))
82 (\lambda (t0: T).(pr1 u2 t0)) (pc1 (THead k u1 t) (THead k u2 t)) (\lambda
83 (x: T).(\lambda (H1: (pr1 u1 x)).(\lambda (H2: (pr1 u2 x)).(ex_intro2 T
84 (\lambda (t0: T).(pr1 (THead k u1 t) t0)) (\lambda (t0: T).(pr1 (THead k u2
85 t) t0)) (THead k x t) (pr1_head_1 u1 x H1 t k) (pr1_head_1 u2 x H2 t k)))))
92 \forall (t1: T).(\forall (t2: T).((pc1 t1 t2) \to (\forall (u: T).(\forall
93 (k: K).(pc1 (THead k u t1) (THead k u t2))))))
95 \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pc1 t1 t2)).(\lambda (u:
96 T).(\lambda (k: K).(let H0 \def H in (ex2_ind T (\lambda (t: T).(pr1 t1 t))
97 (\lambda (t: T).(pr1 t2 t)) (pc1 (THead k u t1) (THead k u t2)) (\lambda (x:
98 T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2 x)).(ex_intro2 T (\lambda
99 (t: T).(pr1 (THead k u t1) t)) (\lambda (t: T).(pr1 (THead k u t2) t)) (THead
100 k u x) (pr1_head_2 t1 x H1 u k) (pr1_head_2 t2 x H2 u k))))) H0)))))).
106 \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (\forall (t3: T).((pc1 t2
107 t3) \to (pc1 t1 t3)))))
109 \lambda (t2: T).(\lambda (t1: T).(\lambda (H: (pc1 t1 t2)).(\lambda (t3:
110 T).(\lambda (H0: (pc1 t2 t3)).(let H1 \def H0 in (ex2_ind T (\lambda (t:
111 T).(pr1 t2 t)) (\lambda (t: T).(pr1 t3 t)) (pc1 t1 t3) (\lambda (x:
112 T).(\lambda (H2: (pr1 t2 x)).(\lambda (H3: (pr1 t3 x)).(let H4 \def H in
113 (ex2_ind T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) (pc1 t1
114 t3) (\lambda (x0: T).(\lambda (H5: (pr1 t1 x0)).(\lambda (H6: (pr1 t2
115 x0)).(ex2_ind T (\lambda (t: T).(pr1 x0 t)) (\lambda (t: T).(pr1 x t)) (pc1
116 t1 t3) (\lambda (x1: T).(\lambda (H7: (pr1 x0 x1)).(\lambda (H8: (pr1 x
117 x1)).(ex_intro2 T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x1
118 (pr1_t x0 t1 H5 x1 H7) (pr1_t x t3 H3 x1 H8))))) (pr1_confluence t2 x0 H6 x
119 H2))))) H4))))) H1)))))).
125 \forall (t0: T).(\forall (t1: T).((pr0 t0 t1) \to (\forall (t2: T).((pc1 t0
126 t2) \to (pc1 t1 t2)))))
128 \lambda (t0: T).(\lambda (t1: T).(\lambda (H: (pr0 t0 t1)).(\lambda (t2:
129 T).(\lambda (H0: (pc1 t0 t2)).(pc1_t t0 t1 (pc1_pr0_x t1 t0 H) t2 H0))))).
135 \forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t1: T).(\forall
136 (t2: T).((pc1 t1 t2) \to (\forall (k: K).(pc1 (THead k u1 t1) (THead k u2
139 \lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pc1 u1 u2)).(\lambda (t1:
140 T).(\lambda (t2: T).(\lambda (H0: (pc1 t1 t2)).(\lambda (k: K).(pc1_t (THead
141 k u2 t1) (THead k u1 t1) (pc1_head_1 u1 u2 H t1 k) (THead k u2 t2)
142 (pc1_head_2 t1 t2 H0 u2 k)))))))).