9 Section pc3_gen. (********************************************************)
11 Theorem pc3_gen_abst : (c:?; u1,u2,t1,t2:?)
12 (pc3 c (TTail (Bind Abst) u1 t1)
13 (TTail (Bind Abst) u2 t2)
16 (b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2).
18 Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H0 in H; Clear H0 x.
19 Inversion H; Rewrite H5 in H1; Rewrite H6 in H2.
23 Theorem pc3_gen_lift: (c:?; t1,t2:?; h,d:?)
24 (pc3 c (lift h d t1) (lift h d t2)) ->
25 (e:?) (drop h d c e) ->
28 Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H1 in H; Clear H1 x.
29 LiftGen; Rewrite H in H2; XEAuto.
32 Theorem pc3_gen_not_abst : (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
33 (pc3 c (TTail (Bind b) u1 t1)
34 (TTail (Bind Abst) u2 t2)
36 (pc3 (CTail c (Bind b) u1) t1
37 (lift (1) (0) (TTail (Bind Abst) u2 t2))
40 Intros b; XElim b; Intros;
41 Try EqFalse; Pc3Confluence; Pr3Gen; Pr3Gen;
42 Try (Rewrite H1 in H0; Inversion H0);
43 Rewrite H1 in H4; Pr3Context;
44 EApply pc3_pr3_t; XEAuto.
47 Theorem pc3_gen_lift_abst : (c:?; t,t2,u2:?; h,d:?)
49 (TTail (Bind Abst) u2 t2)
51 (e:?) (drop h d c e) ->
52 (EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) &
53 (pr3 c u2 (lift h d u1)) &
54 (b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1))
57 Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H1 in H; Clear H1 x.
58 LiftGenBase; Rewrite H in H4; Rewrite H1 in H2; Rewrite H5 in H3; XEAuto.
63 Tactic Definition Pc3Gen :=
65 | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (lift ?2 ?3 ?5));
66 _: (drop ?2 ?3 ?1 ?6) |- ? ] ->
67 LApply (pc3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Intros H_x | XAuto ];
68 LApply (H_x ?6); [ Clear H_x; Intros | XAuto ]
69 | [ H: (pc3 ?1 (TTail (Bind Abst) ?2 ?3) (TTail (Bind Abst) ?4 ?5)) |- ? ] ->
70 LApply (pc3_gen_abst ?1 ?2 ?4 ?3 ?5);[ Clear H; Intros H | XAuto ];
72 | [ H: (pc3 ?1 (TTail (Bind ?2) ?3 ?4) (TTail (Bind Abst) ?5 ?6));
73 _: ~ ?2 = Abst |- ? ] ->
74 LApply (pc3_gen_not_abst ?2); [ Intros H_x | XAuto ];
75 LApply (H_x ?1 ?4 ?6 ?3 ?5); [ Clear H H_x; Intros | XAuto ]
76 | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (TTail (Bind Abst) ?5 ?6));
77 _: (drop ?2 ?3 ?1 ?7) |- ? ] ->
78 LApply (pc3_gen_lift_abst ?1 ?4 ?6 ?5 ?2 ?3); [ Intros H_x | XAuto ];
79 LApply (H_x ?7); [ Clear H_x; Intros H_x | XAuto ];