Welcome to Abella 2.0.5-dev
Abella < Specification "trans".
Reading specification "/home/fac05/gopalan/test/sparrow/compiler-correctness/website/wang-phd-thesis/code/./trans" (from "/home/fac05/gopalan/test/sparrow/compiler-correctness/website/wang-phd-thesis/code/.")
Abella < Import "typing".
Importing from /home/fac05/gopalan/test/sparrow/compiler-correctness/website/wang-phd-thesis/code/./typing
Abella < Define subst : (list (map tm tm)) -> prop by
subst nil;
nabla x, subst (map x V :: ML) := subst ML /\ {val V} /\ {tm V}.
Abella < Define vars_of_subst : (list (map tm tm)) -> (list tm) -> prop by
vars_of_subst nil nil;
nabla x, vars_of_subst (map x V :: ML) (x :: L) := vars_of_subst ML L.
Abella < Theorem subst_mem :
forall ML E, subst ML -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val V} /\ {tm V}).
============================
forall ML E, subst ML -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val V} /\ {tm V})
subst_mem < induction on 1.
IH : forall ML E, subst ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val V} /\ {tm V})
============================
forall ML E, subst ML @ -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val V} /\ {tm V})
subst_mem < intros.
Variables: ML E
IH : forall ML E, subst ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val V} /\ {tm V})
H1 : subst ML @
H2 : member E ML
============================
exists X V, E = map X V /\ name X /\ {val V} /\ {tm V}
subst_mem < case H1.
Subgoal 1:
Variables: E
IH : forall ML E, subst ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val V} /\ {tm V})
H2 : member E nil
============================
exists X V, E = map X V /\ name X /\ {val V} /\ {tm V}
Subgoal 2 is:
exists X V, E n1 = map X V /\ name X /\ {val V} /\ {tm V}
subst_mem < case H2.
Subgoal 2:
Variables: E ML1 V
IH : forall ML E, subst ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val V} /\ {tm V})
H2 : member (E n1) (map n1 V :: ML1)
H3 : subst ML1 *
H4 : {val V}
H5 : {tm V}
============================
exists X V, E n1 = map X V /\ name X /\ {val V} /\ {tm V}
subst_mem < case H2.
Subgoal 2.1:
Variables: ML1 V
IH : forall ML E, subst ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val V} /\ {tm V})
H3 : subst ML1 *
H4 : {val V}
H5 : {tm V}
============================
exists X V1, map n1 V = map X V1 /\ name X /\ {val V1} /\ {tm V1}
Subgoal 2.2 is:
exists X V, E n1 = map X V /\ name X /\ {val V} /\ {tm V}
subst_mem < search.
Subgoal 2.2:
Variables: E ML1 V
IH : forall ML E, subst ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val V} /\ {tm V})
H3 : subst ML1 *
H4 : {val V}
H5 : {tm V}
H6 : member (E n1) ML1
============================
exists X V, E n1 = map X V /\ name X /\ {val V} /\ {tm V}
subst_mem < backchain IH.
Proof completed.
Abella < Theorem subst_extend :
forall ML V, nabla x, subst ML -> {tm V} -> {val V} -> subst (map x V :: ML).
============================
forall ML V, nabla x, subst ML -> {tm V} -> {val V} -> subst (map x V :: ML)
subst_extend < intros.
Variables: ML V
H1 : subst ML
H2 : {tm V}
H3 : {val V}
============================
subst (map n1 V :: ML)
subst_extend < unfold.
Subgoal 1:
Variables: ML V
H1 : subst ML
H2 : {tm V}
H3 : {val V}
============================
subst ML
Subgoal 2 is:
{val V}
Subgoal 3 is:
{tm V}
subst_extend < search.
Subgoal 2:
Variables: ML V
H1 : subst ML
H2 : {tm V}
H3 : {val V}
============================
{val V}
Subgoal 3 is:
{tm V}
subst_extend < search.
Subgoal 3:
Variables: ML V
H1 : subst ML
H2 : {tm V}
H3 : {val V}
============================
{tm V}
subst_extend < search.
Proof completed.
Abella < Theorem app_subst_exists :
forall ML M, subst ML -> (exists M', app_subst ML M M').
============================
forall ML M, subst ML -> (exists M', app_subst ML M M')
app_subst_exists < induction on 1.
IH : forall ML M, subst ML * -> (exists M', app_subst ML M M')
============================
forall ML M, subst ML @ -> (exists M', app_subst ML M M')
app_subst_exists < intros.
Variables: ML M
IH : forall ML M, subst ML * -> (exists M', app_subst ML M M')
H1 : subst ML @
============================
exists M', app_subst ML M M'
app_subst_exists < case H1.
Subgoal 1:
Variables: M
IH : forall ML M, subst ML * -> (exists M', app_subst ML M M')
============================
exists M', app_subst nil M M'
Subgoal 2 is:
exists M', app_subst (map n1 V :: ML1) (M n1) M'
app_subst_exists < search.
Subgoal 2:
Variables: M ML1 V
IH : forall ML M, subst ML * -> (exists M', app_subst ML M M')
H2 : subst ML1 *
H3 : {val V}
H4 : {tm V}
============================
exists M', app_subst (map n1 V :: ML1) (M n1) M'
app_subst_exists < apply IH to H2 with M = M V.
Subgoal 2:
Variables: M ML1 V M'
IH : forall ML M, subst ML * -> (exists M', app_subst ML M M')
H2 : subst ML1 *
H3 : {val V}
H4 : {tm V}
H5 : app_subst ML1 (M V) M'
============================
exists M', app_subst (map n1 V :: ML1) (M n1) M'
app_subst_exists < search.
Proof completed.
Abella < Theorem subst_closed_tm_eq :
forall M ML M', {tm M} -> app_subst ML M M' -> M = M'.
============================
forall M ML M', {tm M} -> app_subst ML M M' -> M = M'
subst_closed_tm_eq < induction on 2.
IH : forall M ML M', {tm M} -> app_subst ML M M' * -> M = M'
============================
forall M ML M', {tm M} -> app_subst ML M M' @ -> M = M'
subst_closed_tm_eq < intros.
Variables: M ML M'
IH : forall M ML M', {tm M} -> app_subst ML M M' * -> M = M'
H1 : {tm M}
H2 : app_subst ML M M' @
============================
M = M'
subst_closed_tm_eq < case H2.
Subgoal 1:
Variables: M'
IH : forall M ML M', {tm M} -> app_subst ML M M' * -> M = M'
H1 : {tm M'}
============================
M' = M'
Subgoal 2 is:
M n1 = M1
subst_closed_tm_eq < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall M ML M', {tm M} -> app_subst ML M M' * -> M = M'
H1 : {tm (M n1)}
H3 : app_subst ML1 (M V) M1 *
============================
M n1 = M1
subst_closed_tm_eq < apply sclosed_tm_prune to H1.
Subgoal 2:
Variables: M1 ML1 V M'1
IH : forall M ML M', {tm M} -> app_subst ML M M' * -> M = M'
H1 : {tm M'1}
H3 : app_subst ML1 M'1 M1 *
============================
M'1 = M1
subst_closed_tm_eq < apply IH to _ H3.
Subgoal 2:
Variables: M1 ML1 V
IH : forall M ML M', {tm M} -> app_subst ML M M' * -> M = M'
H1 : {tm M1}
H3 : app_subst ML1 M1 M1 *
============================
M1 = M1
subst_closed_tm_eq < search.
Proof completed.
Abella < Theorem subst_inst :
forall ML M M' V, nabla x, {tm V} -> app_subst ML (M x) (M' x) ->
app_subst ML (M V) (M' V).
============================
forall ML M M' V, nabla x, {tm V} -> app_subst ML (M x) (M' x) ->
app_subst ML (M V) (M' V)
subst_inst < induction on 2.
IH : forall ML M M' V, nabla x, {tm V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
============================
forall ML M M' V, nabla x, {tm V} -> app_subst ML (M x) (M' x) @ ->
app_subst ML (M V) (M' V)
subst_inst < intros.
Variables: ML M M' V
IH : forall ML M M' V, nabla x, {tm V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm V}
H2 : app_subst ML (M n1) (M' n1) @
============================
app_subst ML (M V) (M' V)
subst_inst < case H2.
Subgoal 1:
Variables: M' V
IH : forall ML M M' V, nabla x, {tm V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm V}
============================
app_subst nil (M' V) (M' V)
Subgoal 2 is:
app_subst (map n2 ML2 :: ML3) (M n2 (V n2)) (M2 (V n2))
subst_inst < search.
Subgoal 2:
Variables: M V M2 ML3 ML2
IH : forall ML M M' V, nabla x, {tm V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm (V n2)}
H3 : app_subst ML3 (M ML2 n1) (M2 n1) *
============================
app_subst (map n2 ML2 :: ML3) (M n2 (V n2)) (M2 (V n2))
subst_inst < apply sclosed_tm_prune to H1.
Subgoal 2:
Variables: M M2 ML3 ML2 M'1
IH : forall ML M M' V, nabla x, {tm V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm M'1}
H3 : app_subst ML3 (M ML2 n1) (M2 n1) *
============================
app_subst (map n2 ML2 :: ML3) (M n2 M'1) (M2 M'1)
subst_inst < unfold.
Subgoal 2:
Variables: M M2 ML3 ML2 M'1
IH : forall ML M M' V, nabla x, {tm V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm M'1}
H3 : app_subst ML3 (M ML2 n1) (M2 n1) *
============================
app_subst ML3 (M ML2 M'1) (M2 M'1)
subst_inst < intros.
Subgoal 2:
Variables: M M2 ML3 ML2 M'1
IH : forall ML M M' V, nabla x, {tm V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm M'1}
H3 : app_subst ML3 (M ML2 n1) (M2 n1) *
============================
app_subst ML3 (M ML2 M'1) (M2 M'1)
subst_inst < apply IH to H1 H3.
Subgoal 2:
Variables: M M2 ML3 ML2 M'1
IH : forall ML M M' V, nabla x, {tm V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm M'1}
H3 : app_subst ML3 (M ML2 n1) (M2 n1) *
H4 : app_subst ML3 (M ML2 M'1) (M2 M'1)
============================
app_subst ML3 (M ML2 M'1) (M2 M'1)
subst_inst < search.
Proof completed.
Abella < Theorem explct_meta_subst_comm :
forall ML M E V, nabla n, {tm V} -> app_subst ML (M n) (E n) ->
app_subst (map n V :: ML) (M n) (E V).
============================
forall ML M E V, nabla n, {tm V} -> app_subst ML (M n) (E n) ->
app_subst (map n V :: ML) (M n) (E V)
explct_meta_subst_comm < intros.
Variables: ML M E V
H1 : {tm V}
H2 : app_subst ML (M n1) (E n1)
============================
app_subst (map n1 V :: ML) (M n1) (E V)
explct_meta_subst_comm < unfold.
Variables: ML M E V
H1 : {tm V}
H2 : app_subst ML (M n1) (E n1)
============================
app_subst ML (M V) (E V)
explct_meta_subst_comm < intros.
Variables: ML M E V
H1 : {tm V}
H2 : app_subst ML (M n1) (E n1)
============================
app_subst ML (M V) (E V)
explct_meta_subst_comm < backchain subst_inst with M = M, M' = E, x = n1.
Proof completed.
Abella < Theorem subst_closed_tm :
forall M ML, {tm M} -> subst ML -> app_subst ML M M.
============================
forall M ML, {tm M} -> subst ML -> app_subst ML M M
subst_closed_tm < induction on 2.
IH : forall M ML, {tm M} -> subst ML * -> app_subst ML M M
============================
forall M ML, {tm M} -> subst ML @ -> app_subst ML M M
subst_closed_tm < intros.
Variables: M ML
IH : forall M ML, {tm M} -> subst ML * -> app_subst ML M M
H1 : {tm M}
H2 : subst ML @
============================
app_subst ML M M
subst_closed_tm < case H2.
Subgoal 1:
Variables: M
IH : forall M ML, {tm M} -> subst ML * -> app_subst ML M M
H1 : {tm M}
============================
app_subst nil M M
Subgoal 2 is:
app_subst (map n1 V :: ML1) (M n1) (M n1)
subst_closed_tm < search.
Subgoal 2:
Variables: M ML1 V
IH : forall M ML, {tm M} -> subst ML * -> app_subst ML M M
H1 : {tm (M n1)}
H3 : subst ML1 *
H4 : {val V}
H5 : {tm V}
============================
app_subst (map n1 V :: ML1) (M n1) (M n1)
subst_closed_tm < apply sclosed_tm_prune to H1.
Subgoal 2:
Variables: ML1 V M'
IH : forall M ML, {tm M} -> subst ML * -> app_subst ML M M
H1 : {tm M'}
H3 : subst ML1 *
H4 : {val V}
H5 : {tm V}
============================
app_subst (map n1 V :: ML1) M' M'
subst_closed_tm < apply IH to H1 H3.
Subgoal 2:
Variables: ML1 V M'
IH : forall M ML, {tm M} -> subst ML * -> app_subst ML M M
H1 : {tm M'}
H3 : subst ML1 *
H4 : {val V}
H5 : {tm V}
H6 : app_subst ML1 M' M'
============================
app_subst (map n1 V :: ML1) M' M'
subst_closed_tm < search.
Proof completed.
Abella < Theorem subst_var :
forall V ML X, subst ML -> member (map X V) ML -> app_subst ML X V.
============================
forall V ML X, subst ML -> member (map X V) ML -> app_subst ML X V
subst_var < induction on 2.
IH : forall V ML X, subst ML -> member (map X V) ML * -> app_subst ML X V
============================
forall V ML X, subst ML -> member (map X V) ML @ -> app_subst ML X V
subst_var < intros.
Variables: V ML X
IH : forall V ML X, subst ML -> member (map X V) ML * -> app_subst ML X V
H1 : subst ML
H2 : member (map X V) ML @
============================
app_subst ML X V
subst_var < case H2.
Subgoal 1:
Variables: V X L
IH : forall V ML X, subst ML -> member (map X V) ML * -> app_subst ML X V
H1 : subst (map X V :: L)
============================
app_subst (map X V :: L) X V
Subgoal 2 is:
app_subst (B :: L) X V
subst_var < case H1.
Subgoal 1:
Variables: ML1 V1
IH : forall V ML X, subst ML -> member (map X V) ML * -> app_subst ML X V
H3 : subst ML1
H4 : {val V1}
H5 : {tm V1}
============================
app_subst (map n1 V1 :: ML1) n1 V1
Subgoal 2 is:
app_subst (B :: L) X V
subst_var < unfold.
Subgoal 1:
Variables: ML1 V1
IH : forall V ML X, subst ML -> member (map X V) ML * -> app_subst ML X V
H3 : subst ML1
H4 : {val V1}
H5 : {tm V1}
============================
app_subst ML1 V1 V1
Subgoal 2 is:
app_subst (B :: L) X V
subst_var < backchain subst_closed_tm.
Subgoal 2:
Variables: V X L B
IH : forall V ML X, subst ML -> member (map X V) ML * -> app_subst ML X V
H1 : subst (B :: L)
H3 : member (map X V) L *
============================
app_subst (B :: L) X V
subst_var < case H1.
Subgoal 2:
Variables: V X ML1 V1
IH : forall V ML X, subst ML -> member (map X V) ML * -> app_subst ML X V
H3 : member (map (X n1) (V n1)) ML1 *
H4 : subst ML1
H5 : {val V1}
H6 : {tm V1}
============================
app_subst (map n1 V1 :: ML1) (X n1) (V n1)
subst_var < apply member_prune to H3.
Subgoal 2:
Variables: ML1 V1 M'2 M'1
IH : forall V ML X, subst ML -> member (map X V) ML * -> app_subst ML X V
H3 : member (map M'1 M'2) ML1 *
H4 : subst ML1
H5 : {val V1}
H6 : {tm V1}
============================
app_subst (map n1 V1 :: ML1) M'1 M'2
subst_var < unfold.
Subgoal 2:
Variables: ML1 V1 M'2 M'1
IH : forall V ML X, subst ML -> member (map X V) ML * -> app_subst ML X V
H3 : member (map M'1 M'2) ML1 *
H4 : subst ML1
H5 : {val V1}
H6 : {tm V1}
============================
app_subst ML1 M'1 M'2
subst_var < backchain IH.
Proof completed.
Abella < Theorem subst_var_eq :
forall V ML E X, subst ML -> member (map X V) ML -> app_subst ML X E -> E = V.
============================
forall V ML E X, subst ML -> member (map X V) ML -> app_subst ML X E -> E =
V
subst_var_eq < intros.
Variables: V ML E X
H1 : subst ML
H2 : member (map X V) ML
H3 : app_subst ML X E
============================
E = V
subst_var_eq < apply subst_var to H1 H2.
Variables: V ML E X
H1 : subst ML
H2 : member (map X V) ML
H3 : app_subst ML X E
H4 : app_subst ML X V
============================
E = V
subst_var_eq < apply app_subst_det to H3 H4.
Variables: V ML X
H1 : subst ML
H2 : member (map X V) ML
H3 : app_subst ML X V
H4 : app_subst ML X V
============================
V = V
subst_var_eq < search.
Proof completed.
Abella < Theorem subst_nabla :
forall ML, nabla x, subst ML -> app_subst ML x x.
============================
forall ML, nabla x, subst ML -> app_subst ML x x
subst_nabla < induction on 1.
IH : forall ML, nabla x, subst ML * -> app_subst ML x x
============================
forall ML, nabla x, subst ML @ -> app_subst ML x x
subst_nabla < intros.
Variables: ML
IH : forall ML, nabla x, subst ML * -> app_subst ML x x
H1 : subst ML @
============================
app_subst ML n1 n1
subst_nabla < case H1.
Subgoal 1:
IH : forall ML, nabla x, subst ML * -> app_subst ML x x
============================
app_subst nil n1 n1
Subgoal 2 is:
app_subst (map n2 V :: ML1) n1 n1
subst_nabla < search.
Subgoal 2:
Variables: ML1 V
IH : forall ML, nabla x, subst ML * -> app_subst ML x x
H2 : subst ML1 *
H3 : {val V}
H4 : {tm V}
============================
app_subst (map n2 V :: ML1) n1 n1
subst_nabla < unfold.
Subgoal 2:
Variables: ML1 V
IH : forall ML, nabla x, subst ML * -> app_subst ML x x
H2 : subst ML1 *
H3 : {val V}
H4 : {tm V}
============================
app_subst ML1 n1 n1
subst_nabla < backchain IH.
Proof completed.
Abella < Theorem subst_result_closed_tm :
forall ML L M M' Vs, tm_sctx L -> {L |- tm M} -> vars_of_tm_sctx L Vs ->
subst ML -> vars_of_subst ML Vs -> app_subst ML M M' -> {tm M'}.
============================
forall ML L M M' Vs, tm_sctx L -> {L |- tm M} -> vars_of_tm_sctx L Vs ->
subst ML -> vars_of_subst ML Vs -> app_subst ML M M' -> {tm M'}
subst_result_closed_tm < induction on 1.
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
============================
forall ML L M M' Vs, tm_sctx L @ -> {L |- tm M} -> vars_of_tm_sctx L Vs ->
subst ML -> vars_of_subst ML Vs -> app_subst ML M M' -> {tm M'}
subst_result_closed_tm < intros.
Variables: ML L M M' Vs
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H1 : tm_sctx L @
H2 : {L |- tm M}
H3 : vars_of_tm_sctx L Vs
H4 : subst ML
H5 : vars_of_subst ML Vs
H6 : app_subst ML M M'
============================
{tm M'}
subst_result_closed_tm < case H1.
Subgoal 1:
Variables: ML M M' Vs
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H2 : {tm M}
H3 : vars_of_tm_sctx nil Vs
H4 : subst ML
H5 : vars_of_subst ML Vs
H6 : app_subst ML M M'
============================
{tm M'}
Subgoal 2 is:
{tm (M' n1)}
subst_result_closed_tm < case H3.
Subgoal 1:
Variables: ML M M'
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H2 : {tm M}
H4 : subst ML
H5 : vars_of_subst ML nil
H6 : app_subst ML M M'
============================
{tm M'}
Subgoal 2 is:
{tm (M' n1)}
subst_result_closed_tm < case H5.
Subgoal 1:
Variables: M M'
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H2 : {tm M}
H4 : subst nil
H6 : app_subst nil M M'
============================
{tm M'}
Subgoal 2 is:
{tm (M' n1)}
subst_result_closed_tm < case H6.
Subgoal 1:
Variables: M'
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H2 : {tm M'}
H4 : subst nil
============================
{tm M'}
Subgoal 2 is:
{tm (M' n1)}
subst_result_closed_tm < search.
Subgoal 2:
Variables: ML M M' Vs L1
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H2 : {L1, tm n1 |- tm (M n1)}
H3 : vars_of_tm_sctx (tm n1 :: L1) (Vs n1)
H4 : subst (ML n1)
H5 : vars_of_subst (ML n1) (Vs n1)
H6 : app_subst (ML n1) (M n1) (M' n1)
H7 : tm_sctx L1 *
============================
{tm (M' n1)}
subst_result_closed_tm < case H3.
Subgoal 2:
Variables: ML M M' L1 L'
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H2 : {L1, tm n1 |- tm (M n1)}
H4 : subst (ML n1)
H5 : vars_of_subst (ML n1) (n1 :: L')
H6 : app_subst (ML n1) (M n1) (M' n1)
H7 : tm_sctx L1 *
H8 : vars_of_tm_sctx L1 L'
============================
{tm (M' n1)}
subst_result_closed_tm < case H5.
Subgoal 2:
Variables: M M' L1 L' ML1 V
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H2 : {L1, tm n1 |- tm (M n1)}
H4 : subst (map n1 V :: ML1)
H6 : app_subst (map n1 V :: ML1) (M n1) (M' n1)
H7 : tm_sctx L1 *
H8 : vars_of_tm_sctx L1 L'
H9 : vars_of_subst ML1 L'
============================
{tm (M' n1)}
subst_result_closed_tm < case H6.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H2 : {L1, tm n1 |- tm (M n1)}
H4 : subst (map n1 V :: ML1)
H7 : tm_sctx L1 *
H8 : vars_of_tm_sctx L1 L'
H9 : vars_of_subst ML1 L'
H10 : app_subst ML1 (M V) M1
============================
{tm M1}
subst_result_closed_tm < case H4.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H2 : {L1, tm n1 |- tm (M n1)}
H7 : tm_sctx L1 *
H8 : vars_of_tm_sctx L1 L'
H9 : vars_of_subst ML1 L'
H10 : app_subst ML1 (M V) M1
H11 : subst ML1
H12 : {val V}
H13 : {tm V}
============================
{tm M1}
subst_result_closed_tm < inst H2 with n1 = V.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H2 : {L1, tm n1 |- tm (M n1)}
H7 : tm_sctx L1 *
H8 : vars_of_tm_sctx L1 L'
H9 : vars_of_subst ML1 L'
H10 : app_subst ML1 (M V) M1
H11 : subst ML1
H12 : {val V}
H13 : {tm V}
H14 : {L1, tm V |- tm (M V)}
============================
{tm M1}
subst_result_closed_tm < cut H14 with H13.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm_sctx L * -> {L |- tm M} ->
vars_of_tm_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
H2 : {L1, tm n1 |- tm (M n1)}
H7 : tm_sctx L1 *
H8 : vars_of_tm_sctx L1 L'
H9 : vars_of_subst ML1 L'
H10 : app_subst ML1 (M V) M1
H11 : subst ML1
H12 : {val V}
H13 : {tm V}
H14 : {L1, tm V |- tm (M V)}
H15 : {L1 |- tm (M V)}
============================
{tm M1}
subst_result_closed_tm < backchain IH with ML = ML1, L = L1, M = M V.
Proof completed.
Abella < Theorem subst_result_closed_tm' :
forall ML L T M M' Vs, {is_sty T} -> sctx L -> {L |- of M T} ->
vars_of_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}.
============================
forall ML L T M M' Vs, {is_sty T} -> sctx L -> {L |- of M T} ->
vars_of_sctx L Vs -> subst ML -> vars_of_subst ML Vs ->
app_subst ML M M' -> {tm M'}
subst_result_closed_tm' < intros.
Variables: ML L T M M' Vs
H1 : {is_sty T}
H2 : sctx L
H3 : {L |- of M T}
H4 : vars_of_sctx L Vs
H5 : subst ML
H6 : vars_of_subst ML Vs
H7 : app_subst ML M M'
============================
{tm M'}
subst_result_closed_tm' < apply sctx_to_tm_sctx to H2 H4.
Variables: ML L T M M' Vs SL
H1 : {is_sty T}
H2 : sctx L
H3 : {L |- of M T}
H4 : vars_of_sctx L Vs
H5 : subst ML
H6 : vars_of_subst ML Vs
H7 : app_subst ML M M'
H8 : tm_sctx SL
H9 : vars_of_tm_sctx SL Vs
============================
{tm M'}
subst_result_closed_tm' < assert {SL |- tm M}.
Subgoal 1:
Variables: ML L T M M' Vs SL
H1 : {is_sty T}
H2 : sctx L
H3 : {L |- of M T}
H4 : vars_of_sctx L Vs
H5 : subst ML
H6 : vars_of_subst ML Vs
H7 : app_subst ML M M'
H8 : tm_sctx SL
H9 : vars_of_tm_sctx SL Vs
============================
{SL |- tm M}
Subgoal is:
{tm M'}
subst_result_closed_tm' < backchain sof_to_tm with T = T.
Variables: ML L T M M' Vs SL
H1 : {is_sty T}
H2 : sctx L
H3 : {L |- of M T}
H4 : vars_of_sctx L Vs
H5 : subst ML
H6 : vars_of_subst ML Vs
H7 : app_subst ML M M'
H8 : tm_sctx SL
H9 : vars_of_tm_sctx SL Vs
H10 : {SL |- tm M}
============================
{tm M'}
subst_result_closed_tm' < backchain subst_result_closed_tm.
Proof completed.
Abella < Theorem app_subst_pred_comm :
forall ML M M', app_subst ML (pred M) M' ->
(exists M'', M' = pred M'' /\ app_subst ML M M'').
============================
forall ML M M', app_subst ML (pred M) M' ->
(exists M'', M' = pred M'' /\ app_subst ML M M'')
app_subst_pred_comm < induction on 1.
IH : forall ML M M', app_subst ML (pred M) M' * ->
(exists M'', M' = pred M'' /\ app_subst ML M M'')
============================
forall ML M M', app_subst ML (pred M) M' @ ->
(exists M'', M' = pred M'' /\ app_subst ML M M'')
app_subst_pred_comm < intros.
Variables: ML M M'
IH : forall ML M M', app_subst ML (pred M) M' * ->
(exists M'', M' = pred M'' /\ app_subst ML M M'')
H1 : app_subst ML (pred M) M' @
============================
exists M'', M' = pred M'' /\ app_subst ML M M''
app_subst_pred_comm < case H1.
Subgoal 1:
Variables: M
IH : forall ML M M', app_subst ML (pred M) M' * ->
(exists M'', M' = pred M'' /\ app_subst ML M M'')
============================
exists M'', pred M = pred M'' /\ app_subst nil M M''
Subgoal 2 is:
exists M'', M1 = pred M'' /\ app_subst (map n1 V :: ML1) (M n1) M''
app_subst_pred_comm < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML (pred M) M' * ->
(exists M'', M' = pred M'' /\ app_subst ML M M'')
H2 : app_subst ML1 (pred (M V)) M1 *
============================
exists M'', M1 = pred M'' /\ app_subst (map n1 V :: ML1) (M n1) M''
app_subst_pred_comm < apply IH to H2.
Subgoal 2:
Variables: M ML1 V M''
IH : forall ML M M', app_subst ML (pred M) M' * ->
(exists M'', M' = pred M'' /\ app_subst ML M M'')
H2 : app_subst ML1 (pred (M V)) (pred M'') *
H3 : app_subst ML1 (M V) M''
============================
exists M''1, pred M'' = pred M''1 /\ app_subst (map n1 V :: ML1) (M n1) M''1
app_subst_pred_comm < search.
Proof completed.
Abella < Theorem app_subst_ifz_comm :
forall ML M M1 M2 M3, app_subst ML (ifz M M1 M2) M3 ->
(exists M' M1' M2', M3 = ifz M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2').
============================
forall ML M M1 M2 M3, app_subst ML (ifz M M1 M2) M3 ->
(exists M' M1' M2', M3 = ifz M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
app_subst_ifz_comm < induction on 1.
IH : forall ML M M1 M2 M3, app_subst ML (ifz M M1 M2) M3 * ->
(exists M' M1' M2', M3 = ifz M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
============================
forall ML M M1 M2 M3, app_subst ML (ifz M M1 M2) M3 @ ->
(exists M' M1' M2', M3 = ifz M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
app_subst_ifz_comm < intros.
Variables: ML M M1 M2 M3
IH : forall ML M M1 M2 M3, app_subst ML (ifz M M1 M2) M3 * ->
(exists M' M1' M2', M3 = ifz M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
H1 : app_subst ML (ifz M M1 M2) M3 @
============================
exists M' M1' M2', M3 = ifz M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2'
app_subst_ifz_comm < case H1.
Subgoal 1:
Variables: M M1 M2
IH : forall ML M M1 M2 M3, app_subst ML (ifz M M1 M2) M3 * ->
(exists M' M1' M2', M3 = ifz M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
============================
exists M' M1' M2', ifz M M1 M2 = ifz M' M1' M2' /\ app_subst nil M M' /\
app_subst nil M1 M1' /\ app_subst nil M2 M2'
Subgoal 2 is:
exists M' M1' M2', M4 = ifz M' M1' M2' /\
app_subst (map n1 V :: ML1) (M n1) M' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst_ifz_comm < search.
Subgoal 2:
Variables: M M1 M2 M4 ML1 V
IH : forall ML M M1 M2 M3, app_subst ML (ifz M M1 M2) M3 * ->
(exists M' M1' M2', M3 = ifz M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
H2 : app_subst ML1 (ifz (M V) (M1 V) (M2 V)) M4 *
============================
exists M' M1' M2', M4 = ifz M' M1' M2' /\
app_subst (map n1 V :: ML1) (M n1) M' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst_ifz_comm < apply IH to H2.
Subgoal 2:
Variables: M M1 M2 ML1 V M' M1' M2'
IH : forall ML M M1 M2 M3, app_subst ML (ifz M M1 M2) M3 * ->
(exists M' M1' M2', M3 = ifz M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
H2 : app_subst ML1 (ifz (M V) (M1 V) (M2 V)) (ifz M' M1' M2') *
H3 : app_subst ML1 (M V) M'
H4 : app_subst ML1 (M1 V) M1'
H5 : app_subst ML1 (M2 V) M2'
============================
exists M'1 M1'1 M2'1, ifz M' M1' M2' = ifz M'1 M1'1 M2'1 /\
app_subst (map n1 V :: ML1) (M n1) M'1 /\
app_subst (map n1 V :: ML1) (M1 n1) M1'1 /\
app_subst (map n1 V :: ML1) (M2 n1) M2'1
app_subst_ifz_comm < search.
Proof completed.
Abella < Theorem app_subst_let_comm :
forall ML M R M', app_subst ML (let M R) M' ->
(exists M1 R1, M' = let M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x))).
============================
forall ML M R M', app_subst ML (let M R) M' ->
(exists M1 R1, M' = let M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
app_subst_let_comm < induction on 1.
IH : forall ML M R M', app_subst ML (let M R) M' * ->
(exists M1 R1, M' = let M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
============================
forall ML M R M', app_subst ML (let M R) M' @ ->
(exists M1 R1, M' = let M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
app_subst_let_comm < intros.
Variables: ML M R M'
IH : forall ML M R M', app_subst ML (let M R) M' * ->
(exists M1 R1, M' = let M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
H1 : app_subst ML (let M R) M' @
============================
exists M1 R1, M' = let M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x))
app_subst_let_comm < case H1.
Subgoal 1:
Variables: M R
IH : forall ML M R M', app_subst ML (let M R) M' * ->
(exists M1 R1, M' = let M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
============================
exists M1 R1, let M R = let M1 R1 /\ app_subst nil M M1 /\
(nabla x, app_subst nil (R x) (R1 x))
Subgoal 2 is:
exists M2 R1, M1 = let M2 R1 /\ app_subst (map n1 V :: ML1) (M n1) M2 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R1 x))
app_subst_let_comm < search.
Subgoal 2:
Variables: M R M1 ML1 V
IH : forall ML M R M', app_subst ML (let M R) M' * ->
(exists M1 R1, M' = let M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
H2 : app_subst ML1 (let (M V) (R V)) M1 *
============================
exists M2 R1, M1 = let M2 R1 /\ app_subst (map n1 V :: ML1) (M n1) M2 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R1 x))
app_subst_let_comm < apply IH to H2.
Subgoal 2:
Variables: M R ML1 V M2 R1
IH : forall ML M R M', app_subst ML (let M R) M' * ->
(exists M1 R1, M' = let M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
H2 : app_subst ML1 (let (M V) (R V)) (let M2 R1) *
H3 : app_subst ML1 (M V) M2
H4 : app_subst ML1 (R V n1) (R1 n1)
============================
exists M1 R2, let M2 R1 = let M1 R2 /\
app_subst (map n1 V :: ML1) (M n1) M1 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R2 x))
app_subst_let_comm < search.
Proof completed.
Abella < Theorem app_subst_fix_comm :
forall ML R M', app_subst ML (fix R) M' ->
(exists R', M' = fix R' /\ (nabla f x, app_subst ML (R f x) (R' f x))).
============================
forall ML R M', app_subst ML (fix R) M' ->
(exists R', M' = fix R' /\ (nabla f x, app_subst ML (R f x) (R' f x)))
app_subst_fix_comm < induction on 1.
IH : forall ML R M', app_subst ML (fix R) M' * ->
(exists R', M' = fix R' /\ (nabla f x, app_subst ML (R f x) (R' f x)))
============================
forall ML R M', app_subst ML (fix R) M' @ ->
(exists R', M' = fix R' /\ (nabla f x, app_subst ML (R f x) (R' f x)))
app_subst_fix_comm < intros.
Variables: ML R M'
IH : forall ML R M', app_subst ML (fix R) M' * ->
(exists R', M' = fix R' /\ (nabla f x, app_subst ML (R f x) (R' f x)))
H1 : app_subst ML (fix R) M' @
============================
exists R', M' = fix R' /\ (nabla f x, app_subst ML (R f x) (R' f x))
app_subst_fix_comm < case H1.
Subgoal 1:
Variables: R
IH : forall ML R M', app_subst ML (fix R) M' * ->
(exists R', M' = fix R' /\ (nabla f x, app_subst ML (R f x) (R' f x)))
============================
exists R', fix R = fix R' /\ (nabla f x, app_subst nil (R f x) (R' f x))
Subgoal 2 is:
exists R', M = fix R' /\
(nabla f x, app_subst (map n1 V :: ML1) (R n1 f x) (R' f x))
app_subst_fix_comm < search.
Subgoal 2:
Variables: R M ML1 V
IH : forall ML R M', app_subst ML (fix R) M' * ->
(exists R', M' = fix R' /\ (nabla f x, app_subst ML (R f x) (R' f x)))
H2 : app_subst ML1 (fix (R V)) M *
============================
exists R', M = fix R' /\
(nabla f x, app_subst (map n1 V :: ML1) (R n1 f x) (R' f x))
app_subst_fix_comm < apply IH to H2.
Subgoal 2:
Variables: R ML1 V R'
IH : forall ML R M', app_subst ML (fix R) M' * ->
(exists R', M' = fix R' /\ (nabla f x, app_subst ML (R f x) (R' f x)))
H2 : app_subst ML1 (fix (R V)) (fix R') *
H3 : app_subst ML1 (R V n1 n2) (R' n1 n2)
============================
exists R'1, fix R' = fix R'1 /\
(nabla f x, app_subst (map n1 V :: ML1) (R n1 f x) (R'1 f x))
app_subst_fix_comm < search.
Proof completed.
Abella < Theorem app_subst_app_comm :
forall ML M1 M2 M', app_subst ML (app M1 M2) M' ->
(exists M1' M2', M' = app M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2').
============================
forall ML M1 M2 M', app_subst ML (app M1 M2) M' ->
(exists M1' M2', M' = app M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst_app_comm < induction on 1.
IH : forall ML M1 M2 M', app_subst ML (app M1 M2) M' * ->
(exists M1' M2', M' = app M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
forall ML M1 M2 M', app_subst ML (app M1 M2) M' @ ->
(exists M1' M2', M' = app M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst_app_comm < intros.
Variables: ML M1 M2 M'
IH : forall ML M1 M2 M', app_subst ML (app M1 M2) M' * ->
(exists M1' M2', M' = app M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H1 : app_subst ML (app M1 M2) M' @
============================
exists M1' M2', M' = app M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2'
app_subst_app_comm < case H1.
Subgoal 1:
Variables: M1 M2
IH : forall ML M1 M2 M', app_subst ML (app M1 M2) M' * ->
(exists M1' M2', M' = app M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
exists M1' M2', app M1 M2 = app M1' M2' /\ app_subst nil M1 M1' /\
app_subst nil M2 M2'
Subgoal 2 is:
exists M1' M2', M = app M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst_app_comm < search.
Subgoal 2:
Variables: M1 M2 M ML1 V
IH : forall ML M1 M2 M', app_subst ML (app M1 M2) M' * ->
(exists M1' M2', M' = app M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (app (M1 V) (M2 V)) M *
============================
exists M1' M2', M = app M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst_app_comm < apply IH to H2.
Subgoal 2:
Variables: M1 M2 ML1 V M1' M2'
IH : forall ML M1 M2 M', app_subst ML (app M1 M2) M' * ->
(exists M1' M2', M' = app M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (app (M1 V) (M2 V)) (app M1' M2') *
H3 : app_subst ML1 (M1 V) M1'
H4 : app_subst ML1 (M2 V) M2'
============================
exists M1'1 M2'1, app M1' M2' = app M1'1 M2'1 /\
app_subst (map n1 V :: ML1) (M1 n1) M1'1 /\
app_subst (map n1 V :: ML1) (M2 n1) M2'1
app_subst_app_comm < search.
Proof completed.
Abella < Theorem app_subst_plus_comm :
forall ML M1 M2 M', app_subst ML (plus M1 M2) M' ->
(exists M1' M2', M' = plus M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2').
============================
forall ML M1 M2 M', app_subst ML (plus M1 M2) M' ->
(exists M1' M2', M' = plus M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst_plus_comm < induction on 1.
IH : forall ML M1 M2 M', app_subst ML (plus M1 M2) M' * ->
(exists M1' M2', M' = plus M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
forall ML M1 M2 M', app_subst ML (plus M1 M2) M' @ ->
(exists M1' M2', M' = plus M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst_plus_comm < intros.
Variables: ML M1 M2 M'
IH : forall ML M1 M2 M', app_subst ML (plus M1 M2) M' * ->
(exists M1' M2', M' = plus M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H1 : app_subst ML (plus M1 M2) M' @
============================
exists M1' M2', M' = plus M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2'
app_subst_plus_comm < case H1.
Subgoal 1:
Variables: M1 M2
IH : forall ML M1 M2 M', app_subst ML (plus M1 M2) M' * ->
(exists M1' M2', M' = plus M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
exists M1' M2', plus M1 M2 = plus M1' M2' /\ app_subst nil M1 M1' /\
app_subst nil M2 M2'
Subgoal 2 is:
exists M1' M2', M = plus M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst_plus_comm < search.
Subgoal 2:
Variables: M1 M2 M ML1 V
IH : forall ML M1 M2 M', app_subst ML (plus M1 M2) M' * ->
(exists M1' M2', M' = plus M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (plus (M1 V) (M2 V)) M *
============================
exists M1' M2', M = plus M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst_plus_comm < apply IH to H2.
Subgoal 2:
Variables: M1 M2 ML1 V M1' M2'
IH : forall ML M1 M2 M', app_subst ML (plus M1 M2) M' * ->
(exists M1' M2', M' = plus M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (plus (M1 V) (M2 V)) (plus M1' M2') *
H3 : app_subst ML1 (M1 V) M1'
H4 : app_subst ML1 (M2 V) M2'
============================
exists M1'1 M2'1, plus M1' M2' = plus M1'1 M2'1 /\
app_subst (map n1 V :: ML1) (M1 n1) M1'1 /\
app_subst (map n1 V :: ML1) (M2 n1) M2'1
app_subst_plus_comm < search.
Proof completed.
Abella < Theorem app_subst_pair_comm :
forall ML M1 M2 M', app_subst ML (pair M1 M2) M' ->
(exists M1' M2', M' = pair M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2').
============================
forall ML M1 M2 M', app_subst ML (pair M1 M2) M' ->
(exists M1' M2', M' = pair M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst_pair_comm < induction on 1.
IH : forall ML M1 M2 M', app_subst ML (pair M1 M2) M' * ->
(exists M1' M2', M' = pair M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
forall ML M1 M2 M', app_subst ML (pair M1 M2) M' @ ->
(exists M1' M2', M' = pair M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst_pair_comm < intros.
Variables: ML M1 M2 M'
IH : forall ML M1 M2 M', app_subst ML (pair M1 M2) M' * ->
(exists M1' M2', M' = pair M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H1 : app_subst ML (pair M1 M2) M' @
============================
exists M1' M2', M' = pair M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2'
app_subst_pair_comm < case H1.
Subgoal 1:
Variables: M1 M2
IH : forall ML M1 M2 M', app_subst ML (pair M1 M2) M' * ->
(exists M1' M2', M' = pair M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
exists M1' M2', pair M1 M2 = pair M1' M2' /\ app_subst nil M1 M1' /\
app_subst nil M2 M2'
Subgoal 2 is:
exists M1' M2', M = pair M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst_pair_comm < search.
Subgoal 2:
Variables: M1 M2 M ML1 V
IH : forall ML M1 M2 M', app_subst ML (pair M1 M2) M' * ->
(exists M1' M2', M' = pair M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (pair (M1 V) (M2 V)) M *
============================
exists M1' M2', M = pair M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst_pair_comm < apply IH to H2.
Subgoal 2:
Variables: M1 M2 ML1 V M1' M2'
IH : forall ML M1 M2 M', app_subst ML (pair M1 M2) M' * ->
(exists M1' M2', M' = pair M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (pair (M1 V) (M2 V)) (pair M1' M2') *
H3 : app_subst ML1 (M1 V) M1'
H4 : app_subst ML1 (M2 V) M2'
============================
exists M1'1 M2'1, pair M1' M2' = pair M1'1 M2'1 /\
app_subst (map n1 V :: ML1) (M1 n1) M1'1 /\
app_subst (map n1 V :: ML1) (M2 n1) M2'1
app_subst_pair_comm < search.
Proof completed.
Abella < Theorem app_subst_fst_comm :
forall ML M M', app_subst ML (fst M) M' ->
(exists M1', M' = fst M1' /\ app_subst ML M M1').
============================
forall ML M M', app_subst ML (fst M) M' ->
(exists M1', M' = fst M1' /\ app_subst ML M M1')
app_subst_fst_comm < induction on 1.
IH : forall ML M M', app_subst ML (fst M) M' * ->
(exists M1', M' = fst M1' /\ app_subst ML M M1')
============================
forall ML M M', app_subst ML (fst M) M' @ ->
(exists M1', M' = fst M1' /\ app_subst ML M M1')
app_subst_fst_comm < intros.
Variables: ML M M'
IH : forall ML M M', app_subst ML (fst M) M' * ->
(exists M1', M' = fst M1' /\ app_subst ML M M1')
H1 : app_subst ML (fst M) M' @
============================
exists M1', M' = fst M1' /\ app_subst ML M M1'
app_subst_fst_comm < case H1.
Subgoal 1:
Variables: M
IH : forall ML M M', app_subst ML (fst M) M' * ->
(exists M1', M' = fst M1' /\ app_subst ML M M1')
============================
exists M1', fst M = fst M1' /\ app_subst nil M M1'
Subgoal 2 is:
exists M1', M1 = fst M1' /\ app_subst (map n1 V :: ML1) (M n1) M1'
app_subst_fst_comm < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML (fst M) M' * ->
(exists M1', M' = fst M1' /\ app_subst ML M M1')
H2 : app_subst ML1 (fst (M V)) M1 *
============================
exists M1', M1 = fst M1' /\ app_subst (map n1 V :: ML1) (M n1) M1'
app_subst_fst_comm < apply IH to H2.
Subgoal 2:
Variables: M ML1 V M1'
IH : forall ML M M', app_subst ML (fst M) M' * ->
(exists M1', M' = fst M1' /\ app_subst ML M M1')
H2 : app_subst ML1 (fst (M V)) (fst M1') *
H3 : app_subst ML1 (M V) M1'
============================
exists M1'1, fst M1' = fst M1'1 /\ app_subst (map n1 V :: ML1) (M n1) M1'1
app_subst_fst_comm < search.
Proof completed.
Abella < Theorem app_subst_snd_comm :
forall ML M M', app_subst ML (snd M) M' ->
(exists M1', M' = snd M1' /\ app_subst ML M M1').
============================
forall ML M M', app_subst ML (snd M) M' ->
(exists M1', M' = snd M1' /\ app_subst ML M M1')
app_subst_snd_comm < induction on 1.
IH : forall ML M M', app_subst ML (snd M) M' * ->
(exists M1', M' = snd M1' /\ app_subst ML M M1')
============================
forall ML M M', app_subst ML (snd M) M' @ ->
(exists M1', M' = snd M1' /\ app_subst ML M M1')
app_subst_snd_comm < intros.
Variables: ML M M'
IH : forall ML M M', app_subst ML (snd M) M' * ->
(exists M1', M' = snd M1' /\ app_subst ML M M1')
H1 : app_subst ML (snd M) M' @
============================
exists M1', M' = snd M1' /\ app_subst ML M M1'
app_subst_snd_comm < case H1.
Subgoal 1:
Variables: M
IH : forall ML M M', app_subst ML (snd M) M' * ->
(exists M1', M' = snd M1' /\ app_subst ML M M1')
============================
exists M1', snd M = snd M1' /\ app_subst nil M M1'
Subgoal 2 is:
exists M1', M1 = snd M1' /\ app_subst (map n1 V :: ML1) (M n1) M1'
app_subst_snd_comm < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML (snd M) M' * ->
(exists M1', M' = snd M1' /\ app_subst ML M M1')
H2 : app_subst ML1 (snd (M V)) M1 *
============================
exists M1', M1 = snd M1' /\ app_subst (map n1 V :: ML1) (M n1) M1'
app_subst_snd_comm < apply IH to H2.
Subgoal 2:
Variables: M ML1 V M1'
IH : forall ML M M', app_subst ML (snd M) M' * ->
(exists M1', M' = snd M1' /\ app_subst ML M M1')
H2 : app_subst ML1 (snd (M V)) (snd M1') *
H3 : app_subst ML1 (M V) M1'
============================
exists M1'1, snd M1' = snd M1'1 /\ app_subst (map n1 V :: ML1) (M n1) M1'1
app_subst_snd_comm < search.
Proof completed.
Abella < Theorem app_subst_meta_app_comm :
forall ML R M P, app_subst ML (R M) P ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x))).
============================
forall ML R M P, app_subst ML (R M) P ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x)))
app_subst_meta_app_comm < induction on 1.
IH : forall ML R M P, app_subst ML (R M) P * ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x)))
============================
forall ML R M P, app_subst ML (R M) P @ ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x)))
app_subst_meta_app_comm < intros.
Variables: ML R M P
IH : forall ML R M P, app_subst ML (R M) P * ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x)))
H1 : app_subst ML (R M) P @
============================
exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x))
app_subst_meta_app_comm < case H1.
Subgoal 1:
Variables: R M
IH : forall ML R M P, app_subst ML (R M) P * ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x)))
============================
exists R' M', R M = R' M' /\ app_subst nil M M' /\
(nabla x, app_subst nil (R x) (R' x))
Subgoal 2 is:
exists R' M', M1 = R' M' /\ app_subst (map n1 V :: ML1) (M n1) M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x))
app_subst_meta_app_comm < exists R.
Subgoal 1:
Variables: R M
IH : forall ML R M P, app_subst ML (R M) P * ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x)))
============================
exists M', R M = R M' /\ app_subst nil M M' /\
(nabla x, app_subst nil (R x) (R x))
Subgoal 2 is:
exists R' M', M1 = R' M' /\ app_subst (map n1 V :: ML1) (M n1) M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x))
app_subst_meta_app_comm < exists M.
Subgoal 1:
Variables: R M
IH : forall ML R M P, app_subst ML (R M) P * ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x)))
============================
R M = R M /\ app_subst nil M M /\ (nabla x, app_subst nil (R x) (R x))
Subgoal 2 is:
exists R' M', M1 = R' M' /\ app_subst (map n1 V :: ML1) (M n1) M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x))
app_subst_meta_app_comm < search.
Subgoal 2:
Variables: R M M1 ML1 V
IH : forall ML R M P, app_subst ML (R M) P * ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x)))
H2 : app_subst ML1 (R V (M V)) M1 *
============================
exists R' M', M1 = R' M' /\ app_subst (map n1 V :: ML1) (M n1) M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x))
app_subst_meta_app_comm < apply IH to H2 with R = R V, M = M V.
Subgoal 2:
Variables: R M ML1 V R' M'
IH : forall ML R M P, app_subst ML (R M) P * ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x)))
H2 : app_subst ML1 (R V (M V)) (R' M') *
H3 : app_subst ML1 (M V) M'
H4 : app_subst ML1 (R V n1) (R' n1)
============================
exists R'1 M'1, R' M' = R'1 M'1 /\ app_subst (map n1 V :: ML1) (M n1) M'1 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R'1 x))
app_subst_meta_app_comm < exists R'.
Subgoal 2:
Variables: R M ML1 V R' M'
IH : forall ML R M P, app_subst ML (R M) P * ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x)))
H2 : app_subst ML1 (R V (M V)) (R' M') *
H3 : app_subst ML1 (M V) M'
H4 : app_subst ML1 (R V n1) (R' n1)
============================
exists M'1, R' M' = R' M'1 /\ app_subst (map n1 V :: ML1) (M n1) M'1 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x))
app_subst_meta_app_comm < exists M'.
Subgoal 2:
Variables: R M ML1 V R' M'
IH : forall ML R M P, app_subst ML (R M) P * ->
(exists R' M', P = R' M' /\ app_subst ML M M' /\
(nabla x, app_subst ML (R x) (R' x)))
H2 : app_subst ML1 (R V (M V)) (R' M') *
H3 : app_subst ML1 (M V) M'
H4 : app_subst ML1 (R V n1) (R' n1)
============================
R' M' = R' M' /\ app_subst (map n1 V :: ML1) (M n1) M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x))
app_subst_meta_app_comm < search.
Proof completed.
Abella < Theorem app_subst_pred_compose :
forall ML M M', app_subst ML M M' -> app_subst ML (pred M) (pred M').
============================
forall ML M M', app_subst ML M M' -> app_subst ML (pred M) (pred M')
app_subst_pred_compose < induction on 1.
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (pred M) (pred M')
============================
forall ML M M', app_subst ML M M' @ -> app_subst ML (pred M) (pred M')
app_subst_pred_compose < intros.
Variables: ML M M'
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (pred M) (pred M')
H1 : app_subst ML M M' @
============================
app_subst ML (pred M) (pred M')
app_subst_pred_compose < case H1.
Subgoal 1:
Variables: M'
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (pred M) (pred M')
============================
app_subst nil (pred M') (pred M')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (pred (M n1)) (pred M1)
app_subst_pred_compose < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (pred M) (pred M')
H2 : app_subst ML1 (M V) M1 *
============================
app_subst (map n1 V :: ML1) (pred (M n1)) (pred M1)
app_subst_pred_compose < unfold.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (pred M) (pred M')
H2 : app_subst ML1 (M V) M1 *
============================
app_subst ML1 (pred (M V)) (pred M1)
app_subst_pred_compose < backchain IH.
Proof completed.
Abella < Theorem app_subst_ifz_compose :
forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' -> app_subst ML M2 M2' ->
app_subst ML M3 M3' -> app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3').
============================
forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' ->
app_subst ML M2 M2' -> app_subst ML M3 M3' ->
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
app_subst_ifz_compose < induction on 1.
IH : forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' * ->
app_subst ML M2 M2' -> app_subst ML M3 M3' ->
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
============================
forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' @ ->
app_subst ML M2 M2' -> app_subst ML M3 M3' ->
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
app_subst_ifz_compose < intros.
Variables: ML M1 M2 M1' M2' M3 M3'
IH : forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' * ->
app_subst ML M2 M2' -> app_subst ML M3 M3' ->
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
H1 : app_subst ML M1 M1' @
H2 : app_subst ML M2 M2'
H3 : app_subst ML M3 M3'
============================
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
app_subst_ifz_compose < case H1.
Subgoal 1:
Variables: M2 M1' M2' M3 M3'
IH : forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' * ->
app_subst ML M2 M2' -> app_subst ML M3 M3' ->
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
H2 : app_subst nil M2 M2'
H3 : app_subst nil M3 M3'
============================
app_subst nil (ifz M1' M2 M3) (ifz M1' M2' M3')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (ifz (M1 n1) (M2 n1) (M3 n1))
(ifz M (M2' n1) (M3' n1))
app_subst_ifz_compose < case H2.
Subgoal 1:
Variables: M1' M2' M3 M3'
IH : forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' * ->
app_subst ML M2 M2' -> app_subst ML M3 M3' ->
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
H3 : app_subst nil M3 M3'
============================
app_subst nil (ifz M1' M2' M3) (ifz M1' M2' M3')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (ifz (M1 n1) (M2 n1) (M3 n1))
(ifz M (M2' n1) (M3' n1))
app_subst_ifz_compose < case H3.
Subgoal 1:
Variables: M1' M2' M3'
IH : forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' * ->
app_subst ML M2 M2' -> app_subst ML M3 M3' ->
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
============================
app_subst nil (ifz M1' M2' M3') (ifz M1' M2' M3')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (ifz (M1 n1) (M2 n1) (M3 n1))
(ifz M (M2' n1) (M3' n1))
app_subst_ifz_compose < search.
Subgoal 2:
Variables: M1 M2 M2' M3 M3' M ML1 V
IH : forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' * ->
app_subst ML M2 M2' -> app_subst ML M3 M3' ->
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
H2 : app_subst (map n1 V :: ML1) (M2 n1) (M2' n1)
H3 : app_subst (map n1 V :: ML1) (M3 n1) (M3' n1)
H4 : app_subst ML1 (M1 V) M *
============================
app_subst (map n1 V :: ML1) (ifz (M1 n1) (M2 n1) (M3 n1))
(ifz M (M2' n1) (M3' n1))
app_subst_ifz_compose < case H2.
Subgoal 2:
Variables: M1 M2 M3 M3' M ML1 V M4
IH : forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' * ->
app_subst ML M2 M2' -> app_subst ML M3 M3' ->
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
H3 : app_subst (map n1 V :: ML1) (M3 n1) (M3' n1)
H4 : app_subst ML1 (M1 V) M *
H5 : app_subst ML1 (M2 V) M4
============================
app_subst (map n1 V :: ML1) (ifz (M1 n1) (M2 n1) (M3 n1))
(ifz M M4 (M3' n1))
app_subst_ifz_compose < case H3.
Subgoal 2:
Variables: M1 M2 M3 M ML1 V M4 M5
IH : forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' * ->
app_subst ML M2 M2' -> app_subst ML M3 M3' ->
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
H4 : app_subst ML1 (M1 V) M *
H5 : app_subst ML1 (M2 V) M4
H6 : app_subst ML1 (M3 V) M5
============================
app_subst (map n1 V :: ML1) (ifz (M1 n1) (M2 n1) (M3 n1)) (ifz M M4 M5)
app_subst_ifz_compose < unfold.
Subgoal 2:
Variables: M1 M2 M3 M ML1 V M4 M5
IH : forall ML M1 M2 M1' M2' M3 M3', app_subst ML M1 M1' * ->
app_subst ML M2 M2' -> app_subst ML M3 M3' ->
app_subst ML (ifz M1 M2 M3) (ifz M1' M2' M3')
H4 : app_subst ML1 (M1 V) M *
H5 : app_subst ML1 (M2 V) M4
H6 : app_subst ML1 (M3 V) M5
============================
app_subst ML1 (ifz (M1 V) (M2 V) (M3 V)) (ifz M M4 M5)
app_subst_ifz_compose < backchain IH.
Proof completed.
Abella < Theorem app_subst_plus_compose :
forall ML M1 M2 M1' M2', app_subst ML M1 M1' -> app_subst ML M2 M2' ->
app_subst ML (plus M1 M2) (plus M1' M2').
============================
forall ML M1 M2 M1' M2', app_subst ML M1 M1' -> app_subst ML M2 M2' ->
app_subst ML (plus M1 M2) (plus M1' M2')
app_subst_plus_compose < induction on 1.
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (plus M1 M2) (plus M1' M2')
============================
forall ML M1 M2 M1' M2', app_subst ML M1 M1' @ -> app_subst ML M2 M2' ->
app_subst ML (plus M1 M2) (plus M1' M2')
app_subst_plus_compose < intros.
Variables: ML M1 M2 M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (plus M1 M2) (plus M1' M2')
H1 : app_subst ML M1 M1' @
H2 : app_subst ML M2 M2'
============================
app_subst ML (plus M1 M2) (plus M1' M2')
app_subst_plus_compose < case H1.
Subgoal 1:
Variables: M2 M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (plus M1 M2) (plus M1' M2')
H2 : app_subst nil M2 M2'
============================
app_subst nil (plus M1' M2) (plus M1' M2')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (plus (M1 n1) (M2 n1)) (plus M (M2' n1))
app_subst_plus_compose < case H2.
Subgoal 1:
Variables: M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (plus M1 M2) (plus M1' M2')
============================
app_subst nil (plus M1' M2') (plus M1' M2')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (plus (M1 n1) (M2 n1)) (plus M (M2' n1))
app_subst_plus_compose < search.
Subgoal 2:
Variables: M1 M2 M2' M ML1 V
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (plus M1 M2) (plus M1' M2')
H2 : app_subst (map n1 V :: ML1) (M2 n1) (M2' n1)
H3 : app_subst ML1 (M1 V) M *
============================
app_subst (map n1 V :: ML1) (plus (M1 n1) (M2 n1)) (plus M (M2' n1))
app_subst_plus_compose < case H2.
Subgoal 2:
Variables: M1 M2 M ML1 V M3
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (plus M1 M2) (plus M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V) M3
============================
app_subst (map n1 V :: ML1) (plus (M1 n1) (M2 n1)) (plus M M3)
app_subst_plus_compose < unfold.
Subgoal 2:
Variables: M1 M2 M ML1 V M3
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (plus M1 M2) (plus M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V) M3
============================
app_subst ML1 (plus (M1 V) (M2 V)) (plus M M3)
app_subst_plus_compose < backchain IH.
Proof completed.
Abella < Theorem app_subst_fst_compose :
forall ML M M', app_subst ML M M' -> app_subst ML (fst M) (fst M').
============================
forall ML M M', app_subst ML M M' -> app_subst ML (fst M) (fst M')
app_subst_fst_compose < induction on 1.
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (fst M) (fst M')
============================
forall ML M M', app_subst ML M M' @ -> app_subst ML (fst M) (fst M')
app_subst_fst_compose < intros.
Variables: ML M M'
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (fst M) (fst M')
H1 : app_subst ML M M' @
============================
app_subst ML (fst M) (fst M')
app_subst_fst_compose < case H1.
Subgoal 1:
Variables: M'
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (fst M) (fst M')
============================
app_subst nil (fst M') (fst M')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (fst (M n1)) (fst M1)
app_subst_fst_compose < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (fst M) (fst M')
H2 : app_subst ML1 (M V) M1 *
============================
app_subst (map n1 V :: ML1) (fst (M n1)) (fst M1)
app_subst_fst_compose < unfold.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (fst M) (fst M')
H2 : app_subst ML1 (M V) M1 *
============================
app_subst ML1 (fst (M V)) (fst M1)
app_subst_fst_compose < backchain IH.
Proof completed.
Abella < Theorem app_subst_snd_compose :
forall ML M M', app_subst ML M M' -> app_subst ML (snd M) (snd M').
============================
forall ML M M', app_subst ML M M' -> app_subst ML (snd M) (snd M')
app_subst_snd_compose < induction on 1.
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (snd M) (snd M')
============================
forall ML M M', app_subst ML M M' @ -> app_subst ML (snd M) (snd M')
app_subst_snd_compose < intros.
Variables: ML M M'
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (snd M) (snd M')
H1 : app_subst ML M M' @
============================
app_subst ML (snd M) (snd M')
app_subst_snd_compose < case H1.
Subgoal 1:
Variables: M'
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (snd M) (snd M')
============================
app_subst nil (snd M') (snd M')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (snd (M n1)) (snd M1)
app_subst_snd_compose < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (snd M) (snd M')
H2 : app_subst ML1 (M V) M1 *
============================
app_subst (map n1 V :: ML1) (snd (M n1)) (snd M1)
app_subst_snd_compose < unfold.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (snd M) (snd M')
H2 : app_subst ML1 (M V) M1 *
============================
app_subst ML1 (snd (M V)) (snd M1)
app_subst_snd_compose < backchain IH.
Proof completed.
Abella < Theorem app_subst_pair_compose :
forall ML M1 M2 M1' M2', app_subst ML M1 M1' -> app_subst ML M2 M2' ->
app_subst ML (pair M1 M2) (pair M1' M2').
============================
forall ML M1 M2 M1' M2', app_subst ML M1 M1' -> app_subst ML M2 M2' ->
app_subst ML (pair M1 M2) (pair M1' M2')
app_subst_pair_compose < induction on 1.
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair M1 M2) (pair M1' M2')
============================
forall ML M1 M2 M1' M2', app_subst ML M1 M1' @ -> app_subst ML M2 M2' ->
app_subst ML (pair M1 M2) (pair M1' M2')
app_subst_pair_compose < intros.
Variables: ML M1 M2 M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair M1 M2) (pair M1' M2')
H1 : app_subst ML M1 M1' @
H2 : app_subst ML M2 M2'
============================
app_subst ML (pair M1 M2) (pair M1' M2')
app_subst_pair_compose < case H1.
Subgoal 1:
Variables: M2 M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair M1 M2) (pair M1' M2')
H2 : app_subst nil M2 M2'
============================
app_subst nil (pair M1' M2) (pair M1' M2')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (pair (M1 n1) (M2 n1)) (pair M (M2' n1))
app_subst_pair_compose < case H2.
Subgoal 1:
Variables: M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair M1 M2) (pair M1' M2')
============================
app_subst nil (pair M1' M2') (pair M1' M2')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (pair (M1 n1) (M2 n1)) (pair M (M2' n1))
app_subst_pair_compose < search.
Subgoal 2:
Variables: M1 M2 M2' M ML1 V
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair M1 M2) (pair M1' M2')
H2 : app_subst (map n1 V :: ML1) (M2 n1) (M2' n1)
H3 : app_subst ML1 (M1 V) M *
============================
app_subst (map n1 V :: ML1) (pair (M1 n1) (M2 n1)) (pair M (M2' n1))
app_subst_pair_compose < case H2.
Subgoal 2:
Variables: M1 M2 M ML1 V M3
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair M1 M2) (pair M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V) M3
============================
app_subst (map n1 V :: ML1) (pair (M1 n1) (M2 n1)) (pair M M3)
app_subst_pair_compose < unfold.
Subgoal 2:
Variables: M1 M2 M ML1 V M3
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair M1 M2) (pair M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V) M3
============================
app_subst ML1 (pair (M1 V) (M2 V)) (pair M M3)
app_subst_pair_compose < backchain IH.
Proof completed.
Abella < Theorem app_subst_app_compose :
forall ML M1 M2 M1' M2', app_subst ML M1 M1' -> app_subst ML M2 M2' ->
app_subst ML (app M1 M2) (app M1' M2').
============================
forall ML M1 M2 M1' M2', app_subst ML M1 M1' -> app_subst ML M2 M2' ->
app_subst ML (app M1 M2) (app M1' M2')
app_subst_app_compose < induction on 1.
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (app M1 M2) (app M1' M2')
============================
forall ML M1 M2 M1' M2', app_subst ML M1 M1' @ -> app_subst ML M2 M2' ->
app_subst ML (app M1 M2) (app M1' M2')
app_subst_app_compose < intros.
Variables: ML M1 M2 M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (app M1 M2) (app M1' M2')
H1 : app_subst ML M1 M1' @
H2 : app_subst ML M2 M2'
============================
app_subst ML (app M1 M2) (app M1' M2')
app_subst_app_compose < case H1.
Subgoal 1:
Variables: M2 M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (app M1 M2) (app M1' M2')
H2 : app_subst nil M2 M2'
============================
app_subst nil (app M1' M2) (app M1' M2')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (app (M1 n1) (M2 n1)) (app M (M2' n1))
app_subst_app_compose < case H2.
Subgoal 1:
Variables: M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (app M1 M2) (app M1' M2')
============================
app_subst nil (app M1' M2') (app M1' M2')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (app (M1 n1) (M2 n1)) (app M (M2' n1))
app_subst_app_compose < search.
Subgoal 2:
Variables: M1 M2 M2' M ML1 V
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (app M1 M2) (app M1' M2')
H2 : app_subst (map n1 V :: ML1) (M2 n1) (M2' n1)
H3 : app_subst ML1 (M1 V) M *
============================
app_subst (map n1 V :: ML1) (app (M1 n1) (M2 n1)) (app M (M2' n1))
app_subst_app_compose < case H2.
Subgoal 2:
Variables: M1 M2 M ML1 V M3
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (app M1 M2) (app M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V) M3
============================
app_subst (map n1 V :: ML1) (app (M1 n1) (M2 n1)) (app M M3)
app_subst_app_compose < unfold.
Subgoal 2:
Variables: M1 M2 M ML1 V M3
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (app M1 M2) (app M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V) M3
============================
app_subst ML1 (app (M1 V) (M2 V)) (app M M3)
app_subst_app_compose < backchain IH.
Proof completed.
Abella < Theorem app_subst_fix_compose :
forall ML M M', nabla f x, app_subst ML (M f x) (M' f x) ->
app_subst ML (fix M) (fix M').
============================
forall ML M M', nabla f x, app_subst ML (M f x) (M' f x) ->
app_subst ML (fix M) (fix M')
app_subst_fix_compose < induction on 1.
IH : forall ML M M', nabla f x, app_subst ML (M f x) (M' f x) * ->
app_subst ML (fix M) (fix M')
============================
forall ML M M', nabla f x, app_subst ML (M f x) (M' f x) @ ->
app_subst ML (fix M) (fix M')
app_subst_fix_compose < intros.
Variables: ML M M'
IH : forall ML M M', nabla f x, app_subst ML (M f x) (M' f x) * ->
app_subst ML (fix M) (fix M')
H1 : app_subst ML (M n1 n2) (M' n1 n2) @
============================
app_subst ML (fix M) (fix M')
app_subst_fix_compose < case H1.
Subgoal 1:
Variables: M'
IH : forall ML M M', nabla f x, app_subst ML (M f x) (M' f x) * ->
app_subst ML (fix M) (fix M')
============================
app_subst nil (fix (z1\z2\M' z1 z2)) (fix M')
Subgoal 2 is:
app_subst (map n3 ML2 :: ML3) (fix (M n3)) (fix (z2\z3\M2 z2 z3))
app_subst_fix_compose < search.
Subgoal 2:
Variables: M M2 ML3 ML2
IH : forall ML M M', nabla f x, app_subst ML (M f x) (M' f x) * ->
app_subst ML (fix M) (fix M')
H2 : app_subst ML3 (M ML2 n1 n2) (M2 n1 n2) *
============================
app_subst (map n3 ML2 :: ML3) (fix (M n3)) (fix (z2\z3\M2 z2 z3))
app_subst_fix_compose < unfold.
Subgoal 2:
Variables: M M2 ML3 ML2
IH : forall ML M M', nabla f x, app_subst ML (M f x) (M' f x) * ->
app_subst ML (fix M) (fix M')
H2 : app_subst ML3 (M ML2 n1 n2) (M2 n1 n2) *
============================
app_subst ML3 (fix (M ML2)) (fix (z2\z3\M2 z2 z3))
app_subst_fix_compose < backchain IH with M = M ML2, M' = M2, f = n1, x = n2.
Proof completed.
Abella < Theorem app_subst_let_compose :
forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let M1 M2) (let M1' M2').
============================
forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let M1 M2) (let M1' M2')
app_subst_let_compose < induction on 1.
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let M1 M2) (let M1' M2')
============================
forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' @ ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let M1 M2) (let M1' M2')
app_subst_let_compose < intros.
Variables: ML M1 M2 M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let M1 M2) (let M1' M2')
H1 : app_subst ML M1 M1' @
H2 : app_subst ML (M2 n1) (M2' n1)
============================
app_subst ML (let M1 M2) (let M1' M2')
app_subst_let_compose < case H1.
Subgoal 1:
Variables: M2 M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let M1 M2) (let M1' M2')
H2 : app_subst nil (M2 n1) (M2' n1)
============================
app_subst nil (let M1' M2) (let M1' M2')
Subgoal 2 is:
app_subst (map n2 V :: ML1) (let (M1 n2) (M2 n2)) (let M (M2' n2))
app_subst_let_compose < case H2.
Subgoal 1:
Variables: M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let M1 M2) (let M1' M2')
============================
app_subst nil (let M1' (z1\M2' z1)) (let M1' M2')
Subgoal 2 is:
app_subst (map n2 V :: ML1) (let (M1 n2) (M2 n2)) (let M (M2' n2))
app_subst_let_compose < search.
Subgoal 2:
Variables: M1 M2 M2' M ML1 V
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let M1 M2) (let M1' M2')
H2 : app_subst (map n2 V :: ML1) (M2 n2 n1) (M2' n2 n1)
H3 : app_subst ML1 (M1 V) M *
============================
app_subst (map n2 V :: ML1) (let (M1 n2) (M2 n2)) (let M (M2' n2))
app_subst_let_compose < case H2.
Subgoal 2:
Variables: M1 M2 M ML1 V M4
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let M1 M2) (let M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V n1) (M4 n1)
============================
app_subst (map n2 V :: ML1) (let (M1 n2) (M2 n2)) (let M (z2\M4 z2))
app_subst_let_compose < unfold.
Subgoal 2:
Variables: M1 M2 M ML1 V M4
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let M1 M2) (let M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V n1) (M4 n1)
============================
app_subst ML1 (let (M1 V) (M2 V)) (let M (z2\M4 z2))
app_subst_let_compose < backchain IH with x = n1.
Proof completed.
Abella < Define vars_in_subst : (list tm) -> (list (map tm tm)) -> prop by
vars_in_subst nil ML;
vars_in_subst (X :: Vs) ML := vars_in_subst Vs ML /\ (exists V, member (map X V) ML).
Abella < Theorem vars_in_subst_extend :
forall Vs L E, vars_in_subst Vs L -> vars_in_subst Vs (E :: L).
============================
forall Vs L E, vars_in_subst Vs L -> vars_in_subst Vs (E :: L)
vars_in_subst_extend < induction on 1.
IH : forall Vs L E, vars_in_subst Vs L * -> vars_in_subst Vs (E :: L)
============================
forall Vs L E, vars_in_subst Vs L @ -> vars_in_subst Vs (E :: L)
vars_in_subst_extend < intros.
Variables: Vs L E
IH : forall Vs L E, vars_in_subst Vs L * -> vars_in_subst Vs (E :: L)
H1 : vars_in_subst Vs L @
============================
vars_in_subst Vs (E :: L)
vars_in_subst_extend < case H1.
Subgoal 1:
Variables: L E
IH : forall Vs L E, vars_in_subst Vs L * -> vars_in_subst Vs (E :: L)
============================
vars_in_subst nil (E :: L)
Subgoal 2 is:
vars_in_subst (X :: Vs1) (E :: L)
vars_in_subst_extend < search.
Subgoal 2:
Variables: L E V Vs1 X
IH : forall Vs L E, vars_in_subst Vs L * -> vars_in_subst Vs (E :: L)
H2 : vars_in_subst Vs1 L *
H3 : member (map X V) L
============================
vars_in_subst (X :: Vs1) (E :: L)
vars_in_subst_extend < apply IH to H2 with E = E.
Subgoal 2:
Variables: L E V Vs1 X
IH : forall Vs L E, vars_in_subst Vs L * -> vars_in_subst Vs (E :: L)
H2 : vars_in_subst Vs1 L *
H3 : member (map X V) L
H4 : vars_in_subst Vs1 (E :: L)
============================
vars_in_subst (X :: Vs1) (E :: L)
vars_in_subst_extend < search.
Proof completed.
Abella < Theorem subst_var_rsl_clear :
forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'').
============================
forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
subst_var_rsl_clear < induction on 2.
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
============================
forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) @ ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
subst_var_rsl_clear < intros.
Variables: ML V M M'
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
H1 : subst (ML n1)
H2 : member (map n1 V) (ML n1) @
H3 : app_subst (ML n1) (M n1) (M' n1)
============================
exists M'', M' = y\M''
subst_var_rsl_clear < case H2.
Subgoal 1:
Variables: V M M' L
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
H1 : subst (map n1 V :: L n1)
H3 : app_subst (map n1 V :: L n1) (M n1) (M' n1)
============================
exists M'', M' = y\M''
Subgoal 2 is:
exists M'', M' = y\M''
subst_var_rsl_clear < case H3.
Subgoal 1:
Variables: V M M1 ML1
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
H1 : subst (map n1 V :: ML1)
H4 : app_subst ML1 (M V) M1
============================
exists M'', z1\M1 = y\M''
Subgoal 2 is:
exists M'', M' = y\M''
subst_var_rsl_clear < search.
Subgoal 2:
Variables: V M M' L B
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
H1 : subst (B n1 :: L n1)
H3 : app_subst (B n1 :: L n1) (M n1) (M' n1)
H4 : member (map n1 V) (L n1) *
============================
exists M'', M' = y\M''
subst_var_rsl_clear < case H3.
Subgoal 2.1:
Variables: V M M2 ML2 V1
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
H1 : subst (map n2 (V1 n1) :: ML2 n1)
H4 : member (map n1 (V n2)) (ML2 n1) *
H5 : app_subst (ML2 n1) (M (V1 n1) n1) (M2 n1)
============================
exists M'', z2\M2 z2 = y\M''
Subgoal 2.2 is:
exists M'', z1\M1 = y\M''
subst_var_rsl_clear < case H1.
Subgoal 2.1:
Variables: V M M2 ML2 V1
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
H4 : member (map n1 (V n2)) (ML2 n1) *
H5 : app_subst (ML2 n1) (M (V1 n1) n1) (M2 n1)
H6 : subst (ML2 n1)
H7 : {val (V1 n1)}
H8 : {tm (V1 n1)}
============================
exists M'', z2\M2 z2 = y\M''
Subgoal 2.2 is:
exists M'', z1\M1 = y\M''
subst_var_rsl_clear < apply closed_tm_prune to H8.
Subgoal 2.1:
Variables: V M M2 ML2 M'1
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
H4 : member (map n1 (V n2)) (ML2 n1) *
H5 : app_subst (ML2 n1) (M M'1 n1) (M2 n1)
H6 : subst (ML2 n1)
H7 : {val M'1}
H8 : {tm M'1}
============================
exists M'', z2\M2 z2 = y\M''
Subgoal 2.2 is:
exists M'', z1\M1 = y\M''
subst_var_rsl_clear < apply IH to H6 H4 H5.
Subgoal 2.1:
Variables: V M ML2 M'1 M''
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
H4 : member (map n1 (V n2)) (ML2 n1) *
H5 : app_subst (ML2 n1) (M M'1 n1) M''
H6 : subst (ML2 n1)
H7 : {val M'1}
H8 : {tm M'1}
============================
exists M''1, z2\M'' = y\M''1
Subgoal 2.2 is:
exists M'', z1\M1 = y\M''
subst_var_rsl_clear < search.
Subgoal 2.2:
Variables: V M M1 ML1 V1
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) (M' x) -> (exists M'', M' = y\M'')
H1 : subst (map n1 V1 :: ML1)
H4 : member (map n1 V) ML1 *
H5 : app_subst ML1 (M V1) M1
============================
exists M'', z1\M1 = y\M''
subst_var_rsl_clear < search.
Proof completed.
Abella < Theorem subst_var_inst :
forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'.
============================
forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
subst_var_inst < induction on 2.
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
============================
forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) @ ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
subst_var_inst < intros.
Variables: ML V M M'
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H1 : subst (ML n1)
H2 : member (map n1 V) (ML n1) @
H3 : app_subst (ML n1) (M n1) M'
============================
app_subst (ML n1) (M V) M'
subst_var_inst < case H2.
Subgoal 1:
Variables: V M M' L
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H1 : subst (map n1 V :: L n1)
H3 : app_subst (map n1 V :: L n1) (M n1) M'
============================
app_subst (map n1 V :: L n1) (M V) M'
Subgoal 2 is:
app_subst (B n1 :: L n1) (M V) M'
subst_var_inst < case H3.
Subgoal 1:
Variables: V M M' ML1
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H1 : subst (map n1 V :: ML1)
H4 : app_subst ML1 (M V) M'
============================
app_subst (map n1 V :: ML1) (M V) M'
Subgoal 2 is:
app_subst (B n1 :: L n1) (M V) M'
subst_var_inst < search.
Subgoal 2:
Variables: V M M' L B
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H1 : subst (B n1 :: L n1)
H3 : app_subst (B n1 :: L n1) (M n1) M'
H4 : member (map n1 V) (L n1) *
============================
app_subst (B n1 :: L n1) (M V) M'
subst_var_inst < case H3.
Subgoal 2.1:
Variables: V M M2 ML2 V1
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H1 : subst (map n2 (V1 n1) :: ML2 n1)
H4 : member (map n1 (V n2)) (ML2 n1) *
H5 : app_subst (ML2 n1) (M (V1 n1) n1) M2
============================
app_subst (map n2 (V1 n1) :: ML2 n1) (M n2 (V n2)) M2
Subgoal 2.2 is:
app_subst (map n1 V1 :: ML1) (M V) M'
subst_var_inst < case H1.
Subgoal 2.1:
Variables: V M M2 ML2 V1
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H4 : member (map n1 (V n2)) (ML2 n1) *
H5 : app_subst (ML2 n1) (M (V1 n1) n1) M2
H6 : subst (ML2 n1)
H7 : {val (V1 n1)}
H8 : {tm (V1 n1)}
============================
app_subst (map n2 (V1 n1) :: ML2 n1) (M n2 (V n2)) M2
Subgoal 2.2 is:
app_subst (map n1 V1 :: ML1) (M V) M'
subst_var_inst < apply closed_tm_prune to H8.
Subgoal 2.1:
Variables: V M M2 ML2 M'1
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H4 : member (map n1 (V n2)) (ML2 n1) *
H5 : app_subst (ML2 n1) (M M'1 n1) M2
H6 : subst (ML2 n1)
H7 : {val M'1}
H8 : {tm M'1}
============================
app_subst (map n2 M'1 :: ML2 n1) (M n2 (V n2)) M2
Subgoal 2.2 is:
app_subst (map n1 V1 :: ML1) (M V) M'
subst_var_inst < apply subst_mem to H6 H4.
Subgoal 2.1:
Variables: M M2 ML2 M'1 V3
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H4 : member (map n1 (V3 n2)) (ML2 n1) *
H5 : app_subst (ML2 n1) (M M'1 n1) M2
H6 : subst (ML2 n1)
H7 : {val M'1}
H8 : {tm M'1}
H9 : name n1
H10 : {val (V3 n2)}
H11 : {tm (V3 n2)}
============================
app_subst (map n2 M'1 :: ML2 n1) (M n2 (V3 n2)) M2
Subgoal 2.2 is:
app_subst (map n1 V1 :: ML1) (M V) M'
subst_var_inst < apply closed_tm_prune to H11.
Subgoal 2.1:
Variables: M M2 ML2 M'1 M'2
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H4 : member (map n1 M'2) (ML2 n1) *
H5 : app_subst (ML2 n1) (M M'1 n1) M2
H6 : subst (ML2 n1)
H7 : {val M'1}
H8 : {tm M'1}
H9 : name n1
H10 : {val M'2}
H11 : {tm M'2}
============================
app_subst (map n2 M'1 :: ML2 n1) (M n2 M'2) M2
Subgoal 2.2 is:
app_subst (map n1 V1 :: ML1) (M V) M'
subst_var_inst < unfold.
Subgoal 2.1:
Variables: M M2 ML2 M'1 M'2
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H4 : member (map n1 M'2) (ML2 n1) *
H5 : app_subst (ML2 n1) (M M'1 n1) M2
H6 : subst (ML2 n1)
H7 : {val M'1}
H8 : {tm M'1}
H9 : name n1
H10 : {val M'2}
H11 : {tm M'2}
============================
app_subst (ML2 n1) (M M'1 M'2) M2
Subgoal 2.2 is:
app_subst (map n1 V1 :: ML1) (M V) M'
subst_var_inst < apply IH to H6 H4 H5.
Subgoal 2.1:
Variables: M M2 ML2 M'1 M'2
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H4 : member (map n1 M'2) (ML2 n1) *
H5 : app_subst (ML2 n1) (M M'1 n1) M2
H6 : subst (ML2 n1)
H7 : {val M'1}
H8 : {tm M'1}
H9 : name n1
H10 : {val M'2}
H11 : {tm M'2}
H12 : app_subst (ML2 n1) (M M'1 M'2) M2
============================
app_subst (ML2 n1) (M M'1 M'2) M2
Subgoal 2.2 is:
app_subst (map n1 V1 :: ML1) (M V) M'
subst_var_inst < search.
Subgoal 2.2:
Variables: V M M' ML1 V1
IH : forall ML V M M', nabla x, subst (ML x) -> member (map x V) (ML x) * ->
app_subst (ML x) (M x) M' -> app_subst (ML x) (M V) M'
H1 : subst (map n1 V1 :: ML1)
H4 : member (map n1 V) ML1 *
H5 : app_subst ML1 (M V1) M'
============================
app_subst (map n1 V1 :: ML1) (M V) M'
subst_var_inst < apply member_prune to H4.
Proof completed.
Abella < Theorem subst_result_closed_tm_alt :
forall ML L M M' Vs, subst ML -> tm_ctx L -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}.
============================
forall ML L M M' Vs, subst ML -> tm_ctx L -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
subst_result_closed_tm_alt < induction on 2.
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
============================
forall ML L M M' Vs, subst ML -> tm_ctx L @ -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
subst_result_closed_tm_alt < intros.
Variables: ML L M M' Vs
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst ML
H2 : tm_ctx L @
H3 : {L |- tm M}
H4 : vars_of_tm_ctx L Vs
H5 : vars_in_subst Vs ML
H6 : app_subst ML M M'
============================
{tm M'}
subst_result_closed_tm_alt < case H2.
Subgoal 1:
Variables: ML M M' Vs
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst ML
H3 : {tm M}
H4 : vars_of_tm_ctx nil Vs
H5 : vars_in_subst Vs ML
H6 : app_subst ML M M'
============================
{tm M'}
Subgoal 2 is:
{tm M'}
subst_result_closed_tm_alt < case H4.
Subgoal 1:
Variables: ML M M'
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst ML
H3 : {tm M}
H5 : vars_in_subst nil ML
H6 : app_subst ML M M'
============================
{tm M'}
Subgoal 2 is:
{tm M'}
subst_result_closed_tm_alt < case H5.
Subgoal 1:
Variables: ML M M'
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst ML
H3 : {tm M}
H6 : app_subst ML M M'
============================
{tm M'}
Subgoal 2 is:
{tm M'}
subst_result_closed_tm_alt < apply subst_closed_tm_eq to _ H6.
Subgoal 1:
Variables: ML M'
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst ML
H3 : {tm M'}
H6 : app_subst ML M' M'
============================
{tm M'}
Subgoal 2 is:
{tm M'}
subst_result_closed_tm_alt < search.
Subgoal 2:
Variables: ML M M' Vs L1 X
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst ML
H3 : {L1, tm X |- tm M}
H4 : vars_of_tm_ctx (tm X :: L1) Vs
H5 : vars_in_subst Vs ML
H6 : app_subst ML M M'
H7 : tm_ctx L1 *
H8 : name X
============================
{tm M'}
subst_result_closed_tm_alt < case H4.
Subgoal 2:
Variables: ML M M' L1 X L'
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst ML
H3 : {L1, tm X |- tm M}
H5 : vars_in_subst (X :: L') ML
H6 : app_subst ML M M'
H7 : tm_ctx L1 *
H8 : name X
H9 : vars_of_tm_ctx L1 L'
============================
{tm M'}
subst_result_closed_tm_alt < case H5.
Subgoal 2:
Variables: ML M M' L1 X L' V
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst ML
H3 : {L1, tm X |- tm M}
H6 : app_subst ML M M'
H7 : tm_ctx L1 *
H8 : name X
H9 : vars_of_tm_ctx L1 L'
H10 : vars_in_subst L' ML
H11 : member (map X V) ML
============================
{tm M'}
subst_result_closed_tm_alt < apply subst_mem to _ H11.
Subgoal 2:
Variables: ML M M' L1 L' X1 V1
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst ML
H3 : {L1, tm X1 |- tm M}
H6 : app_subst ML M M'
H7 : tm_ctx L1 *
H8 : name X1
H9 : vars_of_tm_ctx L1 L'
H10 : vars_in_subst L' ML
H11 : member (map X1 V1) ML
H12 : name X1
H13 : {val V1}
H14 : {tm V1}
============================
{tm M'}
subst_result_closed_tm_alt < case H8.
Subgoal 2:
Variables: ML M M' L1 L' V1
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst (ML n1)
H3 : {L1 n1, tm n1 |- tm (M n1)}
H6 : app_subst (ML n1) (M n1) (M' n1)
H7 : tm_ctx (L1 n1) *
H9 : vars_of_tm_ctx (L1 n1) (L' n1)
H10 : vars_in_subst (L' n1) (ML n1)
H11 : member (map n1 (V1 n1)) (ML n1)
H12 : name n1
H13 : {val (V1 n1)}
H14 : {tm (V1 n1)}
============================
{tm (M' n1)}
subst_result_closed_tm_alt < apply closed_tm_prune to H14.
Subgoal 2:
Variables: ML M M' L1 L' M'1
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst (ML n1)
H3 : {L1 n1, tm n1 |- tm (M n1)}
H6 : app_subst (ML n1) (M n1) (M' n1)
H7 : tm_ctx (L1 n1) *
H9 : vars_of_tm_ctx (L1 n1) (L' n1)
H10 : vars_in_subst (L' n1) (ML n1)
H11 : member (map n1 M'1) (ML n1)
H12 : name n1
H13 : {val M'1}
H14 : {tm M'1}
============================
{tm (M' n1)}
subst_result_closed_tm_alt < apply tm_cut to _ H7 H3.
Subgoal 2:
Variables: ML M M' L1 L' M'1
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst (ML n1)
H3 : {L1 n1, tm n1 |- tm (M n1)}
H6 : app_subst (ML n1) (M n1) (M' n1)
H7 : tm_ctx (L1 n1) *
H9 : vars_of_tm_ctx (L1 n1) (L' n1)
H10 : vars_in_subst (L' n1) (ML n1)
H11 : member (map n1 M'1) (ML n1)
H12 : name n1
H13 : {val M'1}
H14 : {tm M'1}
H15 : {L1 n1 |- tm (M M'1)}
============================
{tm (M' n1)}
subst_result_closed_tm_alt < apply subst_var_rsl_clear to _ H11 H6.
Subgoal 2:
Variables: ML M L1 L' M'1 M''
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst (ML n1)
H3 : {L1 n1, tm n1 |- tm (M n1)}
H6 : app_subst (ML n1) (M n1) M''
H7 : tm_ctx (L1 n1) *
H9 : vars_of_tm_ctx (L1 n1) (L' n1)
H10 : vars_in_subst (L' n1) (ML n1)
H11 : member (map n1 M'1) (ML n1)
H12 : name n1
H13 : {val M'1}
H14 : {tm M'1}
H15 : {L1 n1 |- tm (M M'1)}
============================
{tm M''}
subst_result_closed_tm_alt < apply subst_var_inst to _ H11 H6.
Subgoal 2:
Variables: ML M L1 L' M'1 M''
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst (ML n1)
H3 : {L1 n1, tm n1 |- tm (M n1)}
H6 : app_subst (ML n1) (M n1) M''
H7 : tm_ctx (L1 n1) *
H9 : vars_of_tm_ctx (L1 n1) (L' n1)
H10 : vars_in_subst (L' n1) (ML n1)
H11 : member (map n1 M'1) (ML n1)
H12 : name n1
H13 : {val M'1}
H14 : {tm M'1}
H15 : {L1 n1 |- tm (M M'1)}
H16 : app_subst (ML n1) (M M'1) M''
============================
{tm M''}
subst_result_closed_tm_alt < apply IH to H1 H7 H15 _ _ H16.
Subgoal 2:
Variables: ML M L1 L' M'1 M''
IH : forall ML L M M' Vs, subst ML -> tm_ctx L * -> {L |- tm M} ->
vars_of_tm_ctx L Vs -> vars_in_subst Vs ML -> app_subst ML M M' ->
{tm M'}
H1 : subst (ML n1)
H3 : {L1 n1, tm n1 |- tm (M n1)}
H6 : app_subst (ML n1) (M n1) M''
H7 : tm_ctx (L1 n1) *
H9 : vars_of_tm_ctx (L1 n1) (L' n1)
H10 : vars_in_subst (L' n1) (ML n1)
H11 : member (map n1 M'1) (ML n1)
H12 : name n1
H13 : {val M'1}
H14 : {tm M'1}
H15 : {L1 n1 |- tm (M M'1)}
H16 : app_subst (ML n1) (M M'1) M''
H17 : {tm M''}
============================
{tm M''}
subst_result_closed_tm_alt < search.
Proof completed.
Abella < Define subst' : (list (map tm' tm')) -> prop by
subst' nil;
nabla x, subst' (map x V :: ML) := subst' ML /\ {val' V} /\ {tm' V}.
Abella < Define vars_of_subst' : (list (map tm' tm')) -> (list tm') -> prop by
vars_of_subst' nil nil;
nabla x, vars_of_subst' (map x V :: ML) (x :: L) := vars_of_subst' ML L.
Abella < Theorem app_subst'_exists :
forall ML M, subst' ML -> (exists M', app_subst ML M M').
============================
forall ML M, subst' ML -> (exists M', app_subst ML M M')
app_subst'_exists < induction on 1.
IH : forall ML M, subst' ML * -> (exists M', app_subst ML M M')
============================
forall ML M, subst' ML @ -> (exists M', app_subst ML M M')
app_subst'_exists < intros.
Variables: ML M
IH : forall ML M, subst' ML * -> (exists M', app_subst ML M M')
H1 : subst' ML @
============================
exists M', app_subst ML M M'
app_subst'_exists < case H1.
Subgoal 1:
Variables: M
IH : forall ML M, subst' ML * -> (exists M', app_subst ML M M')
============================
exists M', app_subst nil M M'
Subgoal 2 is:
exists M', app_subst (map n1 V :: ML1) (M n1) M'
app_subst'_exists < search.
Subgoal 2:
Variables: M ML1 V
IH : forall ML M, subst' ML * -> (exists M', app_subst ML M M')
H2 : subst' ML1 *
H3 : {val' V}
H4 : {tm' V}
============================
exists M', app_subst (map n1 V :: ML1) (M n1) M'
app_subst'_exists < apply IH to H2 with M = M V.
Subgoal 2:
Variables: M ML1 V M'
IH : forall ML M, subst' ML * -> (exists M', app_subst ML M M')
H2 : subst' ML1 *
H3 : {val' V}
H4 : {tm' V}
H5 : app_subst ML1 (M V) M'
============================
exists M', app_subst (map n1 V :: ML1) (M n1) M'
app_subst'_exists < search.
Proof completed.
Abella < Theorem subst'_nabla :
forall ML, nabla x, subst' ML -> app_subst ML x x.
============================
forall ML, nabla x, subst' ML -> app_subst ML x x
subst'_nabla < induction on 1.
IH : forall ML, nabla x, subst' ML * -> app_subst ML x x
============================
forall ML, nabla x, subst' ML @ -> app_subst ML x x
subst'_nabla < intros.
Variables: ML
IH : forall ML, nabla x, subst' ML * -> app_subst ML x x
H1 : subst' ML @
============================
app_subst ML n1 n1
subst'_nabla < case H1.
Subgoal 1:
IH : forall ML, nabla x, subst' ML * -> app_subst ML x x
============================
app_subst nil n1 n1
Subgoal 2 is:
app_subst (map n2 V :: ML1) n1 n1
subst'_nabla < search.
Subgoal 2:
Variables: ML1 V
IH : forall ML, nabla x, subst' ML * -> app_subst ML x x
H2 : subst' ML1 *
H3 : {val' V}
H4 : {tm' V}
============================
app_subst (map n2 V :: ML1) n1 n1
subst'_nabla < unfold.
Subgoal 2:
Variables: ML1 V
IH : forall ML, nabla x, subst' ML * -> app_subst ML x x
H2 : subst' ML1 *
H3 : {val' V}
H4 : {tm' V}
============================
app_subst ML1 n1 n1
subst'_nabla < backchain IH.
Proof completed.
Abella < Theorem subst'_result_closed_tm :
forall ML L M M' Vs, tm'_ctx L -> {L |- tm' M} -> vars_of_tm'_ctx L Vs ->
subst' ML -> vars_of_subst' ML Vs -> app_subst ML M M' -> {tm' M'}.
============================
forall ML L M M' Vs, tm'_ctx L -> {L |- tm' M} -> vars_of_tm'_ctx L Vs ->
subst' ML -> vars_of_subst' ML Vs -> app_subst ML M M' -> {tm' M'}
subst'_result_closed_tm < induction on 1.
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
============================
forall ML L M M' Vs, tm'_ctx L @ -> {L |- tm' M} -> vars_of_tm'_ctx L Vs ->
subst' ML -> vars_of_subst' ML Vs -> app_subst ML M M' -> {tm' M'}
subst'_result_closed_tm < intros.
Variables: ML L M M' Vs
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H1 : tm'_ctx L @
H2 : {L |- tm' M}
H3 : vars_of_tm'_ctx L Vs
H4 : subst' ML
H5 : vars_of_subst' ML Vs
H6 : app_subst ML M M'
============================
{tm' M'}
subst'_result_closed_tm < case H1.
Subgoal 1:
Variables: ML M M' Vs
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H2 : {tm' M}
H3 : vars_of_tm'_ctx nil Vs
H4 : subst' ML
H5 : vars_of_subst' ML Vs
H6 : app_subst ML M M'
============================
{tm' M'}
Subgoal 2 is:
{tm' (M' n1)}
subst'_result_closed_tm < case H3.
Subgoal 1:
Variables: ML M M'
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H2 : {tm' M}
H4 : subst' ML
H5 : vars_of_subst' ML nil
H6 : app_subst ML M M'
============================
{tm' M'}
Subgoal 2 is:
{tm' (M' n1)}
subst'_result_closed_tm < case H5.
Subgoal 1:
Variables: M M'
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H2 : {tm' M}
H4 : subst' nil
H6 : app_subst nil M M'
============================
{tm' M'}
Subgoal 2 is:
{tm' (M' n1)}
subst'_result_closed_tm < case H6.
Subgoal 1:
Variables: M'
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H2 : {tm' M'}
H4 : subst' nil
============================
{tm' M'}
Subgoal 2 is:
{tm' (M' n1)}
subst'_result_closed_tm < search.
Subgoal 2:
Variables: ML M M' Vs L1
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H2 : {L1, tm' n1 |- tm' (M n1)}
H3 : vars_of_tm'_ctx (tm' n1 :: L1) (Vs n1)
H4 : subst' (ML n1)
H5 : vars_of_subst' (ML n1) (Vs n1)
H6 : app_subst (ML n1) (M n1) (M' n1)
H7 : tm'_ctx L1 *
============================
{tm' (M' n1)}
subst'_result_closed_tm < case H3.
Subgoal 2:
Variables: ML M M' L1 L'
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H2 : {L1, tm' n1 |- tm' (M n1)}
H4 : subst' (ML n1)
H5 : vars_of_subst' (ML n1) (n1 :: L')
H6 : app_subst (ML n1) (M n1) (M' n1)
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
============================
{tm' (M' n1)}
subst'_result_closed_tm < case H5.
Subgoal 2:
Variables: M M' L1 L' ML1 V
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H2 : {L1, tm' n1 |- tm' (M n1)}
H4 : subst' (map n1 V :: ML1)
H6 : app_subst (map n1 V :: ML1) (M n1) (M' n1)
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
H9 : vars_of_subst' ML1 L'
============================
{tm' (M' n1)}
subst'_result_closed_tm < case H6.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H2 : {L1, tm' n1 |- tm' (M n1)}
H4 : subst' (map n1 V :: ML1)
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
H9 : vars_of_subst' ML1 L'
H10 : app_subst ML1 (M V) M1
============================
{tm' M1}
subst'_result_closed_tm < case H4.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H2 : {L1, tm' n1 |- tm' (M n1)}
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
H9 : vars_of_subst' ML1 L'
H10 : app_subst ML1 (M V) M1
H11 : subst' ML1
H12 : {val' V}
H13 : {tm' V}
============================
{tm' M1}
subst'_result_closed_tm < inst H2 with n1 = V.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H2 : {L1, tm' n1 |- tm' (M n1)}
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
H9 : vars_of_subst' ML1 L'
H10 : app_subst ML1 (M V) M1
H11 : subst' ML1
H12 : {val' V}
H13 : {tm' V}
H14 : {L1, tm' V |- tm' (M V)}
============================
{tm' M1}
subst'_result_closed_tm < cut H14 with H13.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm' M'}
H2 : {L1, tm' n1 |- tm' (M n1)}
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
H9 : vars_of_subst' ML1 L'
H10 : app_subst ML1 (M V) M1
H11 : subst' ML1
H12 : {val' V}
H13 : {tm' V}
H14 : {L1, tm' V |- tm' (M V)}
H15 : {L1 |- tm' (M V)}
============================
{tm' M1}
subst'_result_closed_tm < backchain IH with ML = ML1, L = L1, M = M V.
Proof completed.
Abella < Theorem subst'_result_closed_tm'' :
forall ML L M M' Vs, tm'_ctx L -> {L |- tm'' M} -> vars_of_tm'_ctx L Vs ->
subst' ML -> vars_of_subst' ML Vs -> app_subst ML M M' -> {tm'' M'}.
============================
forall ML L M M' Vs, tm'_ctx L -> {L |- tm'' M} -> vars_of_tm'_ctx L Vs ->
subst' ML -> vars_of_subst' ML Vs -> app_subst ML M M' -> {tm'' M'}
subst'_result_closed_tm'' < induction on 1.
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
============================
forall ML L M M' Vs, tm'_ctx L @ -> {L |- tm'' M} -> vars_of_tm'_ctx L Vs ->
subst' ML -> vars_of_subst' ML Vs -> app_subst ML M M' -> {tm'' M'}
subst'_result_closed_tm'' < intros.
Variables: ML L M M' Vs
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H1 : tm'_ctx L @
H2 : {L |- tm'' M}
H3 : vars_of_tm'_ctx L Vs
H4 : subst' ML
H5 : vars_of_subst' ML Vs
H6 : app_subst ML M M'
============================
{tm'' M'}
subst'_result_closed_tm'' < case H1.
Subgoal 1:
Variables: ML M M' Vs
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H2 : {tm'' M}
H3 : vars_of_tm'_ctx nil Vs
H4 : subst' ML
H5 : vars_of_subst' ML Vs
H6 : app_subst ML M M'
============================
{tm'' M'}
Subgoal 2 is:
{tm'' (M' n1)}
subst'_result_closed_tm'' < case H3.
Subgoal 1:
Variables: ML M M'
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H2 : {tm'' M}
H4 : subst' ML
H5 : vars_of_subst' ML nil
H6 : app_subst ML M M'
============================
{tm'' M'}
Subgoal 2 is:
{tm'' (M' n1)}
subst'_result_closed_tm'' < case H5.
Subgoal 1:
Variables: M M'
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H2 : {tm'' M}
H4 : subst' nil
H6 : app_subst nil M M'
============================
{tm'' M'}
Subgoal 2 is:
{tm'' (M' n1)}
subst'_result_closed_tm'' < case H6.
Subgoal 1:
Variables: M'
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H2 : {tm'' M'}
H4 : subst' nil
============================
{tm'' M'}
Subgoal 2 is:
{tm'' (M' n1)}
subst'_result_closed_tm'' < search.
Subgoal 2:
Variables: ML M M' Vs L1
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H2 : {L1, tm' n1 |- tm'' (M n1)}
H3 : vars_of_tm'_ctx (tm' n1 :: L1) (Vs n1)
H4 : subst' (ML n1)
H5 : vars_of_subst' (ML n1) (Vs n1)
H6 : app_subst (ML n1) (M n1) (M' n1)
H7 : tm'_ctx L1 *
============================
{tm'' (M' n1)}
subst'_result_closed_tm'' < case H3.
Subgoal 2:
Variables: ML M M' L1 L'
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H2 : {L1, tm' n1 |- tm'' (M n1)}
H4 : subst' (ML n1)
H5 : vars_of_subst' (ML n1) (n1 :: L')
H6 : app_subst (ML n1) (M n1) (M' n1)
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
============================
{tm'' (M' n1)}
subst'_result_closed_tm'' < case H5.
Subgoal 2:
Variables: M M' L1 L' ML1 V
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H2 : {L1, tm' n1 |- tm'' (M n1)}
H4 : subst' (map n1 V :: ML1)
H6 : app_subst (map n1 V :: ML1) (M n1) (M' n1)
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
H9 : vars_of_subst' ML1 L'
============================
{tm'' (M' n1)}
subst'_result_closed_tm'' < case H6.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H2 : {L1, tm' n1 |- tm'' (M n1)}
H4 : subst' (map n1 V :: ML1)
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
H9 : vars_of_subst' ML1 L'
H10 : app_subst ML1 (M V) M1
============================
{tm'' M1}
subst'_result_closed_tm'' < case H4.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H2 : {L1, tm' n1 |- tm'' (M n1)}
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
H9 : vars_of_subst' ML1 L'
H10 : app_subst ML1 (M V) M1
H11 : subst' ML1
H12 : {val' V}
H13 : {tm' V}
============================
{tm'' M1}
subst'_result_closed_tm'' < inst H2 with n1 = V.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H2 : {L1, tm' n1 |- tm'' (M n1)}
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
H9 : vars_of_subst' ML1 L'
H10 : app_subst ML1 (M V) M1
H11 : subst' ML1
H12 : {val' V}
H13 : {tm' V}
H14 : {L1, tm' V |- tm'' (M V)}
============================
{tm'' M1}
subst'_result_closed_tm'' < cut H14 with H13.
Subgoal 2:
Variables: M L1 L' ML1 V M1
IH : forall ML L M M' Vs, tm'_ctx L * -> {L |- tm'' M} ->
vars_of_tm'_ctx L Vs -> subst' ML -> vars_of_subst' ML Vs ->
app_subst ML M M' -> {tm'' M'}
H2 : {L1, tm' n1 |- tm'' (M n1)}
H7 : tm'_ctx L1 *
H8 : vars_of_tm'_ctx L1 L'
H9 : vars_of_subst' ML1 L'
H10 : app_subst ML1 (M V) M1
H11 : subst' ML1
H12 : {val' V}
H13 : {tm' V}
H14 : {L1, tm' V |- tm'' (M V)}
H15 : {L1 |- tm'' (M V)}
============================
{tm'' M1}
subst'_result_closed_tm'' < backchain IH with ML = ML1, L = L1, M = M V.
Proof completed.
Abella < Theorem subst'_mem :
forall ML E, subst' ML -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val' V} /\ {tm' V}).
============================
forall ML E, subst' ML -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val' V} /\ {tm' V})
subst'_mem < induction on 1.
IH : forall ML E, subst' ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val' V} /\ {tm' V})
============================
forall ML E, subst' ML @ -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val' V} /\ {tm' V})
subst'_mem < intros.
Variables: ML E
IH : forall ML E, subst' ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val' V} /\ {tm' V})
H1 : subst' ML @
H2 : member E ML
============================
exists X V, E = map X V /\ name X /\ {val' V} /\ {tm' V}
subst'_mem < case H1.
Subgoal 1:
Variables: E
IH : forall ML E, subst' ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val' V} /\ {tm' V})
H2 : member E nil
============================
exists X V, E = map X V /\ name X /\ {val' V} /\ {tm' V}
Subgoal 2 is:
exists X V, E n1 = map X V /\ name X /\ {val' V} /\ {tm' V}
subst'_mem < case H2.
Subgoal 2:
Variables: E ML1 V
IH : forall ML E, subst' ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val' V} /\ {tm' V})
H2 : member (E n1) (map n1 V :: ML1)
H3 : subst' ML1 *
H4 : {val' V}
H5 : {tm' V}
============================
exists X V, E n1 = map X V /\ name X /\ {val' V} /\ {tm' V}
subst'_mem < case H2.
Subgoal 2.1:
Variables: ML1 V
IH : forall ML E, subst' ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val' V} /\ {tm' V})
H3 : subst' ML1 *
H4 : {val' V}
H5 : {tm' V}
============================
exists X V1, map n1 V = map X V1 /\ name X /\ {val' V1} /\ {tm' V1}
Subgoal 2.2 is:
exists X V, E n1 = map X V /\ name X /\ {val' V} /\ {tm' V}
subst'_mem < search.
Subgoal 2.2:
Variables: E ML1 V
IH : forall ML E, subst' ML * -> member E ML ->
(exists X V, E = map X V /\ name X /\ {val' V} /\ {tm' V})
H3 : subst' ML1 *
H4 : {val' V}
H5 : {tm' V}
H6 : member (E n1) ML1
============================
exists X V, E n1 = map X V /\ name X /\ {val' V} /\ {tm' V}
subst'_mem < backchain IH.
Proof completed.
Abella < Theorem subst'_extend :
forall ML V, nabla x, subst' ML -> {tm' V} -> {val' V} ->
subst' (map x V :: ML).
============================
forall ML V, nabla x, subst' ML -> {tm' V} -> {val' V} ->
subst' (map x V :: ML)
subst'_extend < intros.
Variables: ML V
H1 : subst' ML
H2 : {tm' V}
H3 : {val' V}
============================
subst' (map n1 V :: ML)
subst'_extend < unfold.
Subgoal 1:
Variables: ML V
H1 : subst' ML
H2 : {tm' V}
H3 : {val' V}
============================
subst' ML
Subgoal 2 is:
{val' V}
Subgoal 3 is:
{tm' V}
subst'_extend < search.
Subgoal 2:
Variables: ML V
H1 : subst' ML
H2 : {tm' V}
H3 : {val' V}
============================
{val' V}
Subgoal 3 is:
{tm' V}
subst'_extend < search.
Subgoal 3:
Variables: ML V
H1 : subst' ML
H2 : {tm' V}
H3 : {val' V}
============================
{tm' V}
subst'_extend < search.
Proof completed.
Abella < Theorem subst'_closed_tm_eq :
forall M ML M', {tm' M} -> app_subst ML M M' -> M = M'.
============================
forall M ML M', {tm' M} -> app_subst ML M M' -> M = M'
subst'_closed_tm_eq < induction on 2.
IH : forall M ML M', {tm' M} -> app_subst ML M M' * -> M = M'
============================
forall M ML M', {tm' M} -> app_subst ML M M' @ -> M = M'
subst'_closed_tm_eq < intros.
Variables: M ML M'
IH : forall M ML M', {tm' M} -> app_subst ML M M' * -> M = M'
H1 : {tm' M}
H2 : app_subst ML M M' @
============================
M = M'
subst'_closed_tm_eq < case H2.
Subgoal 1:
Variables: M'
IH : forall M ML M', {tm' M} -> app_subst ML M M' * -> M = M'
H1 : {tm' M'}
============================
M' = M'
Subgoal 2 is:
M n1 = M1
subst'_closed_tm_eq < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall M ML M', {tm' M} -> app_subst ML M M' * -> M = M'
H1 : {tm' (M n1)}
H3 : app_subst ML1 (M V) M1 *
============================
M n1 = M1
subst'_closed_tm_eq < apply closed_tm'_prune to H1.
Subgoal 2:
Variables: M1 ML1 V M'1
IH : forall M ML M', {tm' M} -> app_subst ML M M' * -> M = M'
H1 : {tm' M'1}
H3 : app_subst ML1 M'1 M1 *
============================
M'1 = M1
subst'_closed_tm_eq < apply IH to _ H3.
Subgoal 2:
Variables: M1 ML1 V
IH : forall M ML M', {tm' M} -> app_subst ML M M' * -> M = M'
H1 : {tm' M1}
H3 : app_subst ML1 M1 M1 *
============================
M1 = M1
subst'_closed_tm_eq < search.
Proof completed.
Abella < Theorem subst'_closed_tm :
forall M ML, {tm' M} -> subst' ML -> app_subst ML M M.
============================
forall M ML, {tm' M} -> subst' ML -> app_subst ML M M
subst'_closed_tm < induction on 2.
IH : forall M ML, {tm' M} -> subst' ML * -> app_subst ML M M
============================
forall M ML, {tm' M} -> subst' ML @ -> app_subst ML M M
subst'_closed_tm < intros.
Variables: M ML
IH : forall M ML, {tm' M} -> subst' ML * -> app_subst ML M M
H1 : {tm' M}
H2 : subst' ML @
============================
app_subst ML M M
subst'_closed_tm < case H2.
Subgoal 1:
Variables: M
IH : forall M ML, {tm' M} -> subst' ML * -> app_subst ML M M
H1 : {tm' M}
============================
app_subst nil M M
Subgoal 2 is:
app_subst (map n1 V :: ML1) (M n1) (M n1)
subst'_closed_tm < search.
Subgoal 2:
Variables: M ML1 V
IH : forall M ML, {tm' M} -> subst' ML * -> app_subst ML M M
H1 : {tm' (M n1)}
H3 : subst' ML1 *
H4 : {val' V}
H5 : {tm' V}
============================
app_subst (map n1 V :: ML1) (M n1) (M n1)
subst'_closed_tm < apply closed_tm'_prune to H1.
Subgoal 2:
Variables: ML1 V M'
IH : forall M ML, {tm' M} -> subst' ML * -> app_subst ML M M
H1 : {tm' M'}
H3 : subst' ML1 *
H4 : {val' V}
H5 : {tm' V}
============================
app_subst (map n1 V :: ML1) M' M'
subst'_closed_tm < apply IH to H1 H3.
Subgoal 2:
Variables: ML1 V M'
IH : forall M ML, {tm' M} -> subst' ML * -> app_subst ML M M
H1 : {tm' M'}
H3 : subst' ML1 *
H4 : {val' V}
H5 : {tm' V}
H6 : app_subst ML1 M' M'
============================
app_subst (map n1 V :: ML1) M' M'
subst'_closed_tm < search.
Proof completed.
Abella < Theorem subst'_var :
forall V ML X, subst' ML -> member (map X V) ML -> app_subst ML X V.
============================
forall V ML X, subst' ML -> member (map X V) ML -> app_subst ML X V
subst'_var < induction on 2.
IH : forall V ML X, subst' ML -> member (map X V) ML * -> app_subst ML X V
============================
forall V ML X, subst' ML -> member (map X V) ML @ -> app_subst ML X V
subst'_var < intros.
Variables: V ML X
IH : forall V ML X, subst' ML -> member (map X V) ML * -> app_subst ML X V
H1 : subst' ML
H2 : member (map X V) ML @
============================
app_subst ML X V
subst'_var < case H2.
Subgoal 1:
Variables: V X L
IH : forall V ML X, subst' ML -> member (map X V) ML * -> app_subst ML X V
H1 : subst' (map X V :: L)
============================
app_subst (map X V :: L) X V
Subgoal 2 is:
app_subst (B :: L) X V
subst'_var < case H1.
Subgoal 1:
Variables: ML1 V1
IH : forall V ML X, subst' ML -> member (map X V) ML * -> app_subst ML X V
H3 : subst' ML1
H4 : {val' V1}
H5 : {tm' V1}
============================
app_subst (map n1 V1 :: ML1) n1 V1
Subgoal 2 is:
app_subst (B :: L) X V
subst'_var < unfold.
Subgoal 1:
Variables: ML1 V1
IH : forall V ML X, subst' ML -> member (map X V) ML * -> app_subst ML X V
H3 : subst' ML1
H4 : {val' V1}
H5 : {tm' V1}
============================
app_subst ML1 V1 V1
Subgoal 2 is:
app_subst (B :: L) X V
subst'_var < intros.
Subgoal 1:
Variables: ML1 V1
IH : forall V ML X, subst' ML -> member (map X V) ML * -> app_subst ML X V
H3 : subst' ML1
H4 : {val' V1}
H5 : {tm' V1}
============================
app_subst ML1 V1 V1
Subgoal 2 is:
app_subst (B :: L) X V
subst'_var < backchain subst'_closed_tm.
Subgoal 2:
Variables: V X L B
IH : forall V ML X, subst' ML -> member (map X V) ML * -> app_subst ML X V
H1 : subst' (B :: L)
H3 : member (map X V) L *
============================
app_subst (B :: L) X V
subst'_var < case H1.
Subgoal 2:
Variables: V X ML1 V1
IH : forall V ML X, subst' ML -> member (map X V) ML * -> app_subst ML X V
H3 : member (map (X n1) (V n1)) ML1 *
H4 : subst' ML1
H5 : {val' V1}
H6 : {tm' V1}
============================
app_subst (map n1 V1 :: ML1) (X n1) (V n1)
subst'_var < apply member_prune to H3.
Subgoal 2:
Variables: ML1 V1 M'2 M'1
IH : forall V ML X, subst' ML -> member (map X V) ML * -> app_subst ML X V
H3 : member (map M'1 M'2) ML1 *
H4 : subst' ML1
H5 : {val' V1}
H6 : {tm' V1}
============================
app_subst (map n1 V1 :: ML1) M'1 M'2
subst'_var < unfold.
Subgoal 2:
Variables: ML1 V1 M'2 M'1
IH : forall V ML X, subst' ML -> member (map X V) ML * -> app_subst ML X V
H3 : member (map M'1 M'2) ML1 *
H4 : subst' ML1
H5 : {val' V1}
H6 : {tm' V1}
============================
app_subst ML1 M'1 M'2
subst'_var < intros.
Subgoal 2:
Variables: ML1 V1 M'2 M'1
IH : forall V ML X, subst' ML -> member (map X V) ML * -> app_subst ML X V
H3 : member (map M'1 M'2) ML1 *
H4 : subst' ML1
H5 : {val' V1}
H6 : {tm' V1}
============================
app_subst ML1 M'1 M'2
subst'_var < backchain IH.
Proof completed.
Abella < Theorem subst'_var_eq :
forall V ML E X, subst' ML -> member (map X V) ML -> app_subst ML X E -> E =
V.
============================
forall V ML E X, subst' ML -> member (map X V) ML -> app_subst ML X E -> E =
V
subst'_var_eq < intros.
Variables: V ML E X
H1 : subst' ML
H2 : member (map X V) ML
H3 : app_subst ML X E
============================
E = V
subst'_var_eq < apply subst'_var to H1 H2.
Variables: V ML E X
H1 : subst' ML
H2 : member (map X V) ML
H3 : app_subst ML X E
H4 : app_subst ML X V
============================
E = V
subst'_var_eq < apply app_subst_det to H3 H4.
Variables: V ML X
H1 : subst' ML
H2 : member (map X V) ML
H3 : app_subst ML X V
H4 : app_subst ML X V
============================
V = V
subst'_var_eq < search.
Proof completed.
Abella < Theorem subst'_inst :
forall ML M M' V, nabla x, {tm' V} -> app_subst ML (M x) (M' x) ->
app_subst ML (M V) (M' V).
============================
forall ML M M' V, nabla x, {tm' V} -> app_subst ML (M x) (M' x) ->
app_subst ML (M V) (M' V)
subst'_inst < induction on 2.
IH : forall ML M M' V, nabla x, {tm' V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
============================
forall ML M M' V, nabla x, {tm' V} -> app_subst ML (M x) (M' x) @ ->
app_subst ML (M V) (M' V)
subst'_inst < intros.
Variables: ML M M' V
IH : forall ML M M' V, nabla x, {tm' V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm' V}
H2 : app_subst ML (M n1) (M' n1) @
============================
app_subst ML (M V) (M' V)
subst'_inst < case H2.
Subgoal 1:
Variables: M' V
IH : forall ML M M' V, nabla x, {tm' V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm' V}
============================
app_subst nil (M' V) (M' V)
Subgoal 2 is:
app_subst (map n2 ML2 :: ML3) (M n2 (V n2)) (M2 (V n2))
subst'_inst < search.
Subgoal 2:
Variables: M V M2 ML3 ML2
IH : forall ML M M' V, nabla x, {tm' V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm' (V n2)}
H3 : app_subst ML3 (M ML2 n1) (M2 n1) *
============================
app_subst (map n2 ML2 :: ML3) (M n2 (V n2)) (M2 (V n2))
subst'_inst < apply closed_tm'_prune to H1.
Subgoal 2:
Variables: M M2 ML3 ML2 M'1
IH : forall ML M M' V, nabla x, {tm' V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm' M'1}
H3 : app_subst ML3 (M ML2 n1) (M2 n1) *
============================
app_subst (map n2 ML2 :: ML3) (M n2 M'1) (M2 M'1)
subst'_inst < unfold.
Subgoal 2:
Variables: M M2 ML3 ML2 M'1
IH : forall ML M M' V, nabla x, {tm' V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm' M'1}
H3 : app_subst ML3 (M ML2 n1) (M2 n1) *
============================
app_subst ML3 (M ML2 M'1) (M2 M'1)
subst'_inst < apply IH to H1 H3.
Subgoal 2:
Variables: M M2 ML3 ML2 M'1
IH : forall ML M M' V, nabla x, {tm' V} -> app_subst ML (M x) (M' x) * ->
app_subst ML (M V) (M' V)
H1 : {tm' M'1}
H3 : app_subst ML3 (M ML2 n1) (M2 n1) *
H4 : app_subst ML3 (M ML2 M'1) (M2 M'1)
============================
app_subst ML3 (M ML2 M'1) (M2 M'1)
subst'_inst < search.
Proof completed.
Abella < Theorem explct_meta_subst'_comm :
forall ML M E V, nabla n, {tm' V} -> app_subst ML (M n) (E n) ->
app_subst (map n V :: ML) (M n) (E V).
============================
forall ML M E V, nabla n, {tm' V} -> app_subst ML (M n) (E n) ->
app_subst (map n V :: ML) (M n) (E V)
explct_meta_subst'_comm < intros.
Variables: ML M E V
H1 : {tm' V}
H2 : app_subst ML (M n1) (E n1)
============================
app_subst (map n1 V :: ML) (M n1) (E V)
explct_meta_subst'_comm < unfold.
Variables: ML M E V
H1 : {tm' V}
H2 : app_subst ML (M n1) (E n1)
============================
app_subst ML (M V) (E V)
explct_meta_subst'_comm < intros.
Variables: ML M E V
H1 : {tm' V}
H2 : app_subst ML (M n1) (E n1)
============================
app_subst ML (M V) (E V)
explct_meta_subst'_comm < backchain subst'_inst with M = M, M' = E, x = n1.
Proof completed.
Abella < Theorem subst'_closed_tm''_eq :
forall M ML M', {tm'' M} -> app_subst ML M M' -> M = M'.
============================
forall M ML M', {tm'' M} -> app_subst ML M M' -> M = M'
subst'_closed_tm''_eq < induction on 2.
IH : forall M ML M', {tm'' M} -> app_subst ML M M' * -> M = M'
============================
forall M ML M', {tm'' M} -> app_subst ML M M' @ -> M = M'
subst'_closed_tm''_eq < intros.
Variables: M ML M'
IH : forall M ML M', {tm'' M} -> app_subst ML M M' * -> M = M'
H1 : {tm'' M}
H2 : app_subst ML M M' @
============================
M = M'
subst'_closed_tm''_eq < case H2.
Subgoal 1:
Variables: M'
IH : forall M ML M', {tm'' M} -> app_subst ML M M' * -> M = M'
H1 : {tm'' M'}
============================
M' = M'
Subgoal 2 is:
M n1 = M1
subst'_closed_tm''_eq < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall M ML M', {tm'' M} -> app_subst ML M M' * -> M = M'
H1 : {tm'' (M n1)}
H3 : app_subst ML1 (M V) M1 *
============================
M n1 = M1
subst'_closed_tm''_eq < apply closed_tm''_prune to H1.
Subgoal 2:
Variables: M1 ML1 V M'1
IH : forall M ML M', {tm'' M} -> app_subst ML M M' * -> M = M'
H1 : {tm'' M'1}
H3 : app_subst ML1 M'1 M1 *
============================
M'1 = M1
subst'_closed_tm''_eq < apply IH to _ H3.
Subgoal 2:
Variables: M1 ML1 V
IH : forall M ML M', {tm'' M} -> app_subst ML M M' * -> M = M'
H1 : {tm'' M1}
H3 : app_subst ML1 M1 M1 *
============================
M1 = M1
subst'_closed_tm''_eq < search.
Proof completed.
Abella < Theorem subst'_closed_tm''_body_eq :
forall M ML M', {tm''_body M} -> app_subst ML M M' -> M = M'.
============================
forall M ML M', {tm''_body M} -> app_subst ML M M' -> M = M'
subst'_closed_tm''_body_eq < induction on 2.
IH : forall M ML M', {tm''_body M} -> app_subst ML M M' * -> M = M'
============================
forall M ML M', {tm''_body M} -> app_subst ML M M' @ -> M = M'
subst'_closed_tm''_body_eq < intros.
Variables: M ML M'
IH : forall M ML M', {tm''_body M} -> app_subst ML M M' * -> M = M'
H1 : {tm''_body M}
H2 : app_subst ML M M' @
============================
M = M'
subst'_closed_tm''_body_eq < case H2.
Subgoal 1:
Variables: M'
IH : forall M ML M', {tm''_body M} -> app_subst ML M M' * -> M = M'
H1 : {tm''_body M'}
============================
M' = M'
Subgoal 2 is:
M n1 = M1
subst'_closed_tm''_body_eq < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall M ML M', {tm''_body M} -> app_subst ML M M' * -> M = M'
H1 : {tm''_body (M n1)}
H3 : app_subst ML1 (M V) M1 *
============================
M n1 = M1
subst'_closed_tm''_body_eq < apply closed_tm''_body_prune to H1.
Subgoal 2:
Variables: M1 ML1 V M'1
IH : forall M ML M', {tm''_body M} -> app_subst ML M M' * -> M = M'
H1 : {tm''_body M'1}
H3 : app_subst ML1 M'1 M1 *
============================
M'1 = M1
subst'_closed_tm''_body_eq < apply IH to _ H3.
Subgoal 2:
Variables: M1 ML1 V
IH : forall M ML M', {tm''_body M} -> app_subst ML M M' * -> M = M'
H1 : {tm''_body M1}
H3 : app_subst ML1 M1 M1 *
============================
M1 = M1
subst'_closed_tm''_body_eq < search.
Proof completed.
Abella < Theorem app_subst'_pred_comm :
forall ML M M', app_subst ML (pred' M) M' ->
(exists M'', M' = pred' M'' /\ app_subst ML M M'').
============================
forall ML M M', app_subst ML (pred' M) M' ->
(exists M'', M' = pred' M'' /\ app_subst ML M M'')
app_subst'_pred_comm < induction on 1.
IH : forall ML M M', app_subst ML (pred' M) M' * ->
(exists M'', M' = pred' M'' /\ app_subst ML M M'')
============================
forall ML M M', app_subst ML (pred' M) M' @ ->
(exists M'', M' = pred' M'' /\ app_subst ML M M'')
app_subst'_pred_comm < intros.
Variables: ML M M'
IH : forall ML M M', app_subst ML (pred' M) M' * ->
(exists M'', M' = pred' M'' /\ app_subst ML M M'')
H1 : app_subst ML (pred' M) M' @
============================
exists M'', M' = pred' M'' /\ app_subst ML M M''
app_subst'_pred_comm < case H1.
Subgoal 1:
Variables: M
IH : forall ML M M', app_subst ML (pred' M) M' * ->
(exists M'', M' = pred' M'' /\ app_subst ML M M'')
============================
exists M'', pred' M = pred' M'' /\ app_subst nil M M''
Subgoal 2 is:
exists M'', M1 = pred' M'' /\ app_subst (map n1 V :: ML1) (M n1) M''
app_subst'_pred_comm < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML (pred' M) M' * ->
(exists M'', M' = pred' M'' /\ app_subst ML M M'')
H2 : app_subst ML1 (pred' (M V)) M1 *
============================
exists M'', M1 = pred' M'' /\ app_subst (map n1 V :: ML1) (M n1) M''
app_subst'_pred_comm < apply IH to H2.
Subgoal 2:
Variables: M ML1 V M''
IH : forall ML M M', app_subst ML (pred' M) M' * ->
(exists M'', M' = pred' M'' /\ app_subst ML M M'')
H2 : app_subst ML1 (pred' (M V)) (pred' M'') *
H3 : app_subst ML1 (M V) M''
============================
exists M''1, pred' M'' = pred' M''1 /\
app_subst (map n1 V :: ML1) (M n1) M''1
app_subst'_pred_comm < search.
Proof completed.
Abella < Theorem app_subst'_ifz_comm :
forall ML M M1 M2 M3, app_subst ML (ifz' M M1 M2) M3 ->
(exists M' M1' M2', M3 = ifz' M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2').
============================
forall ML M M1 M2 M3, app_subst ML (ifz' M M1 M2) M3 ->
(exists M' M1' M2', M3 = ifz' M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
app_subst'_ifz_comm < induction on 1.
IH : forall ML M M1 M2 M3, app_subst ML (ifz' M M1 M2) M3 * ->
(exists M' M1' M2', M3 = ifz' M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
============================
forall ML M M1 M2 M3, app_subst ML (ifz' M M1 M2) M3 @ ->
(exists M' M1' M2', M3 = ifz' M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
app_subst'_ifz_comm < intros.
Variables: ML M M1 M2 M3
IH : forall ML M M1 M2 M3, app_subst ML (ifz' M M1 M2) M3 * ->
(exists M' M1' M2', M3 = ifz' M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
H1 : app_subst ML (ifz' M M1 M2) M3 @
============================
exists M' M1' M2', M3 = ifz' M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2'
app_subst'_ifz_comm < case H1.
Subgoal 1:
Variables: M M1 M2
IH : forall ML M M1 M2 M3, app_subst ML (ifz' M M1 M2) M3 * ->
(exists M' M1' M2', M3 = ifz' M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
============================
exists M' M1' M2', ifz' M M1 M2 = ifz' M' M1' M2' /\ app_subst nil M M' /\
app_subst nil M1 M1' /\ app_subst nil M2 M2'
Subgoal 2 is:
exists M' M1' M2', M4 = ifz' M' M1' M2' /\
app_subst (map n1 V :: ML1) (M n1) M' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst'_ifz_comm < search.
Subgoal 2:
Variables: M M1 M2 M4 ML1 V
IH : forall ML M M1 M2 M3, app_subst ML (ifz' M M1 M2) M3 * ->
(exists M' M1' M2', M3 = ifz' M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
H2 : app_subst ML1 (ifz' (M V) (M1 V) (M2 V)) M4 *
============================
exists M' M1' M2', M4 = ifz' M' M1' M2' /\
app_subst (map n1 V :: ML1) (M n1) M' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst'_ifz_comm < apply IH to H2.
Subgoal 2:
Variables: M M1 M2 ML1 V M' M1' M2'
IH : forall ML M M1 M2 M3, app_subst ML (ifz' M M1 M2) M3 * ->
(exists M' M1' M2', M3 = ifz' M' M1' M2' /\ app_subst ML M M' /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
H2 : app_subst ML1 (ifz' (M V) (M1 V) (M2 V)) (ifz' M' M1' M2') *
H3 : app_subst ML1 (M V) M'
H4 : app_subst ML1 (M1 V) M1'
H5 : app_subst ML1 (M2 V) M2'
============================
exists M'1 M1'1 M2'1, ifz' M' M1' M2' = ifz' M'1 M1'1 M2'1 /\
app_subst (map n1 V :: ML1) (M n1) M'1 /\
app_subst (map n1 V :: ML1) (M1 n1) M1'1 /\
app_subst (map n1 V :: ML1) (M2 n1) M2'1
app_subst'_ifz_comm < search.
Proof completed.
Abella < Theorem app_subst'_let_comm :
forall ML M R M', app_subst ML (let' M R) M' ->
(exists M1 R1, M' = let' M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x))).
============================
forall ML M R M', app_subst ML (let' M R) M' ->
(exists M1 R1, M' = let' M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
app_subst'_let_comm < induction on 1.
IH : forall ML M R M', app_subst ML (let' M R) M' * ->
(exists M1 R1, M' = let' M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
============================
forall ML M R M', app_subst ML (let' M R) M' @ ->
(exists M1 R1, M' = let' M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
app_subst'_let_comm < intros.
Variables: ML M R M'
IH : forall ML M R M', app_subst ML (let' M R) M' * ->
(exists M1 R1, M' = let' M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
H1 : app_subst ML (let' M R) M' @
============================
exists M1 R1, M' = let' M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x))
app_subst'_let_comm < case H1.
Subgoal 1:
Variables: M R
IH : forall ML M R M', app_subst ML (let' M R) M' * ->
(exists M1 R1, M' = let' M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
============================
exists M1 R1, let' M R = let' M1 R1 /\ app_subst nil M M1 /\
(nabla x, app_subst nil (R x) (R1 x))
Subgoal 2 is:
exists M2 R1, M1 = let' M2 R1 /\ app_subst (map n1 V :: ML1) (M n1) M2 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R1 x))
app_subst'_let_comm < search.
Subgoal 2:
Variables: M R M1 ML1 V
IH : forall ML M R M', app_subst ML (let' M R) M' * ->
(exists M1 R1, M' = let' M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
H2 : app_subst ML1 (let' (M V) (R V)) M1 *
============================
exists M2 R1, M1 = let' M2 R1 /\ app_subst (map n1 V :: ML1) (M n1) M2 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R1 x))
app_subst'_let_comm < apply IH to H2.
Subgoal 2:
Variables: M R ML1 V M2 R1
IH : forall ML M R M', app_subst ML (let' M R) M' * ->
(exists M1 R1, M' = let' M1 R1 /\ app_subst ML M M1 /\
(nabla x, app_subst ML (R x) (R1 x)))
H2 : app_subst ML1 (let' (M V) (R V)) (let' M2 R1) *
H3 : app_subst ML1 (M V) M2
H4 : app_subst ML1 (R V n1) (R1 n1)
============================
exists M1 R2, let' M2 R1 = let' M1 R2 /\
app_subst (map n1 V :: ML1) (M n1) M1 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R2 x))
app_subst'_let_comm < search.
Proof completed.
Abella < Theorem app_subst'_clos_comm :
forall ML F M M', app_subst ML (clos' F M) M' ->
(exists F' M1', M' = clos' F' M1' /\ app_subst ML F F' /\
app_subst ML M M1').
============================
forall ML F M M', app_subst ML (clos' F M) M' ->
(exists F' M1', M' = clos' F' M1' /\ app_subst ML F F' /\
app_subst ML M M1')
app_subst'_clos_comm < induction on 1.
IH : forall ML F M M', app_subst ML (clos' F M) M' * ->
(exists F' M1', M' = clos' F' M1' /\ app_subst ML F F' /\
app_subst ML M M1')
============================
forall ML F M M', app_subst ML (clos' F M) M' @ ->
(exists F' M1', M' = clos' F' M1' /\ app_subst ML F F' /\
app_subst ML M M1')
app_subst'_clos_comm < intros.
Variables: ML F M M'
IH : forall ML F M M', app_subst ML (clos' F M) M' * ->
(exists F' M1', M' = clos' F' M1' /\ app_subst ML F F' /\
app_subst ML M M1')
H1 : app_subst ML (clos' F M) M' @
============================
exists F' M1', M' = clos' F' M1' /\ app_subst ML F F' /\ app_subst ML M M1'
app_subst'_clos_comm < case H1.
Subgoal 1:
Variables: F M
IH : forall ML F M M', app_subst ML (clos' F M) M' * ->
(exists F' M1', M' = clos' F' M1' /\ app_subst ML F F' /\
app_subst ML M M1')
============================
exists F' M1', clos' F M = clos' F' M1' /\ app_subst nil F F' /\
app_subst nil M M1'
Subgoal 2 is:
exists F' M1', M1 = clos' F' M1' /\ app_subst (map n1 V :: ML1) (F n1) F' /\
app_subst (map n1 V :: ML1) (M n1) M1'
app_subst'_clos_comm < search.
Subgoal 2:
Variables: F M M1 ML1 V
IH : forall ML F M M', app_subst ML (clos' F M) M' * ->
(exists F' M1', M' = clos' F' M1' /\ app_subst ML F F' /\
app_subst ML M M1')
H2 : app_subst ML1 (clos' (F V) (M V)) M1 *
============================
exists F' M1', M1 = clos' F' M1' /\ app_subst (map n1 V :: ML1) (F n1) F' /\
app_subst (map n1 V :: ML1) (M n1) M1'
app_subst'_clos_comm < apply IH to H2.
Subgoal 2:
Variables: F M ML1 V F' M1'
IH : forall ML F M M', app_subst ML (clos' F M) M' * ->
(exists F' M1', M' = clos' F' M1' /\ app_subst ML F F' /\
app_subst ML M M1')
H2 : app_subst ML1 (clos' (F V) (M V)) (clos' F' M1') *
H3 : app_subst ML1 (F V) F'
H4 : app_subst ML1 (M V) M1'
============================
exists F'1 M1'1, clos' F' M1' = clos' F'1 M1'1 /\
app_subst (map n1 V :: ML1) (F n1) F'1 /\
app_subst (map n1 V :: ML1) (M n1) M1'1
app_subst'_clos_comm < search.
Proof completed.
Abella < Theorem app_subst'_open_comm :
forall ML M1 M2 M', app_subst ML
(open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) M' ->
(exists M1' M2', M' = open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\
app_subst ML M1 M1' /\ app_subst ML M2 M2').
============================
forall ML M1 M2 M', app_subst ML
(open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) M' ->
(exists M1' M2', M' = open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
app_subst'_open_comm < induction on 1.
IH : forall ML M1 M2 M', app_subst ML
(open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) M' * ->
(exists M1' M2', M' =
open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
============================
forall ML M1 M2 M', app_subst ML
(open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) M' @ ->
(exists M1' M2', M' = open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
app_subst'_open_comm < intros.
Variables: ML M1 M2 M'
IH : forall ML M1 M2 M', app_subst ML
(open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) M' * ->
(exists M1' M2', M' =
open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
H1 : app_subst ML (open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) M' @
============================
exists M1' M2', M' = open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\
app_subst ML M1 M1' /\ app_subst ML M2 M2'
app_subst'_open_comm < case H1.
Subgoal 1:
Variables: M1 M2
IH : forall ML M1 M2 M', app_subst ML
(open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) M' * ->
(exists M1' M2', M' =
open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
============================
exists M1' M2', open' M1 (f\e\app' f (pair' M1 (pair' M2 e))) =
open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\ app_subst nil M1 M1' /\
app_subst nil M2 M2'
Subgoal 2 is:
exists M1' M2', M = open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst'_open_comm < search.
Subgoal 2:
Variables: M1 M2 M ML1 V
IH : forall ML M1 M2 M', app_subst ML
(open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) M' * ->
(exists M1' M2', M' =
open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
H2 : app_subst ML1
(open' (M1 V) (f\e\app' f (pair' (M1 V) (pair' (M2 V) e)))) M *
============================
exists M1' M2', M = open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst'_open_comm < apply IH to H2.
Subgoal 2:
Variables: M1 M2 ML1 V M1' M2'
IH : forall ML M1 M2 M', app_subst ML
(open' M1 (f\e\app' f (pair' M1 (pair' M2 e)))) M' * ->
(exists M1' M2', M' =
open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) /\
app_subst ML M1 M1' /\ app_subst ML M2 M2')
H2 : app_subst ML1
(open' (M1 V) (f\e\app' f (pair' (M1 V) (pair' (M2 V) e))))
(open' M1' (f\e\app' f (pair' M1' (pair' M2' e)))) *
H3 : app_subst ML1 (M1 V) M1'
H4 : app_subst ML1 (M2 V) M2'
============================
exists M1'1 M2'1, open' M1' (f\e\app' f (pair' M1' (pair' M2' e))) =
open' M1'1 (f\e\app' f (pair' M1'1 (pair' M2'1 e))) /\
app_subst (map n1 V :: ML1) (M1 n1) M1'1 /\
app_subst (map n1 V :: ML1) (M2 n1) M2'1
app_subst'_open_comm < search.
Proof completed.
Abella < Theorem app_subst'_plus_comm :
forall ML M1 M2 M', app_subst ML (plus' M1 M2) M' ->
(exists M1' M2', M' = plus' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2').
============================
forall ML M1 M2 M', app_subst ML (plus' M1 M2) M' ->
(exists M1' M2', M' = plus' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst'_plus_comm < induction on 1.
IH : forall ML M1 M2 M', app_subst ML (plus' M1 M2) M' * ->
(exists M1' M2', M' = plus' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
forall ML M1 M2 M', app_subst ML (plus' M1 M2) M' @ ->
(exists M1' M2', M' = plus' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst'_plus_comm < intros.
Variables: ML M1 M2 M'
IH : forall ML M1 M2 M', app_subst ML (plus' M1 M2) M' * ->
(exists M1' M2', M' = plus' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H1 : app_subst ML (plus' M1 M2) M' @
============================
exists M1' M2', M' = plus' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2'
app_subst'_plus_comm < case H1.
Subgoal 1:
Variables: M1 M2
IH : forall ML M1 M2 M', app_subst ML (plus' M1 M2) M' * ->
(exists M1' M2', M' = plus' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
exists M1' M2', plus' M1 M2 = plus' M1' M2' /\ app_subst nil M1 M1' /\
app_subst nil M2 M2'
Subgoal 2 is:
exists M1' M2', M = plus' M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst'_plus_comm < search.
Subgoal 2:
Variables: M1 M2 M ML1 V
IH : forall ML M1 M2 M', app_subst ML (plus' M1 M2) M' * ->
(exists M1' M2', M' = plus' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (plus' (M1 V) (M2 V)) M *
============================
exists M1' M2', M = plus' M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst'_plus_comm < apply IH to H2.
Subgoal 2:
Variables: M1 M2 ML1 V M1' M2'
IH : forall ML M1 M2 M', app_subst ML (plus' M1 M2) M' * ->
(exists M1' M2', M' = plus' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (plus' (M1 V) (M2 V)) (plus' M1' M2') *
H3 : app_subst ML1 (M1 V) M1'
H4 : app_subst ML1 (M2 V) M2'
============================
exists M1'1 M2'1, plus' M1' M2' = plus' M1'1 M2'1 /\
app_subst (map n1 V :: ML1) (M1 n1) M1'1 /\
app_subst (map n1 V :: ML1) (M2 n1) M2'1
app_subst'_plus_comm < search.
Proof completed.
Abella < Theorem app_subst'_pair_comm :
forall ML M1 M2 M', app_subst ML (pair' M1 M2) M' ->
(exists M1' M2', M' = pair' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2').
============================
forall ML M1 M2 M', app_subst ML (pair' M1 M2) M' ->
(exists M1' M2', M' = pair' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst'_pair_comm < induction on 1.
IH : forall ML M1 M2 M', app_subst ML (pair' M1 M2) M' * ->
(exists M1' M2', M' = pair' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
forall ML M1 M2 M', app_subst ML (pair' M1 M2) M' @ ->
(exists M1' M2', M' = pair' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst'_pair_comm < intros.
Variables: ML M1 M2 M'
IH : forall ML M1 M2 M', app_subst ML (pair' M1 M2) M' * ->
(exists M1' M2', M' = pair' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H1 : app_subst ML (pair' M1 M2) M' @
============================
exists M1' M2', M' = pair' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2'
app_subst'_pair_comm < case H1.
Subgoal 1:
Variables: M1 M2
IH : forall ML M1 M2 M', app_subst ML (pair' M1 M2) M' * ->
(exists M1' M2', M' = pair' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
exists M1' M2', pair' M1 M2 = pair' M1' M2' /\ app_subst nil M1 M1' /\
app_subst nil M2 M2'
Subgoal 2 is:
exists M1' M2', M = pair' M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst'_pair_comm < search.
Subgoal 2:
Variables: M1 M2 M ML1 V
IH : forall ML M1 M2 M', app_subst ML (pair' M1 M2) M' * ->
(exists M1' M2', M' = pair' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (pair' (M1 V) (M2 V)) M *
============================
exists M1' M2', M = pair' M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst'_pair_comm < apply IH to H2.
Subgoal 2:
Variables: M1 M2 ML1 V M1' M2'
IH : forall ML M1 M2 M', app_subst ML (pair' M1 M2) M' * ->
(exists M1' M2', M' = pair' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (pair' (M1 V) (M2 V)) (pair' M1' M2') *
H3 : app_subst ML1 (M1 V) M1'
H4 : app_subst ML1 (M2 V) M2'
============================
exists M1'1 M2'1, pair' M1' M2' = pair' M1'1 M2'1 /\
app_subst (map n1 V :: ML1) (M1 n1) M1'1 /\
app_subst (map n1 V :: ML1) (M2 n1) M2'1
app_subst'_pair_comm < search.
Proof completed.
Abella < Theorem app_subst'_fst_comm :
forall ML M M', app_subst ML (fst' M) M' ->
(exists M1', M' = fst' M1' /\ app_subst ML M M1').
============================
forall ML M M', app_subst ML (fst' M) M' ->
(exists M1', M' = fst' M1' /\ app_subst ML M M1')
app_subst'_fst_comm < induction on 1.
IH : forall ML M M', app_subst ML (fst' M) M' * ->
(exists M1', M' = fst' M1' /\ app_subst ML M M1')
============================
forall ML M M', app_subst ML (fst' M) M' @ ->
(exists M1', M' = fst' M1' /\ app_subst ML M M1')
app_subst'_fst_comm < intros.
Variables: ML M M'
IH : forall ML M M', app_subst ML (fst' M) M' * ->
(exists M1', M' = fst' M1' /\ app_subst ML M M1')
H1 : app_subst ML (fst' M) M' @
============================
exists M1', M' = fst' M1' /\ app_subst ML M M1'
app_subst'_fst_comm < case H1.
Subgoal 1:
Variables: M
IH : forall ML M M', app_subst ML (fst' M) M' * ->
(exists M1', M' = fst' M1' /\ app_subst ML M M1')
============================
exists M1', fst' M = fst' M1' /\ app_subst nil M M1'
Subgoal 2 is:
exists M1', M1 = fst' M1' /\ app_subst (map n1 V :: ML1) (M n1) M1'
app_subst'_fst_comm < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML (fst' M) M' * ->
(exists M1', M' = fst' M1' /\ app_subst ML M M1')
H2 : app_subst ML1 (fst' (M V)) M1 *
============================
exists M1', M1 = fst' M1' /\ app_subst (map n1 V :: ML1) (M n1) M1'
app_subst'_fst_comm < apply IH to H2.
Subgoal 2:
Variables: M ML1 V M1'
IH : forall ML M M', app_subst ML (fst' M) M' * ->
(exists M1', M' = fst' M1' /\ app_subst ML M M1')
H2 : app_subst ML1 (fst' (M V)) (fst' M1') *
H3 : app_subst ML1 (M V) M1'
============================
exists M1'1, fst' M1' = fst' M1'1 /\ app_subst (map n1 V :: ML1) (M n1) M1'1
app_subst'_fst_comm < search.
Proof completed.
Abella < Theorem app_subst'_snd_comm :
forall ML M M', app_subst ML (snd' M) M' ->
(exists M1', M' = snd' M1' /\ app_subst ML M M1').
============================
forall ML M M', app_subst ML (snd' M) M' ->
(exists M1', M' = snd' M1' /\ app_subst ML M M1')
app_subst'_snd_comm < induction on 1.
IH : forall ML M M', app_subst ML (snd' M) M' * ->
(exists M1', M' = snd' M1' /\ app_subst ML M M1')
============================
forall ML M M', app_subst ML (snd' M) M' @ ->
(exists M1', M' = snd' M1' /\ app_subst ML M M1')
app_subst'_snd_comm < intros.
Variables: ML M M'
IH : forall ML M M', app_subst ML (snd' M) M' * ->
(exists M1', M' = snd' M1' /\ app_subst ML M M1')
H1 : app_subst ML (snd' M) M' @
============================
exists M1', M' = snd' M1' /\ app_subst ML M M1'
app_subst'_snd_comm < case H1.
Subgoal 1:
Variables: M
IH : forall ML M M', app_subst ML (snd' M) M' * ->
(exists M1', M' = snd' M1' /\ app_subst ML M M1')
============================
exists M1', snd' M = snd' M1' /\ app_subst nil M M1'
Subgoal 2 is:
exists M1', M1 = snd' M1' /\ app_subst (map n1 V :: ML1) (M n1) M1'
app_subst'_snd_comm < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML (snd' M) M' * ->
(exists M1', M' = snd' M1' /\ app_subst ML M M1')
H2 : app_subst ML1 (snd' (M V)) M1 *
============================
exists M1', M1 = snd' M1' /\ app_subst (map n1 V :: ML1) (M n1) M1'
app_subst'_snd_comm < apply IH to H2.
Subgoal 2:
Variables: M ML1 V M1'
IH : forall ML M M', app_subst ML (snd' M) M' * ->
(exists M1', M' = snd' M1' /\ app_subst ML M M1')
H2 : app_subst ML1 (snd' (M V)) (snd' M1') *
H3 : app_subst ML1 (M V) M1'
============================
exists M1'1, snd' M1' = snd' M1'1 /\ app_subst (map n1 V :: ML1) (M n1) M1'1
app_subst'_snd_comm < search.
Proof completed.
Abella < Theorem app_subst'_abs_comm :
forall ML R M', app_subst ML (abs' R) M' ->
(exists R', M' = abs' R' /\ (nabla x, app_subst ML (R x) (R' x))).
============================
forall ML R M', app_subst ML (abs' R) M' ->
(exists R', M' = abs' R' /\ (nabla x, app_subst ML (R x) (R' x)))
app_subst'_abs_comm < induction on 1.
IH : forall ML R M', app_subst ML (abs' R) M' * ->
(exists R', M' = abs' R' /\ (nabla x, app_subst ML (R x) (R' x)))
============================
forall ML R M', app_subst ML (abs' R) M' @ ->
(exists R', M' = abs' R' /\ (nabla x, app_subst ML (R x) (R' x)))
app_subst'_abs_comm < intros.
Variables: ML R M'
IH : forall ML R M', app_subst ML (abs' R) M' * ->
(exists R', M' = abs' R' /\ (nabla x, app_subst ML (R x) (R' x)))
H1 : app_subst ML (abs' R) M' @
============================
exists R', M' = abs' R' /\ (nabla x, app_subst ML (R x) (R' x))
app_subst'_abs_comm < case H1.
Subgoal 1:
Variables: R
IH : forall ML R M', app_subst ML (abs' R) M' * ->
(exists R', M' = abs' R' /\ (nabla x, app_subst ML (R x) (R' x)))
============================
exists R', abs' R = abs' R' /\ (nabla x, app_subst nil (R x) (R' x))
Subgoal 2 is:
exists R', M = abs' R' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x))
app_subst'_abs_comm < search.
Subgoal 2:
Variables: R M ML1 V
IH : forall ML R M', app_subst ML (abs' R) M' * ->
(exists R', M' = abs' R' /\ (nabla x, app_subst ML (R x) (R' x)))
H2 : app_subst ML1 (abs' (R V)) M *
============================
exists R', M = abs' R' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x))
app_subst'_abs_comm < apply IH to H2.
Subgoal 2:
Variables: R ML1 V R'
IH : forall ML R M', app_subst ML (abs' R) M' * ->
(exists R', M' = abs' R' /\ (nabla x, app_subst ML (R x) (R' x)))
H2 : app_subst ML1 (abs' (R V)) (abs' R') *
H3 : app_subst ML1 (R V n1) (R' n1)
============================
exists R'1, abs' R' = abs' R'1 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R'1 x))
app_subst'_abs_comm < search.
Proof completed.
Abella < Theorem app_subst'_unit_comm :
forall ML M', app_subst ML unit' M' -> M' = unit'.
============================
forall ML M', app_subst ML unit' M' -> M' = unit'
app_subst'_unit_comm < induction on 1.
IH : forall ML M', app_subst ML unit' M' * -> M' = unit'
============================
forall ML M', app_subst ML unit' M' @ -> M' = unit'
app_subst'_unit_comm < intros.
Variables: ML M'
IH : forall ML M', app_subst ML unit' M' * -> M' = unit'
H1 : app_subst ML unit' M' @
============================
M' = unit'
app_subst'_unit_comm < case H1.
Subgoal 1:
IH : forall ML M', app_subst ML unit' M' * -> M' = unit'
============================
unit' = unit'
Subgoal 2 is:
M = unit'
app_subst'_unit_comm < search.
Subgoal 2:
Variables: M ML1 V
IH : forall ML M', app_subst ML unit' M' * -> M' = unit'
H2 : app_subst ML1 unit' M *
============================
M = unit'
app_subst'_unit_comm < apply IH to H2.
Subgoal 2:
Variables: ML1 V
IH : forall ML M', app_subst ML unit' M' * -> M' = unit'
H2 : app_subst ML1 unit' unit' *
============================
unit' = unit'
app_subst'_unit_comm < search.
Proof completed.
Abella < Theorem app_subst'_app_comm :
forall ML M1 M2 M', app_subst ML (app' M1 M2) M' ->
(exists M1' M2', M' = app' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2').
============================
forall ML M1 M2 M', app_subst ML (app' M1 M2) M' ->
(exists M1' M2', M' = app' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst'_app_comm < induction on 1.
IH : forall ML M1 M2 M', app_subst ML (app' M1 M2) M' * ->
(exists M1' M2', M' = app' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
forall ML M1 M2 M', app_subst ML (app' M1 M2) M' @ ->
(exists M1' M2', M' = app' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
app_subst'_app_comm < intros.
Variables: ML M1 M2 M'
IH : forall ML M1 M2 M', app_subst ML (app' M1 M2) M' * ->
(exists M1' M2', M' = app' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H1 : app_subst ML (app' M1 M2) M' @
============================
exists M1' M2', M' = app' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2'
app_subst'_app_comm < case H1.
Subgoal 1:
Variables: M1 M2
IH : forall ML M1 M2 M', app_subst ML (app' M1 M2) M' * ->
(exists M1' M2', M' = app' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
============================
exists M1' M2', app' M1 M2 = app' M1' M2' /\ app_subst nil M1 M1' /\
app_subst nil M2 M2'
Subgoal 2 is:
exists M1' M2', M = app' M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst'_app_comm < search.
Subgoal 2:
Variables: M1 M2 M ML1 V
IH : forall ML M1 M2 M', app_subst ML (app' M1 M2) M' * ->
(exists M1' M2', M' = app' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (app' (M1 V) (M2 V)) M *
============================
exists M1' M2', M = app' M1' M2' /\
app_subst (map n1 V :: ML1) (M1 n1) M1' /\
app_subst (map n1 V :: ML1) (M2 n1) M2'
app_subst'_app_comm < apply IH to H2.
Subgoal 2:
Variables: M1 M2 ML1 V M1' M2'
IH : forall ML M1 M2 M', app_subst ML (app' M1 M2) M' * ->
(exists M1' M2', M' = app' M1' M2' /\ app_subst ML M1 M1' /\
app_subst ML M2 M2')
H2 : app_subst ML1 (app' (M1 V) (M2 V)) (app' M1' M2') *
H3 : app_subst ML1 (M1 V) M1'
H4 : app_subst ML1 (M2 V) M2'
============================
exists M1'1 M2'1, app' M1' M2' = app' M1'1 M2'1 /\
app_subst (map n1 V :: ML1) (M1 n1) M1'1 /\
app_subst (map n1 V :: ML1) (M2 n1) M2'1
app_subst'_app_comm < search.
Proof completed.
Abella < Theorem app_subst'_meta_app_comm :
forall ML R M M1, app_subst ML (R M) M1 ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M').
============================
forall ML R M M1, app_subst ML (R M) M1 ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M')
app_subst'_meta_app_comm < induction on 1.
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M')
============================
forall ML R M M1, app_subst ML (R M) M1 @ ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M')
app_subst'_meta_app_comm < intros.
Variables: ML R M M1
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M')
H1 : app_subst ML (R M) M1 @
============================
exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M'
app_subst'_meta_app_comm < case H1.
Subgoal 1:
Variables: R M
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M')
============================
exists R' M', R M = R' M' /\ (nabla x, app_subst nil (R x) (R' x)) /\
app_subst nil M M'
Subgoal 2 is:
exists R' M', M2 = R' M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
app_subst (map n1 V :: ML1) (M n1) M'
app_subst'_meta_app_comm < exists R.
Subgoal 1:
Variables: R M
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M')
============================
exists M', R M = R M' /\ (nabla x, app_subst nil (R x) (R x)) /\
app_subst nil M M'
Subgoal 2 is:
exists R' M', M2 = R' M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
app_subst (map n1 V :: ML1) (M n1) M'
app_subst'_meta_app_comm < exists M.
Subgoal 1:
Variables: R M
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M')
============================
R M = R M /\ (nabla x, app_subst nil (R x) (R x)) /\ app_subst nil M M
Subgoal 2 is:
exists R' M', M2 = R' M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
app_subst (map n1 V :: ML1) (M n1) M'
app_subst'_meta_app_comm < search.
Subgoal 2:
Variables: R M M2 ML1 V
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M')
H2 : app_subst ML1 (R V (M V)) M2 *
============================
exists R' M', M2 = R' M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
app_subst (map n1 V :: ML1) (M n1) M'
app_subst'_meta_app_comm < apply IH to H2 with R = R V, M = M V.
Subgoal 2:
Variables: R M ML1 V R' M'
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M')
H2 : app_subst ML1 (R V (M V)) (R' M') *
H3 : app_subst ML1 (R V n1) (R' n1)
H4 : app_subst ML1 (M V) M'
============================
exists R'1 M'1, R' M' = R'1 M'1 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R'1 x)) /\
app_subst (map n1 V :: ML1) (M n1) M'1
app_subst'_meta_app_comm < exists R'.
Subgoal 2:
Variables: R M ML1 V R' M'
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M')
H2 : app_subst ML1 (R V (M V)) (R' M') *
H3 : app_subst ML1 (R V n1) (R' n1)
H4 : app_subst ML1 (M V) M'
============================
exists M'1, R' M' = R' M'1 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
app_subst (map n1 V :: ML1) (M n1) M'1
app_subst'_meta_app_comm < exists M'.
Subgoal 2:
Variables: R M ML1 V R' M'
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
app_subst ML M M')
H2 : app_subst ML1 (R V (M V)) (R' M') *
H3 : app_subst ML1 (R V n1) (R' n1)
H4 : app_subst ML1 (M V) M'
============================
R' M' = R' M' /\ (nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
app_subst (map n1 V :: ML1) (M n1) M'
app_subst'_meta_app_comm < search.
Proof completed.
Abella < Theorem app_subst'_meta_app_abs_comm :
forall ML R M M1, app_subst ML (R M) M1 ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y))).
============================
forall ML R M M1, app_subst ML (R M) M1 ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y)))
app_subst'_meta_app_abs_comm < induction on 1.
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y)))
============================
forall ML R M M1, app_subst ML (R M) M1 @ ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y)))
app_subst'_meta_app_abs_comm < intros.
Variables: ML R M M1
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y)))
H1 : app_subst ML (R M) M1 @
============================
exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y))
app_subst'_meta_app_abs_comm < case H1.
Subgoal 1:
Variables: R M
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y)))
============================
exists R' M', R M = R' M' /\ (nabla x, app_subst nil (R x) (R' x)) /\
(nabla y, app_subst nil (M y) (M' y))
Subgoal 2 is:
exists R' M', M2 = R' M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
(nabla y, app_subst (map n1 V :: ML1) (M n1 y) (M' y))
app_subst'_meta_app_abs_comm < exists R.
Subgoal 1:
Variables: R M
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y)))
============================
exists M', R M = R M' /\ (nabla x, app_subst nil (R x) (R x)) /\
(nabla y, app_subst nil (M y) (M' y))
Subgoal 2 is:
exists R' M', M2 = R' M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
(nabla y, app_subst (map n1 V :: ML1) (M n1 y) (M' y))
app_subst'_meta_app_abs_comm < exists M.
Subgoal 1:
Variables: R M
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y)))
============================
R M = R M /\ (nabla x, app_subst nil (R x) (R x)) /\
(nabla y, app_subst nil (M y) (M y))
Subgoal 2 is:
exists R' M', M2 = R' M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
(nabla y, app_subst (map n1 V :: ML1) (M n1 y) (M' y))
app_subst'_meta_app_abs_comm < search.
Subgoal 2:
Variables: R M M2 ML1 V
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y)))
H2 : app_subst ML1 (R V (M V)) M2 *
============================
exists R' M', M2 = R' M' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
(nabla y, app_subst (map n1 V :: ML1) (M n1 y) (M' y))
app_subst'_meta_app_abs_comm < apply IH to H2 with R = R V, M = M V.
Subgoal 2:
Variables: R M ML1 V R' M'
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y)))
H2 : app_subst ML1 (R V (M V)) (R' M') *
H3 : app_subst ML1 (R V n1) (R' n1)
H4 : app_subst ML1 (M V n1) (M' n1)
============================
exists R'1 M'1, R' M' = R'1 M'1 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R'1 x)) /\
(nabla y, app_subst (map n1 V :: ML1) (M n1 y) (M'1 y))
app_subst'_meta_app_abs_comm < exists R'.
Subgoal 2:
Variables: R M ML1 V R' M'
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y)))
H2 : app_subst ML1 (R V (M V)) (R' M') *
H3 : app_subst ML1 (R V n1) (R' n1)
H4 : app_subst ML1 (M V n1) (M' n1)
============================
exists M'1, R' M' = R' M'1 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
(nabla y, app_subst (map n1 V :: ML1) (M n1 y) (M'1 y))
app_subst'_meta_app_abs_comm < exists M'.
Subgoal 2:
Variables: R M ML1 V R' M'
IH : forall ML R M M1, app_subst ML (R M) M1 * ->
(exists R' M', M1 = R' M' /\ (nabla x, app_subst ML (R x) (R' x)) /\
(nabla y, app_subst ML (M y) (M' y)))
H2 : app_subst ML1 (R V (M V)) (R' M') *
H3 : app_subst ML1 (R V n1) (R' n1)
H4 : app_subst ML1 (M V n1) (M' n1)
============================
R' M' = R' M' /\ (nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x)) /\
(nabla y, app_subst (map n1 V :: ML1) (M n1 y) (M' y))
app_subst'_meta_app_abs_comm < search.
Proof completed.
Abella < Theorem app_subst'_hbase_comm :
forall ML M P, app_subst ML (hbase M) P ->
(exists M', P = hbase M' /\ app_subst ML M M').
============================
forall ML M P, app_subst ML (hbase M) P ->
(exists M', P = hbase M' /\ app_subst ML M M')
app_subst'_hbase_comm < induction on 1.
IH : forall ML M P, app_subst ML (hbase M) P * ->
(exists M', P = hbase M' /\ app_subst ML M M')
============================
forall ML M P, app_subst ML (hbase M) P @ ->
(exists M', P = hbase M' /\ app_subst ML M M')
app_subst'_hbase_comm < intros.
Variables: ML M P
IH : forall ML M P, app_subst ML (hbase M) P * ->
(exists M', P = hbase M' /\ app_subst ML M M')
H1 : app_subst ML (hbase M) P @
============================
exists M', P = hbase M' /\ app_subst ML M M'
app_subst'_hbase_comm < case H1.
Subgoal 1:
Variables: M
IH : forall ML M P, app_subst ML (hbase M) P * ->
(exists M', P = hbase M' /\ app_subst ML M M')
============================
exists M', hbase M = hbase M' /\ app_subst nil M M'
Subgoal 2 is:
exists M', M1 = hbase M' /\ app_subst (map n1 V :: ML1) (M n1) M'
app_subst'_hbase_comm < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M P, app_subst ML (hbase M) P * ->
(exists M', P = hbase M' /\ app_subst ML M M')
H2 : app_subst ML1 (hbase (M V)) M1 *
============================
exists M', M1 = hbase M' /\ app_subst (map n1 V :: ML1) (M n1) M'
app_subst'_hbase_comm < apply IH to H2.
Subgoal 2:
Variables: M ML1 V M'
IH : forall ML M P, app_subst ML (hbase M) P * ->
(exists M', P = hbase M' /\ app_subst ML M M')
H2 : app_subst ML1 (hbase (M V)) (hbase M') *
H3 : app_subst ML1 (M V) M'
============================
exists M'1, hbase M' = hbase M'1 /\ app_subst (map n1 V :: ML1) (M n1) M'1
app_subst'_hbase_comm < search.
Proof completed.
Abella < Theorem app_subst'_habs_comm :
forall ML R P, app_subst ML (habs R) P ->
(exists R', P = habs R' /\ (nabla x, app_subst ML (R x) (R' x))).
============================
forall ML R P, app_subst ML (habs R) P ->
(exists R', P = habs R' /\ (nabla x, app_subst ML (R x) (R' x)))
app_subst'_habs_comm < induction on 1.
IH : forall ML R P, app_subst ML (habs R) P * ->
(exists R', P = habs R' /\ (nabla x, app_subst ML (R x) (R' x)))
============================
forall ML R P, app_subst ML (habs R) P @ ->
(exists R', P = habs R' /\ (nabla x, app_subst ML (R x) (R' x)))
app_subst'_habs_comm < intros.
Variables: ML R P
IH : forall ML R P, app_subst ML (habs R) P * ->
(exists R', P = habs R' /\ (nabla x, app_subst ML (R x) (R' x)))
H1 : app_subst ML (habs R) P @
============================
exists R', P = habs R' /\ (nabla x, app_subst ML (R x) (R' x))
app_subst'_habs_comm < case H1.
Subgoal 1:
Variables: R
IH : forall ML R P, app_subst ML (habs R) P * ->
(exists R', P = habs R' /\ (nabla x, app_subst ML (R x) (R' x)))
============================
exists R', habs R = habs R' /\ (nabla x, app_subst nil (R x) (R' x))
Subgoal 2 is:
exists R', M = habs R' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x))
app_subst'_habs_comm < search.
Subgoal 2:
Variables: R M ML1 V
IH : forall ML R P, app_subst ML (habs R) P * ->
(exists R', P = habs R' /\ (nabla x, app_subst ML (R x) (R' x)))
H2 : app_subst ML1 (habs (R V)) M *
============================
exists R', M = habs R' /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R' x))
app_subst'_habs_comm < apply IH to H2.
Subgoal 2:
Variables: R ML1 V R'
IH : forall ML R P, app_subst ML (habs R) P * ->
(exists R', P = habs R' /\ (nabla x, app_subst ML (R x) (R' x)))
H2 : app_subst ML1 (habs (R V)) (habs R') *
H3 : app_subst ML1 (R V n1) (R' n1)
============================
exists R'1, habs R' = habs R'1 /\
(nabla x, app_subst (map n1 V :: ML1) (R n1 x) (R'1 x))
app_subst'_habs_comm < search.
Proof completed.
Abella < Theorem app_subst'_htm_comm :
forall ML FE FE' M M', app_subst ML (htm FE M) (htm FE' M') ->
app_subst_list ML FE FE' /\ app_subst ML M M'.
============================
forall ML FE FE' M M', app_subst ML (htm FE M) (htm FE' M') ->
app_subst_list ML FE FE' /\ app_subst ML M M'
app_subst'_htm_comm < induction on 1.
IH : forall ML FE FE' M M', app_subst ML (htm FE M) (htm FE' M') * ->
app_subst_list ML FE FE' /\ app_subst ML M M'
============================
forall ML FE FE' M M', app_subst ML (htm FE M) (htm FE' M') @ ->
app_subst_list ML FE FE' /\ app_subst ML M M'
app_subst'_htm_comm < intros.
Variables: ML FE FE' M M'
IH : forall ML FE FE' M M', app_subst ML (htm FE M) (htm FE' M') * ->
app_subst_list ML FE FE' /\ app_subst ML M M'
H1 : app_subst ML (htm FE M) (htm FE' M') @
============================
app_subst_list ML FE FE' /\ app_subst ML M M'
app_subst'_htm_comm < case H1.
Subgoal 1:
Variables: FE' M'
IH : forall ML FE FE' M M', app_subst ML (htm FE M) (htm FE' M') * ->
app_subst_list ML FE FE' /\ app_subst ML M M'
============================
app_subst_list nil FE' FE' /\ app_subst nil M' M'
Subgoal 2 is:
app_subst_list (map n1 V :: ML1) (FE n1) M2 /\
app_subst (map n1 V :: ML1) (M n1) M3
app_subst'_htm_comm < search.
Subgoal 2:
Variables: FE M M3 M2 ML1 V
IH : forall ML FE FE' M M', app_subst ML (htm FE M) (htm FE' M') * ->
app_subst_list ML FE FE' /\ app_subst ML M M'
H2 : app_subst ML1 (htm (FE V) (M V)) (htm M2 M3) *
============================
app_subst_list (map n1 V :: ML1) (FE n1) M2 /\
app_subst (map n1 V :: ML1) (M n1) M3
app_subst'_htm_comm < apply IH to H2.
Subgoal 2:
Variables: FE M M3 M2 ML1 V
IH : forall ML FE FE' M M', app_subst ML (htm FE M) (htm FE' M') * ->
app_subst_list ML FE FE' /\ app_subst ML M M'
H2 : app_subst ML1 (htm (FE V) (M V)) (htm M2 M3) *
H3 : app_subst_list ML1 (FE V) M2
H4 : app_subst ML1 (M V) M3
============================
app_subst_list (map n1 V :: ML1) (FE n1) M2 /\
app_subst (map n1 V :: ML1) (M n1) M3
app_subst'_htm_comm < search.
Proof completed.
Abella < Theorem app_subst'_pair_compose :
forall ML M1 M2 M1' M2', app_subst ML M1 M1' -> app_subst ML M2 M2' ->
app_subst ML (pair' M1 M2) (pair' M1' M2').
============================
forall ML M1 M2 M1' M2', app_subst ML M1 M1' -> app_subst ML M2 M2' ->
app_subst ML (pair' M1 M2) (pair' M1' M2')
app_subst'_pair_compose < induction on 1.
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair' M1 M2) (pair' M1' M2')
============================
forall ML M1 M2 M1' M2', app_subst ML M1 M1' @ -> app_subst ML M2 M2' ->
app_subst ML (pair' M1 M2) (pair' M1' M2')
app_subst'_pair_compose < intros.
Variables: ML M1 M2 M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair' M1 M2) (pair' M1' M2')
H1 : app_subst ML M1 M1' @
H2 : app_subst ML M2 M2'
============================
app_subst ML (pair' M1 M2) (pair' M1' M2')
app_subst'_pair_compose < case H1.
Subgoal 1:
Variables: M2 M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair' M1 M2) (pair' M1' M2')
H2 : app_subst nil M2 M2'
============================
app_subst nil (pair' M1' M2) (pair' M1' M2')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (pair' (M1 n1) (M2 n1)) (pair' M (M2' n1))
app_subst'_pair_compose < case H2.
Subgoal 1:
Variables: M1' M2'
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair' M1 M2) (pair' M1' M2')
============================
app_subst nil (pair' M1' M2') (pair' M1' M2')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (pair' (M1 n1) (M2 n1)) (pair' M (M2' n1))
app_subst'_pair_compose < search.
Subgoal 2:
Variables: M1 M2 M2' M ML1 V
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair' M1 M2) (pair' M1' M2')
H2 : app_subst (map n1 V :: ML1) (M2 n1) (M2' n1)
H3 : app_subst ML1 (M1 V) M *
============================
app_subst (map n1 V :: ML1) (pair' (M1 n1) (M2 n1)) (pair' M (M2' n1))
app_subst'_pair_compose < case H2.
Subgoal 2:
Variables: M1 M2 M ML1 V M3
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair' M1 M2) (pair' M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V) M3
============================
app_subst (map n1 V :: ML1) (pair' (M1 n1) (M2 n1)) (pair' M M3)
app_subst'_pair_compose < unfold.
Subgoal 2:
Variables: M1 M2 M ML1 V M3
IH : forall ML M1 M2 M1' M2', app_subst ML M1 M1' * -> app_subst ML M2 M2' ->
app_subst ML (pair' M1 M2) (pair' M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V) M3
============================
app_subst ML1 (pair' (M1 V) (M2 V)) (pair' M M3)
app_subst'_pair_compose < backchain IH.
Proof completed.
Abella < Theorem app_subst'_abs_compose :
forall ML R R', nabla x, app_subst ML (R x) (R' x) ->
app_subst ML (abs' R) (abs' R').
============================
forall ML R R', nabla x, app_subst ML (R x) (R' x) ->
app_subst ML (abs' R) (abs' R')
app_subst'_abs_compose < induction on 1.
IH : forall ML R R', nabla x, app_subst ML (R x) (R' x) * ->
app_subst ML (abs' R) (abs' R')
============================
forall ML R R', nabla x, app_subst ML (R x) (R' x) @ ->
app_subst ML (abs' R) (abs' R')
app_subst'_abs_compose < intros.
Variables: ML R R'
IH : forall ML R R', nabla x, app_subst ML (R x) (R' x) * ->
app_subst ML (abs' R) (abs' R')
H1 : app_subst ML (R n1) (R' n1) @
============================
app_subst ML (abs' R) (abs' R')
app_subst'_abs_compose < case H1.
Subgoal 1:
Variables: R'
IH : forall ML R R', nabla x, app_subst ML (R x) (R' x) * ->
app_subst ML (abs' R) (abs' R')
============================
app_subst nil (abs' (z1\R' z1)) (abs' R')
Subgoal 2 is:
app_subst (map n2 ML2 :: ML3) (abs' (R n2)) (abs' (z2\M1 z2))
app_subst'_abs_compose < search.
Subgoal 2:
Variables: R M1 ML3 ML2
IH : forall ML R R', nabla x, app_subst ML (R x) (R' x) * ->
app_subst ML (abs' R) (abs' R')
H2 : app_subst ML3 (R ML2 n1) (M1 n1) *
============================
app_subst (map n2 ML2 :: ML3) (abs' (R n2)) (abs' (z2\M1 z2))
app_subst'_abs_compose < apply IH to H2.
Subgoal 2:
Variables: R M1 ML3 ML2
IH : forall ML R R', nabla x, app_subst ML (R x) (R' x) * ->
app_subst ML (abs' R) (abs' R')
H2 : app_subst ML3 (R ML2 n1) (M1 n1) *
H3 : app_subst ML3 (abs' (z2\R ML2 z2)) (abs' (z2\M1 z2))
============================
app_subst (map n2 ML2 :: ML3) (abs' (R n2)) (abs' (z2\M1 z2))
app_subst'_abs_compose < search.
Proof completed.
Abella < Theorem app_subst'_let_compose :
forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let' M1 M2) (let' M1' M2').
============================
forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let' M1 M2) (let' M1' M2')
app_subst'_let_compose < induction on 1.
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) ->
app_subst ML (let' M1 M2) (let' M1' M2')
============================
forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' @ ->
app_subst ML (M2 x) (M2' x) -> app_subst ML (let' M1 M2) (let' M1' M2')
app_subst'_let_compose < intros.
Variables: ML M1 M2 M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) ->
app_subst ML (let' M1 M2) (let' M1' M2')
H1 : app_subst ML M1 M1' @
H2 : app_subst ML (M2 n1) (M2' n1)
============================
app_subst ML (let' M1 M2) (let' M1' M2')
app_subst'_let_compose < case H1.
Subgoal 1:
Variables: M2 M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) ->
app_subst ML (let' M1 M2) (let' M1' M2')
H2 : app_subst nil (M2 n1) (M2' n1)
============================
app_subst nil (let' M1' M2) (let' M1' M2')
Subgoal 2 is:
app_subst (map n2 V :: ML1) (let' (M1 n2) (M2 n2)) (let' M (M2' n2))
app_subst'_let_compose < case H2.
Subgoal 1:
Variables: M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) ->
app_subst ML (let' M1 M2) (let' M1' M2')
============================
app_subst nil (let' M1' (z1\M2' z1)) (let' M1' M2')
Subgoal 2 is:
app_subst (map n2 V :: ML1) (let' (M1 n2) (M2 n2)) (let' M (M2' n2))
app_subst'_let_compose < search.
Subgoal 2:
Variables: M1 M2 M2' M ML1 V
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) ->
app_subst ML (let' M1 M2) (let' M1' M2')
H2 : app_subst (map n2 V :: ML1) (M2 n2 n1) (M2' n2 n1)
H3 : app_subst ML1 (M1 V) M *
============================
app_subst (map n2 V :: ML1) (let' (M1 n2) (M2 n2)) (let' M (M2' n2))
app_subst'_let_compose < case H2.
Subgoal 2:
Variables: M1 M2 M ML1 V M4
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) ->
app_subst ML (let' M1 M2) (let' M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V n1) (M4 n1)
============================
app_subst (map n2 V :: ML1) (let' (M1 n2) (M2 n2)) (let' M (z2\M4 z2))
app_subst'_let_compose < unfold.
Subgoal 2:
Variables: M1 M2 M ML1 V M4
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' * ->
app_subst ML (M2 x) (M2' x) ->
app_subst ML (let' M1 M2) (let' M1' M2')
H3 : app_subst ML1 (M1 V) M *
H4 : app_subst ML1 (M2 V n1) (M4 n1)
============================
app_subst ML1 (let' (M1 V) (M2 V)) (let' M (z2\M4 z2))
app_subst'_let_compose < backchain IH with x = n1.
Proof completed.
Abella < Theorem app_subst'_hbase_compose :
forall ML M M', app_subst ML M M' -> app_subst ML (hbase M) (hbase M').
============================
forall ML M M', app_subst ML M M' -> app_subst ML (hbase M) (hbase M')
app_subst'_hbase_compose < induction on 1.
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (hbase M) (hbase M')
============================
forall ML M M', app_subst ML M M' @ -> app_subst ML (hbase M) (hbase M')
app_subst'_hbase_compose < intros.
Variables: ML M M'
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (hbase M) (hbase M')
H1 : app_subst ML M M' @
============================
app_subst ML (hbase M) (hbase M')
app_subst'_hbase_compose < case H1.
Subgoal 1:
Variables: M'
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (hbase M) (hbase M')
============================
app_subst nil (hbase M') (hbase M')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (hbase (M n1)) (hbase M1)
app_subst'_hbase_compose < search.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (hbase M) (hbase M')
H2 : app_subst ML1 (M V) M1 *
============================
app_subst (map n1 V :: ML1) (hbase (M n1)) (hbase M1)
app_subst'_hbase_compose < unfold.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (hbase M) (hbase M')
H2 : app_subst ML1 (M V) M1 *
============================
app_subst ML1 (hbase (M V)) (hbase M1)
app_subst'_hbase_compose < apply IH to H2.
Subgoal 2:
Variables: M M1 ML1 V
IH : forall ML M M', app_subst ML M M' * -> app_subst ML (hbase M) (hbase M')
H2 : app_subst ML1 (M V) M1 *
H3 : app_subst ML1 (hbase (M V)) (hbase M1)
============================
app_subst ML1 (hbase (M V)) (hbase M1)
app_subst'_hbase_compose < search.
Proof completed.
Abella < Theorem app_subst'_habs_compose :
forall ML R R', nabla x, app_subst ML (R x) (R' x) ->
app_subst ML (habs R) (habs R').
============================
forall ML R R', nabla x, app_subst ML (R x) (R' x) ->
app_subst ML (habs R) (habs R')
app_subst'_habs_compose < induction on 1.
IH : forall ML R R', nabla x, app_subst ML (R x) (R' x) * ->
app_subst ML (habs R) (habs R')
============================
forall ML R R', nabla x, app_subst ML (R x) (R' x) @ ->
app_subst ML (habs R) (habs R')
app_subst'_habs_compose < intros.
Variables: ML R R'
IH : forall ML R R', nabla x, app_subst ML (R x) (R' x) * ->
app_subst ML (habs R) (habs R')
H1 : app_subst ML (R n1) (R' n1) @
============================
app_subst ML (habs R) (habs R')
app_subst'_habs_compose < case H1.
Subgoal 1:
Variables: R'
IH : forall ML R R', nabla x, app_subst ML (R x) (R' x) * ->
app_subst ML (habs R) (habs R')
============================
app_subst nil (habs (z1\R' z1)) (habs R')
Subgoal 2 is:
app_subst (map n2 ML2 :: ML3) (habs (R n2)) (habs (z2\M1 z2))
app_subst'_habs_compose < search.
Subgoal 2:
Variables: R M1 ML3 ML2
IH : forall ML R R', nabla x, app_subst ML (R x) (R' x) * ->
app_subst ML (habs R) (habs R')
H2 : app_subst ML3 (R ML2 n1) (M1 n1) *
============================
app_subst (map n2 ML2 :: ML3) (habs (R n2)) (habs (z2\M1 z2))
app_subst'_habs_compose < unfold.
Subgoal 2:
Variables: R M1 ML3 ML2
IH : forall ML R R', nabla x, app_subst ML (R x) (R' x) * ->
app_subst ML (habs R) (habs R')
H2 : app_subst ML3 (R ML2 n1) (M1 n1) *
============================
app_subst ML3 (habs (R ML2)) (habs (z2\M1 z2))
app_subst'_habs_compose < apply IH to H2.
Subgoal 2:
Variables: R M1 ML3 ML2
IH : forall ML R R', nabla x, app_subst ML (R x) (R' x) * ->
app_subst ML (habs R) (habs R')
H2 : app_subst ML3 (R ML2 n1) (M1 n1) *
H3 : app_subst ML3 (habs (z2\R ML2 z2)) (habs (z2\M1 z2))
============================
app_subst ML3 (habs (R ML2)) (habs (z2\M1 z2))
app_subst'_habs_compose < search.
Proof completed.
Abella < Theorem app_subst'_htm_compose :
forall ML L L' M M', app_subst_list ML L L' -> app_subst ML M M' ->
app_subst ML (htm L M) (htm L' M').
============================
forall ML L L' M M', app_subst_list ML L L' -> app_subst ML M M' ->
app_subst ML (htm L M) (htm L' M')
app_subst'_htm_compose < induction on 1.
IH : forall ML L L' M M', app_subst_list ML L L' * -> app_subst ML M M' ->
app_subst ML (htm L M) (htm L' M')
============================
forall ML L L' M M', app_subst_list ML L L' @ -> app_subst ML M M' ->
app_subst ML (htm L M) (htm L' M')
app_subst'_htm_compose < intros.
Variables: ML L L' M M'
IH : forall ML L L' M M', app_subst_list ML L L' * -> app_subst ML M M' ->
app_subst ML (htm L M) (htm L' M')
H1 : app_subst_list ML L L' @
H2 : app_subst ML M M'
============================
app_subst ML (htm L M) (htm L' M')
app_subst'_htm_compose < case H1.
Subgoal 1:
Variables: L' M M'
IH : forall ML L L' M M', app_subst_list ML L L' * -> app_subst ML M M' ->
app_subst ML (htm L M) (htm L' M')
H2 : app_subst nil M M'
============================
app_subst nil (htm L' M) (htm L' M')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (htm (L n1) (M n1)) (htm L'1 (M' n1))
app_subst'_htm_compose < case H2.
Subgoal 1:
Variables: L' M'
IH : forall ML L L' M M', app_subst_list ML L L' * -> app_subst ML M M' ->
app_subst ML (htm L M) (htm L' M')
============================
app_subst nil (htm L' M') (htm L' M')
Subgoal 2 is:
app_subst (map n1 V :: ML1) (htm (L n1) (M n1)) (htm L'1 (M' n1))
app_subst'_htm_compose < search.
Subgoal 2:
Variables: L M M' L'1 ML1 V
IH : forall ML L L' M M', app_subst_list ML L L' * -> app_subst ML M M' ->
app_subst ML (htm L M) (htm L' M')
H2 : app_subst (map n1 V :: ML1) (M n1) (M' n1)
H3 : app_subst_list ML1 (L V) L'1 *
============================
app_subst (map n1 V :: ML1) (htm (L n1) (M n1)) (htm L'1 (M' n1))
app_subst'_htm_compose < case H2.
Subgoal 2:
Variables: L M L'1 ML1 V M1
IH : forall ML L L' M M', app_subst_list ML L L' * -> app_subst ML M M' ->
app_subst ML (htm L M) (htm L' M')
H3 : app_subst_list ML1 (L V) L'1 *
H4 : app_subst ML1 (M V) M1
============================
app_subst (map n1 V :: ML1) (htm (L n1) (M n1)) (htm L'1 M1)
app_subst'_htm_compose < apply IH to H3 H4.
Subgoal 2:
Variables: L M L'1 ML1 V M1
IH : forall ML L L' M M', app_subst_list ML L L' * -> app_subst ML M M' ->
app_subst ML (htm L M) (htm L' M')
H3 : app_subst_list ML1 (L V) L'1 *
H4 : app_subst ML1 (M V) M1
H5 : app_subst ML1 (htm (L V) (M V)) (htm L'1 M1)
============================
app_subst (map n1 V :: ML1) (htm (L n1) (M n1)) (htm L'1 M1)
app_subst'_htm_compose < search.
Proof completed.
Abella < Theorem app_subst'_list_nil1 :
forall ML, subst' ML -> app_subst_list ML nil nil.
============================
forall ML, subst' ML -> app_subst_list ML nil nil
app_subst'_list_nil1 < induction on 1.
IH : forall ML, subst' ML * -> app_subst_list ML nil nil
============================
forall ML, subst' ML @ -> app_subst_list ML nil nil
app_subst'_list_nil1 < intros.
Variables: ML
IH : forall ML, subst' ML * -> app_subst_list ML nil nil
H1 : subst' ML @
============================
app_subst_list ML nil nil
app_subst'_list_nil1 < case H1.
Subgoal 1:
IH : forall ML, subst' ML * -> app_subst_list ML nil nil
============================
app_subst_list nil nil nil
Subgoal 2 is:
app_subst_list (map n1 V :: ML1) nil nil
app_subst'_list_nil1 < search.
Subgoal 2:
Variables: ML1 V
IH : forall ML, subst' ML * -> app_subst_list ML nil nil
H2 : subst' ML1 *
H3 : {val' V}
H4 : {tm' V}
============================
app_subst_list (map n1 V :: ML1) nil nil
app_subst'_list_nil1 < apply IH to H2.
Subgoal 2:
Variables: ML1 V
IH : forall ML, subst' ML * -> app_subst_list ML nil nil
H2 : subst' ML1 *
H3 : {val' V}
H4 : {tm' V}
H5 : app_subst_list ML1 nil nil
============================
app_subst_list (map n1 V :: ML1) nil nil
app_subst'_list_nil1 < search.
Proof completed.
Abella < Theorem app_subst'_list_nil2 :
forall ML L, is_list L -> app_subst_list ML L nil -> L = nil.
============================
forall ML L, is_list L -> app_subst_list ML L nil -> L = nil
app_subst'_list_nil2 < induction on 2.
IH : forall ML L, is_list L -> app_subst_list ML L nil * -> L = nil
============================
forall ML L, is_list L -> app_subst_list ML L nil @ -> L = nil
app_subst'_list_nil2 < intros.
Variables: ML L
IH : forall ML L, is_list L -> app_subst_list ML L nil * -> L = nil
H1 : is_list L
H2 : app_subst_list ML L nil @
============================
L = nil
app_subst'_list_nil2 < case H2.
Subgoal 1:
IH : forall ML L, is_list L -> app_subst_list ML L nil * -> L = nil
H1 : is_list nil
============================
nil = nil
Subgoal 2 is:
L n1 = nil
app_subst'_list_nil2 < search.
Subgoal 2:
Variables: L ML1 V
IH : forall ML L, is_list L -> app_subst_list ML L nil * -> L = nil
H1 : is_list (L n1)
H3 : app_subst_list ML1 (L V) nil *
============================
L n1 = nil
app_subst'_list_nil2 < case H1.
Subgoal 2.1:
Variables: ML1 V
IH : forall ML L, is_list L -> app_subst_list ML L nil * -> L = nil
H3 : app_subst_list ML1 nil nil *
============================
nil = nil
Subgoal 2.2 is:
X n1 :: L1 n1 = nil
app_subst'_list_nil2 < search.
Subgoal 2.2:
Variables: ML1 V L1 X
IH : forall ML L, is_list L -> app_subst_list ML L nil * -> L = nil
H3 : app_subst_list ML1 (X V :: L1 V) nil *
H4 : is_list (L1 n1)
============================
X n1 :: L1 n1 = nil
app_subst'_list_nil2 < apply is_list_inst to H4 with V = V.
Subgoal 2.2:
Variables: ML1 V L1 X
IH : forall ML L, is_list L -> app_subst_list ML L nil * -> L = nil
H3 : app_subst_list ML1 (X V :: L1 V) nil *
H4 : is_list (L1 n1)
H5 : is_list (L1 V)
============================
X n1 :: L1 n1 = nil
app_subst'_list_nil2 < apply IH to _ H3.
Proof completed.
Abella <