Section pr3_confluence. (*************************************************)
+(*#* #stop theorem *)
+
(*#* #caption "confluence with single step reduction: strip lemma" *)
(*#* #cap #cap c, t0, t1, t2, t *)
Theorem pr3_strip : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) ->
(EX t | (pr3 c t1 t) & (pr3 c t2 t)).
-
-(*#* #stop proof *)
-
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
XEAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
Pr2Confluence.
LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
XElim H1; Intros; XEAuto.
Qed.
-(*#* #start proof *)
+(*#* #start theorem *)
(*#* #caption "confluence with itself: Church-Rosser property" *)
(*#* #cap #cap c, t0, t1, t2, t *)
(*#* #stop file *)
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
XEAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
LApply (pr3_strip c t3 t5); [ Clear H2; Intros H2 | XAuto ].
LApply (H2 t2); [ Clear H H2; Intros H | XAuto ].
XElim H; Intros.