Welcome to Abella 2.0.5-dev

Abella < Kind map Type -> Type -> Type.

Abella < Type map A -> B -> (map A B).

Abella < Define subst : (list (map A A)) -> B -> B -> prop by 
subst nil M M;
nabla x, subst (map x V :: ML) (R x) M := subst ML (R V) M.

Abella < Theorem subst_det [A,B] : 
forall ML M M' M'', subst ML M M' -> subst ML M M'' -> M' = M''.

============================
 forall ML M M' M'', subst ML M M' -> subst ML M M'' -> M' = M''

subst_det < induction on 1.

IH : forall ML M M' M'', subst ML M M' * -> subst ML M M'' -> M' = M''
============================
 forall ML M M' M'', subst ML M M' @ -> subst ML M M'' -> M' = M''

subst_det < intros.

Variables: ML M M' M''
IH : forall ML M M' M'', subst ML M M' * -> subst ML M M'' -> M' = M''
H1 : subst ML M M' @
H2 : subst ML M M''
============================
 M' = M''

subst_det < case H1.

Subgoal 1:

Variables: M' M''
IH : forall ML M M' M'', subst ML M M' * -> subst ML M M'' -> M' = M''
H2 : subst nil M' M''
============================
 M' = M''

Subgoal 2 is:
 M1 = M'' n1

subst_det < case H2.

Subgoal 1:

Variables: M''
IH : forall ML M M' M'', subst ML M M' * -> subst ML M M'' -> M' = M''
============================
 M'' = M''

Subgoal 2 is:
 M1 = M'' n1

subst_det < search.

Subgoal 2:

Variables: M M'' M1 ML1 V
IH : forall ML M M' M'', subst ML M M' * -> subst ML M M'' -> M' = M''
H2 : subst (map n1 V :: ML1) (M n1) (M'' n1)
H3 : subst ML1 (M V) M1 *
============================
 M1 = M'' n1

subst_det < case H2.

Subgoal 2:

Variables: M M1 ML1 V M2
IH : forall ML M M' M'', subst ML M M' * -> subst ML M M'' -> M' = M''
H3 : subst ML1 (M V) M1 *
H4 : subst ML1 (M V) M2
============================
 M1 = M2

subst_det < apply IH to H3 H4.

Subgoal 2:

Variables: M ML1 V M2
IH : forall ML M M' M'', subst ML M M' * -> subst ML M M'' -> M' = M''
H3 : subst ML1 (M V) M2 *
H4 : subst ML1 (M V) M2
============================
 M2 = M2

subst_det < search.
Proof completed.

