- Theorem pc3_t : (t2,c,t1:?) (pc3 c t1 t2) ->
- (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
- Intros t2 c t1 H; XElim H; XEAuto.
- Qed.
-
- Hints Resolve pc3_t : ltlc.
-
- Theorem pc3_s : (c,t2,t1:?) (pc3 c t1 t2) -> (pc3 c t2 t1).
- Intros; XElim H; [ XAuto | XEAuto ].
- Qed.
-
- Hints Resolve pc3_s : ltlc.
-
- Theorem pc3_pr3_r : (c:?; t1,t2) (pr3 c t1 t2) -> (pc3 c t1 t2).
- Intros; XElim H; XEAuto.
- Qed.
-
- Theorem pc3_pr3_x : (c:?; t1,t2) (pr3 c t2 t1) -> (pc3 c t1 t2).
- Intros; XElim H; XEAuto.
- Qed.
-
- Hints Resolve pc3_pr3_r pc3_pr3_x : ltlc.
-
- Theorem pc3_pr3_t : (c:?; t1,t0:?) (pr3 c t1 t0) ->
- (t2:?) (pr3 c t2 t0) -> (pc3 c t1 t2).
- Intros; Apply (pc3_t t0); XAuto.