(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/pr0/fwd.ma".
+include "Basic-1/pr0/fwd.ma".
-include "LambdaDelta-1/lift/tlt.ma".
+include "Basic-1/lift/tlt.ma".
theorem pr0_confluence__pr0_cong_upsilon_refl:
\forall (b: B).((not (eq B b Abst)) \to (\forall (u0: T).(\forall (u3:
(THead (Flat Appl) (lift (S O) O x) t5) (pr0_comp (lift (S O) O v2) (lift (S
O) O x) (pr0_lift v2 x H3 (S O) O) t5 t5 (pr0_refl t5) (Flat Appl)) (Bind
b))))))))))))))).
+(* COMMENTS
+Initial nodes: 257
+END *)
theorem pr0_confluence__pr0_cong_upsilon_cong:
\forall (b: B).((not (eq B b Abst)) \to (\forall (u2: T).(\forall (v2:
Appl) (lift (S O) O v2) t5) (THead (Flat Appl) (lift (S O) O x) x0) (pr0_comp
(lift (S O) O v2) (lift (S O) O x) (pr0_lift v2 x H1 (S O) O) t5 x0 H3 (Flat
Appl)) (Bind b))))))))))))))))))).
+(* COMMENTS
+Initial nodes: 269
+END *)
theorem pr0_confluence__pr0_cong_upsilon_delta:
(not (eq B Abbr Abst)) \to (\forall (u5: T).(\forall (t2: T).(\forall (w:
(THead (Flat Appl) (lift (S O) O x) x2) (subst0_snd (Flat Appl) x1 x2 x0 O H9
(lift (S O) O x))))))) H7)) (pr0_subst0 t2 x0 H3 u5 w O H0 x1
H5))))))))))))))))))).
+(* COMMENTS
+Initial nodes: 769
+END *)
theorem pr0_confluence__pr0_cong_upsilon_zeta:
\forall (b: B).((not (eq B b Abst)) \to (\forall (u0: T).(\forall (u3:
Appl) x0 x1) (pr0_comp v2 x0 H2 x x1 H3 (Flat Appl)) u3)) (THead (Flat Appl)
(lift (S O) O v2) (lift (S O) O x)) (lift_flat Appl v2 x (S O)
O)))))))))))))))).
+(* COMMENTS
+Initial nodes: 283
+END *)
theorem pr0_confluence__pr0_cong_delta:
\forall (u3: T).(\forall (t5: T).(\forall (w: T).((subst0 O u3 t5 w) \to
(t: T).(pr0 (THead (Bind Abbr) u3 w) t)) (THead (Bind Abbr) x x1) (pr0_delta
u2 x H0 t3 x0 H2 x1 H6) (pr0_comp u3 x H1 w x1 H5 (Bind Abbr)))))) H4))
(pr0_subst0 t5 x0 H3 u3 w O H x H1))))))))))))).
+(* COMMENTS
+Initial nodes: 409
+END *)
theorem pr0_confluence__pr0_upsilon_upsilon:
\forall (b: B).((not (eq B b Abst)) \to (\forall (v1: T).(\forall (v2:
H3 (THead (Flat Appl) (lift (S O) O v2) t2) (THead (Flat Appl) (lift (S O) O
x0) x2) (pr0_comp (lift (S O) O v2) (lift (S O) O x0) (pr0_lift v2 x0 H1 (S
O) O) t2 x2 H5 (Flat Appl)) (Bind b))))))))))))))))))).
+(* COMMENTS
+Initial nodes: 347
+END *)
theorem pr0_confluence__pr0_delta_delta:
\forall (u2: T).(\forall (t3: T).(\forall (w: T).((subst0 O u2 t3 w) \to
(Bind Abbr)) (pr0_delta u3 x H2 w0 x1 H6 x2 H11))) (subst0_confluence_eq x0
x2 x O H10 x1 H7))))) H8)) (pr0_subst0 t3 x0 H3 u2 w O H x H1))))) H5))
(pr0_subst0 t5 x0 H4 u3 w0 O H0 x H2))))))))))))))).
+(* COMMENTS
+Initial nodes: 1501
+END *)
theorem pr0_confluence__pr0_delta_tau:
\forall (u2: T).(\forall (t3: T).(\forall (w: T).((subst0 O u2 t3 w) \to
(le_n (plus (S O) O)) (plus O (S O)) (plus_sym O (S O))) H3 (ex2 T (\lambda
(t: T).(pr0 (THead (Bind Abbr) u2 w) t)) (\lambda (t: T).(pr0 t2 t))))))))
(pr0_gen_lift t4 t3 (S O) O H0)))))))).
+(* COMMENTS
+Initial nodes: 257
+END *)
theorem pr0_confluence:
\forall (t0: T).(\forall (t1: T).((pr0 t0 t1) \to (\forall (t2: T).((pr0 t0
H13)))) t6 (sym_eq T t6 t2 H10))) t H8 H9 H7)))]) in (H7 (refl_equal T t)
(refl_equal T t2)))) t4 (sym_eq T t4 t1 H5))) t H3 H4 H2)))]) in (H2
(refl_equal T t) (refl_equal T t1))))))))) t0).
+(* COMMENTS
+Initial nodes: 46103
+END *)