Abella < Theorem subst_prune [A,B,C] : 
forall ML M M', nabla x, subst ML M (M' x) -> (exists M'', M' = y\M'').

============================
 forall ML M M', nabla x, subst ML M (M' x) -> (exists M'', M' = y\M'')

subst_prune < induction on 1.

IH : forall ML M M', nabla x, subst ML M (M' x) * -> (exists M'', M' = y\M'')
============================
 forall ML M M', nabla x, subst ML M (M' x) @ -> (exists M'', M' = y\M'')

subst_prune < intros.

Variables: ML M M'
IH : forall ML M M', nabla x, subst ML M (M' x) * -> (exists M'', M' = y\M'')
H1 : subst ML M (M' n1) @
============================
 exists M'', M' = y\M''

subst_prune < case H1.

Subgoal 1:

Variables: M
IH : forall ML M M', nabla x, subst ML M (M' x) * -> (exists M'', M' = y\M'')
============================
 exists M'', z1\M = y\M''

Subgoal 2 is:
 exists M'', z2\M2 z2 = y\M''

subst_prune < search.

Subgoal 2:

Variables: M M2 ML3 ML2
IH : forall ML M M', nabla x, subst ML M (M' x) * -> (exists M'', M' = y\M'')
H2 : subst ML3 (M ML2) (M2 n1) *
============================
 exists M'', z2\M2 z2 = y\M''

subst_prune < apply IH to H2.

Subgoal 2:

Variables: M ML3 ML2 M''
IH : forall ML M M', nabla x, subst ML M (M' x) * -> (exists M'', M' = y\M'')
H2 : subst ML3 (M ML2) M'' *
============================
 exists M''1, z2\M'' = y\M''1

subst_prune < search.
Proof completed.

Abella < Theorem subst_inst [A,B,C] : 
forall ML M1 M2 M1' M2', nabla x, subst ML M1 M1' ->
  subst ML (M2 x) (M2' x) -> subst ML (M2 M1) (M2' M1').

============================
 forall ML M1 M2 M1' M2', nabla x, subst ML M1 M1' ->
   subst ML (M2 x) (M2' x) -> subst ML (M2 M1) (M2' M1')

subst_inst < induction on 2.

IH : forall ML M1 M2 M1' M2', nabla x, subst ML M1 M1' ->
       subst ML (M2 x) (M2' x) * -> subst ML (M2 M1) (M2' M1')
============================
 forall ML M1 M2 M1' M2', nabla x, subst ML M1 M1' ->
   subst ML (M2 x) (M2' x) @ -> subst ML (M2 M1) (M2' M1')

subst_inst < intros.

Variables: ML M1 M2 M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, subst ML M1 M1' ->
       subst ML (M2 x) (M2' x) * -> subst ML (M2 M1) (M2' M1')
H1 : subst ML M1 M1'
H2 : subst ML (M2 n1) (M2' n1) @
============================
 subst ML (M2 M1) (M2' M1')

subst_inst < case H2.

Subgoal 1:

Variables: M1 M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, subst ML M1 M1' ->
       subst ML (M2 x) (M2' x) * -> subst ML (M2 M1) (M2' M1')
H1 : subst nil M1 M1'
============================
 subst nil (M2' M1) (M2' M1')

Subgoal 2 is:
 subst (map n2 ML2 :: ML3) (M2 n2 (M1 n2)) (M3 (M1' n2))

subst_inst < case H1.

Subgoal 1:

Variables: M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, subst ML M1 M1' ->
       subst ML (M2 x) (M2' x) * -> subst ML (M2 M1) (M2' M1')
============================
 subst nil (M2' M1') (M2' M1')

Subgoal 2 is:
 subst (map n2 ML2 :: ML3) (M2 n2 (M1 n2)) (M3 (M1' n2))

subst_inst < search.

Subgoal 2:

Variables: M1 M2 M1' M3 ML3 ML2
IH : forall ML M1 M2 M1' M2', nabla x, subst ML M1 M1' ->
       subst ML (M2 x) (M2' x) * -> subst ML (M2 M1) (M2' M1')
H1 : subst (map n2 ML2 :: ML3) (M1 n2) (M1' n2)
H3 : subst ML3 (M2 ML2 n1) (M3 n1) *
============================
 subst (map n2 ML2 :: ML3) (M2 n2 (M1 n2)) (M3 (M1' n2))

subst_inst < case H1.

Subgoal 2:

Variables: M1 M2 M3 ML3 ML2 M
IH : forall ML M1 M2 M1' M2', nabla x, subst ML M1 M1' ->
       subst ML (M2 x) (M2' x) * -> subst ML (M2 M1) (M2' M1')
H3 : subst ML3 (M2 ML2 n1) (M3 n1) *
H4 : subst ML3 (M1 ML2) M
============================
 subst (map n2 ML2 :: ML3) (M2 n2 (M1 n2)) (M3 M)

subst_inst < apply IH to H4 H3.

Subgoal 2:

Variables: M1 M2 M3 ML3 ML2 M
IH : forall ML M1 M2 M1' M2', nabla x, subst ML M1 M1' ->
       subst ML (M2 x) (M2' x) * -> subst ML (M2 M1) (M2' M1')
H3 : subst ML3 (M2 ML2 n1) (M3 n1) *
H4 : subst ML3 (M1 ML2) M
H5 : subst ML3 (M2 ML2 (M1 ML2)) (M3 M)
============================
 subst (map n2 ML2 :: ML3) (M2 n2 (M1 n2)) (M3 M)

subst_inst < search.
Proof completed.

Abella <