-(*#* #stop file *)
-
Require Export contexts_defs.
Require Export subst0_defs.
Require Export drop_defs.
+(*#* #caption "axioms for strict substitution in contexts",
+ "substituted tail item: second operand",
+ "substituted tail item: first operand",
+ "substituted tail item: both operands"
+*)
+(*#* #cap #cap c, c1, c2 #alpha v in W, u in V, u1 in V1, u2 in V2, k in z, r in q *)
+
Inductive csubst0 : nat -> T -> C -> C -> Prop :=
- | csubst0_fst : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) -> (c:?)
- (csubst0 (S i) v (CTail c k u) (CTail c k w))
- | csubst0_snd : (k:?; i:?; c1,c2:?; v:?) (csubst0 (r k i) v c1 c2) ->
+ | csubst0_snd : (k:?; i:?; v,u1,u2:?) (subst0 (r k i) v u1 u2) -> (c:?)
+ (csubst0 (S i) v (CTail c k u1) (CTail c k u2))
+ | csubst0_fst : (k:?; i:?; c1,c2:?; v:?) (csubst0 (r k i) v c1 c2) ->
(u:?) (csubst0 (S i) v (CTail c1 k u) (CTail c2 k u))
- | csubst0_both : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) ->
+ | csubst0_both : (k:?; i:?; v,u1,u2:?) (subst0 (r k i) v u1 u2) ->
(c1,c2:?) (csubst0 (r k i) v c1 c2) ->
- (csubst0 (S i) v (CTail c1 k u) (CTail c2 k w)).
+ (csubst0 (S i) v (CTail c1 k u1) (CTail c2 k u2)).
- Hint csubst0 : ltlc := Constructors csubst0.
-
- Inductive fsubst0 [i:nat; v:T; c1:C; t1:T] : C -> T -> Prop :=
- | fsubst0_t : (t2:?) (subst0 i v t1 t2) -> (fsubst0 i v c1 t1 c1 t2)
- | fsubst0_c : (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t1)
- | fsubst0_b : (t2:?) (subst0 i v t1 t2) ->
- (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t2).
+(*#* #stop file *)
- Hint fsubst0 : ltlc := Constructors fsubst0.
+ Hint csubst0 : ltlc := Constructors csubst0.
Section csubst0_gen_base. (***********************************************)
)).
Intros until 1; InsertEq H '(S i); InsertEq H '(CTail c1 k u1).
XCase H; Clear x v y y0; Intros; Inversion H1.
-(* case 1: csubst0_fst *)
+(* case 1: csubst0_snd *)
Inversion H0; Rewrite H3 in H; Rewrite H5 in H; Rewrite H6 in H; XEAuto.
-(* case 2: csubst0_snd *)
+(* case 2: csubst0_fst *)
Inversion H0; Rewrite H3 in H; Rewrite H4 in H; Rewrite H5 in H; XEAuto.
(* case 2: csubst0_both *)
Inversion H2; Rewrite H5 in H; Rewrite H6 in H; Rewrite H7 in H;
(* case 2.2: n > 0 *)
Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros.
DropGenBase.
-(* case 2.2.1: csubst0_fst *)
+(* case 2.2.1: csubst0_snd *)
XAuto.
-(* case 2.2.2: csubst0_snd *)
+(* case 2.2.2: csubst0_fst *)
XReplaceIn H0 i0 i; DropGenBase; NewInduction k; XEAuto.
(* case 2.2.3: csubst0_both *)
XReplaceIn H0 i0 i; XReplaceIn H2 i0 i.
(* case 2.2: n > 0 *)
Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Clear c1 c2 v y;
Intros; DropGenBase.
-(* case 2.2.1: csubst0_fst *)
+(* case 2.2.1: csubst0_snd *)
XEAuto.
-(* case 2.2.2: csubst0_snd *)
+(* case 2.2.2: csubst0_fst *)
Replace i0 with i; XAuto; XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; Clear H3 i0.
Apply (r_dis k); Intros; Rewrite (H3 i) in H0; Rewrite (H3 n) in H4.
(* case 2.2.2.1: bind *)
(* case 2.2 : n > 0 *)
Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros;
DropGenBase.
-(* case 2.2.1 : csubst0_fst *)
+(* case 2.2.1 : csubst0_snd *)
XAuto.
-(* case 2.2.2 : csubst0_snd *)
+(* case 2.2.2 : csubst0_fst *)
XReplaceIn H0 i0 i; NewInduction k; XEAuto.
(* case 2.2.3 : csubst0_both *)
XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; NewInduction k; XEAuto.