8 Section pc3_fsubst0. (****************************************************)
10 Theorem pc3_pr2_fsubst0: (c1:?; t1,t:?) (pr2 c1 t1 t) ->
11 (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
12 (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
14 Intros until 1; XElim H.
15 (* case 1: pr2_free *)
16 Intros until 2; XElim H0; Intros.
17 (* case 1.1: fsubst0_snd *)
18 Pr0Subst0; [ XAuto | Apply (pc3_pr3_u c1 x); XEAuto ].
19 (* case 1.2: fsubst0_fst *)
21 (* case 1.3: fsubst0_both *)
22 Pr0Subst0; CSubst0Drop; [ XAuto | Apply (pc3_pr3_u c0 x); XEAuto ].
23 (* case 2 : pr2_delta *)
24 Intros until 4; XElim H2; Intros.
25 (* case 2.1: fsubst0_snd. *)
26 Apply (pc3_t t1); [ Apply pc3_s; XEAuto | XEAuto ].
27 (* case 2.2: fsubst0_fst. *)
28 Apply (lt_le_e i i0); Intros; CSubst0Drop.
29 (* case 2.2.1: i < i0, none *)
31 (* case 2.2.2: i < i0, csubst0_snd *)
32 CGenBase; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H8 H9 H10 c2 t3 x0 x1 x2.
33 Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
34 Apply (pc3_pr3_u c0 x); XEAuto.
35 (* case 2.2.3: i < i0, csubst0_fst *)
36 CGenBase; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H8 H9 H10 c2 t3 x0 x1 x3.
37 Apply pc3_pr2_r; XEAuto.
38 (* case 2.2.4: i < i0, csubst0_both *)
39 CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
40 Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
41 Apply (pc3_pr3_u c0 x); XEAuto.
42 (* case 2.2.5: i >= i0 *)
44 (* case 2.3: fsubst0_both *)
45 Apply (lt_le_e i i0); Intros; CSubst0Drop.
46 (* case 2.3.1 : i < i0, none *)
47 CSubst0Drop; Apply pc3_pr3_u2 with t0 := t1; XEAuto.
48 (* case 2.3.2 : i < i0, csubst0_snd *)
49 CGenBase; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H7; Clear H9 H10 H11 c2 t3 x0 x1 x2.
50 Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
51 Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
52 (* case 2.3.3: i < i0, csubst0_fst *)
53 CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
54 CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
55 (* case 2.3.4: i < i0, csubst0_both *)
56 CGenBase; Rewrite <- H10 in H8; Rewrite <- H11 in H6; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Clear H10 H11 H12 c2 t3 x0 x1 x3.
57 Subst0Subst0; Rewrite <- lt_plus_minus_r in H9; [ CSubst0Drop | XAuto ].
58 Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
59 (* case 2.3.5: i >= i0 *)
60 CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); XEAuto.
63 Theorem pc3_pr2_fsubst0_back: (c1:?; t,t1:?) (pr2 c1 t t1) ->
64 (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
65 (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
67 Intros until 1; XElim H.
68 (* case 1: pr2_free *)
69 Intros until 2; XElim H0; Intros.
70 (* case 1.1: fsubst0_snd. *)
71 Apply (pc3_pr3_u c1 t2); XEAuto.
72 (* case 1.2: fsubst0_fst. *)
74 (* case 1.3: fsubst0_both. *)
75 CSubst0Drop; Apply (pc3_pr3_u c0 t2); XEAuto.
76 (* case 2: pr2_delta *)
77 Intros until 4; XElim H2; Intros.
78 (* case 2.1: fsubst0_snd. *)
79 Apply (pc3_t t2); Apply pc3_pr3_r; XEAuto.
80 (* case 2.2: fsubst0_fst. *)
81 Apply (lt_le_e i i0); Intros; CSubst0Drop.
82 (* case 2.2.1: i < i0, none *)
84 (* case 2.2.2: i < i0, csubst0_bind *)
85 CGenBase; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H8 H9 H10 c2 t3 x0 x1 x2.
86 Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
87 Apply (pc3_pr3_u c0 x); XEAuto.
88 (* case 2.2.3: i < i0, csubst0_fst *)
89 CGenBase; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H8 H9 H10 c2 t3 x0 x1 x3.
90 Apply pc3_pr2_r; XEAuto.
91 (* case 2.2.4: i < i0, csubst0_both *)
92 CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
93 Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
94 Apply (pc3_pr3_u c0 x); XEAuto.
95 (* case 2.2.5: i >= i0 *)
97 (* case 2.3: fsubst0_both *)
98 Apply (lt_le_e i i0); Intros; CSubst0Drop.
99 (* case 2.3.1 : i < i0, none *)
100 CSubst0Drop; Apply pc3_pr3_u with t2:=t2; Try Apply pc3_pr3_r; XEAuto.
101 (* case 2.3.2 : i < i0, csubst0_snd *)
102 CGenBase; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H7; Clear H9 H10 H11 c2 t3 x0 x1 x2.
103 Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
104 Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t0) ]; XEAuto.
105 (* case 2.3.3: i < i0, csubst0_fst *)
106 CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
107 CSubst0Drop; Apply (pc3_pr3_u c0 t0); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
108 (* case 2.3.4: i < i0, csubst0_both *)
109 CGenBase; Rewrite <- H10 in H8; Rewrite <- H11 in H6; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Clear H10 H11 H12 c2 t3 x0 x1 x3.
110 Subst0Subst0; Rewrite <- lt_plus_minus_r in H9; [ CSubst0Drop | XAuto ].
111 Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t0) ]; XEAuto.
112 (* case 2.3.5: i >= i0 *)
113 CSubst0Drop; Apply (pc3_pr3_u c0 t0); XEAuto.
116 Theorem pc3_pc2_fsubst0: (c1:?; t1,t:?) (pc2 c1 t1 t) ->
117 (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
118 (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
120 Intros until 1; XElim H; Intros.
122 EApply pc3_pr2_fsubst0; XEAuto.
124 Apply pc3_s; EApply pc3_pr2_fsubst0_back; XEAuto.
127 Theorem pc3_fsubst0: (c1:?; t1,t:?) (pc3 c1 t1 t) ->
128 (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
129 (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
131 Intros until 1; XElim H.
133 Intros until 1; XElim H; Intros; Try CSubst0Drop; XEAuto.
135 Intros until 4; XElim H2; Intros;
136 (Apply (pc3_t t2); [ EApply pc3_pc2_fsubst0; XEAuto | XEAuto ]).
141 Hints Resolve pc3_fsubst0.