Welcome to Abella 2.0.4

Abella < Specification "stlc".
Reading specification "+/stlc"

Abella < Close tm, ty.

Abella < Kind map type.

Abella < Kind map_list type.

Abella < Type map tm -> tm -> map.

Abella < Type mnil map_list.

Abella < Type mcons map -> map_list -> map_list.

Abella < Define subst : map_list -> tm -> tm -> prop by 
subst mnil M M;
nabla x, subst (mcons (map x V) ML) (R x) M := subst ML (R V) M.

Abella < Theorem subst_app_comm : 
forall ML M1 M2 M', subst ML (app M1 M2) M' ->
  (exists M1' M2', M' = app M1' M2' /\ subst ML M1 M1' /\ subst ML M2 M2').

============================
 forall ML M1 M2 M', subst ML (app M1 M2) M' ->
   (exists M1' M2', M' = app M1' M2' /\ subst ML M1 M1' /\ subst ML M2 M2')

subst_app_comm < induction on 1.

IH : forall ML M1 M2 M', subst ML (app M1 M2) M' * ->
       (exists M1' M2', M' = app M1' M2' /\ subst ML M1 M1' /\
            subst ML M2 M2')
============================
 forall ML M1 M2 M', subst ML (app M1 M2) M' @ ->
   (exists M1' M2', M' = app M1' M2' /\ subst ML M1 M1' /\ subst ML M2 M2')

subst_app_comm < intros.

Variables: ML M1 M2 M'
IH : forall ML M1 M2 M', subst ML (app M1 M2) M' * ->
       (exists M1' M2', M' = app M1' M2' /\ subst ML M1 M1' /\
            subst ML M2 M2')
H1 : subst ML (app M1 M2) M' @
============================
 exists M1' M2', M' = app M1' M2' /\ subst ML M1 M1' /\ subst ML M2 M2'

subst_app_comm < case H1.

Subgoal 1:

Variables: M1 M2
IH : forall ML M1 M2 M', subst ML (app M1 M2) M' * ->
       (exists M1' M2', M' = app M1' M2' /\ subst ML M1 M1' /\
            subst ML M2 M2')
============================
 exists M1' M2', app M1 M2 = app M1' M2' /\ subst mnil M1 M1' /\
   subst mnil M2 M2'

Subgoal 2 is:
 exists M1' M2', M = app M1' M2' /\
   subst (mcons (map n1 V) ML1) (M1 n1) M1' /\
   subst (mcons (map n1 V) ML1) (M2 n1) M2'

subst_app_comm < search.

Subgoal 2:

Variables: M1 M2 M ML1 V
IH : forall ML M1 M2 M', subst ML (app M1 M2) M' * ->
       (exists M1' M2', M' = app M1' M2' /\ subst ML M1 M1' /\
            subst ML M2 M2')
H2 : subst ML1 (app (M1 V) (M2 V)) M *
============================
 exists M1' M2', M = app M1' M2' /\
   subst (mcons (map n1 V) ML1) (M1 n1) M1' /\
   subst (mcons (map n1 V) ML1) (M2 n1) M2'

subst_app_comm < apply IH to H2.

Subgoal 2:

Variables: M1 M2 ML1 V M1' M2'
IH : forall ML M1 M2 M', subst ML (app M1 M2) M' * ->
       (exists M1' M2', M' = app M1' M2' /\ subst ML M1 M1' /\
            subst ML M2 M2')
H2 : subst ML1 (app (M1 V) (M2 V)) (app M1' M2') *
H3 : subst ML1 (M1 V) M1'
H4 : subst ML1 (M2 V) M2'
============================
 exists M1'1 M2'1, app M1' M2' = app M1'1 M2'1 /\
   subst (mcons (map n1 V) ML1) (M1 n1) M1'1 /\
   subst (mcons (map n1 V) ML1) (M2 n1) M2'1

subst_app_comm < search.
Proof completed.

Abella < Theorem subst_abs_comm : 
forall ML R T M', subst ML (abs T R) M' ->
  (exists R', M' = abs T R' /\ (nabla x, subst ML (R x) (R' x))).

============================
 forall ML R T M', subst ML (abs T R) M' ->
   (exists R', M' = abs T R' /\ (nabla x, subst ML (R x) (R' x)))

subst_abs_comm < induction on 1.

IH : forall ML R T M', subst ML (abs T R) M' * ->
       (exists R', M' = abs T R' /\ (nabla x, subst ML (R x) (R' x)))
============================
 forall ML R T M', subst ML (abs T R) M' @ ->
   (exists R', M' = abs T R' /\ (nabla x, subst ML (R x) (R' x)))

subst_abs_comm < intros.

Variables: ML R T M'
IH : forall ML R T M', subst ML (abs T R) M' * ->
       (exists R', M' = abs T R' /\ (nabla x, subst ML (R x) (R' x)))
H1 : subst ML (abs T R) M' @
============================
 exists R', M' = abs T R' /\ (nabla x, subst ML (R x) (R' x))

subst_abs_comm < case H1.

Subgoal 1:

Variables: R T
IH : forall ML R T M', subst ML (abs T R) M' * ->
       (exists R', M' = abs T R' /\ (nabla x, subst ML (R x) (R' x)))
============================
 exists R', abs T R = abs T R' /\ (nabla x, subst mnil (R x) (R' x))

Subgoal 2 is:
 exists R', M = abs T R' /\
   (nabla x, subst (mcons (map n1 V) ML1) (R n1 x) (R' x))

subst_abs_comm < search.

Subgoal 2:

Variables: R T M ML1 V
IH : forall ML R T M', subst ML (abs T R) M' * ->
       (exists R', M' = abs T R' /\ (nabla x, subst ML (R x) (R' x)))
H2 : subst ML1 (abs T (R V)) M *
============================
 exists R', M = abs T R' /\
   (nabla x, subst (mcons (map n1 V) ML1) (R n1 x) (R' x))

subst_abs_comm < apply IH to H2.

Subgoal 2:

Variables: R T ML1 V R'
IH : forall ML R T M', subst ML (abs T R) M' * ->
       (exists R', M' = abs T R' /\ (nabla x, subst ML (R x) (R' x)))
H2 : subst ML1 (abs T (R V)) (abs T R') *
H3 : subst ML1 (R V n1) (R' n1)
============================
 exists R'1, abs T R' = abs T R'1 /\
   (nabla x, subst (mcons (map n1 V) ML1) (R n1 x) (R'1 x))

subst_abs_comm < search.
Proof completed.

Abella < Define name : tm -> prop by 
nabla x, name x.

Abella < Theorem mem_tm_prune : 
forall M L, nabla x, member (M x) L -> (exists M', M = y\M').

============================
 forall M L, nabla x, member (M x) L -> (exists M', M = y\M')

mem_tm_prune < induction on 1.

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

mem_tm_prune < intros.

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

mem_tm_prune < case H1.

Subgoal 1:

Variables: L3 L2
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
============================
 exists M', z1\L2 = y\M'

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

mem_tm_prune < search.

Subgoal 2:

Variables: M L3 L2
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H2 : member (M n1) L3 *
============================
 exists M', M = y\M'

mem_tm_prune < apply IH to H2.

Subgoal 2:

Variables: L3 L2 M'
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H2 : member M' L3 *
============================
 exists M'1, z1\M' = y\M'1

mem_tm_prune < search.
Proof completed.

Abella < Define tm_ctx : olist -> prop by 
tm_ctx nil;
nabla x, tm_ctx (tm x :: L) := tm_ctx L.

Abella < Theorem tm_ctx_mem : 
forall L E, tm_ctx L -> member E L -> (exists X, E = tm X /\ name X).

============================
 forall L E, tm_ctx L -> member E L -> (exists X, E = tm X /\ name X)

tm_ctx_mem < induction on 2.

IH : forall L E, tm_ctx L -> member E L * -> (exists X, E = tm X /\ name X)
============================
 forall L E, tm_ctx L -> member E L @ -> (exists X, E = tm X /\ name X)

tm_ctx_mem < intros.

Variables: L E
IH : forall L E, tm_ctx L -> member E L * -> (exists X, E = tm X /\ name X)
H1 : tm_ctx L
H2 : member E L @
============================
 exists X, E = tm X /\ name X

tm_ctx_mem < case H2.

Subgoal 1:

Variables: E L1
IH : forall L E, tm_ctx L -> member E L * -> (exists X, E = tm X /\ name X)
H1 : tm_ctx (E :: L1)
============================
 exists X, E = tm X /\ name X

Subgoal 2 is:
 exists X, E = tm X /\ name X

tm_ctx_mem < case H1.

Subgoal 1:

Variables: L2
IH : forall L E, tm_ctx L -> member E L * -> (exists X, E = tm X /\ name X)
H3 : tm_ctx L2
============================
 exists X, tm n1 = tm X /\ name X

Subgoal 2 is:
 exists X, E = tm X /\ name X

tm_ctx_mem < search.

Subgoal 2:

Variables: E L1 B
IH : forall L E, tm_ctx L -> member E L * -> (exists X, E = tm X /\ name X)
H1 : tm_ctx (B :: L1)
H3 : member E L1 *
============================
 exists X, E = tm X /\ name X

tm_ctx_mem < case H1.

Subgoal 2:

Variables: E L2
IH : forall L E, tm_ctx L -> member E L * -> (exists X, E = tm X /\ name X)
H3 : member (E n1) L2 *
H4 : tm_ctx L2
============================
 exists X, E n1 = tm X /\ name X

tm_ctx_mem < apply IH to _ H3.

Subgoal 2:

Variables: L2 X
IH : forall L E, tm_ctx L -> member E L * -> (exists X, E = tm X /\ name X)
H3 : member (tm (X n1)) L2 *
H4 : tm_ctx L2
H5 : name (X n1)
============================
 exists X1, tm (X n1) = tm X1 /\ name X1

tm_ctx_mem < search.
Proof completed.

Abella < Theorem closed_tm_prune : 
forall L M, nabla x, tm_ctx L -> {L |- tm (M x)} -> (exists M', M = y\M').

============================
 forall L M, nabla x, tm_ctx L -> {L |- tm (M x)} -> (exists M', M = y\M')

closed_tm_prune < induction on 2.

IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
============================
 forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}@ -> (exists M', M = y\M')

closed_tm_prune < intros.

Variables: L M
IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
H1 : tm_ctx L
H2 : {L |- tm (M n1)}@
============================
 exists M', M = y\M'

closed_tm_prune < case H2.

Subgoal 1:

Variables: L N M1
IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
H1 : tm_ctx L
H3 : {L |- tm (M1 n1)}*
H4 : {L |- tm (N n1)}*
============================
 exists M', z1\app (M1 z1) (N z1) = y\M'

Subgoal 2 is:
 exists M', z1\abs T (R z1) = y\M'

Subgoal 3 is:
 exists M', M = y\M'

closed_tm_prune < apply IH to _ H3.

Subgoal 1:

Variables: L N M'
IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
H1 : tm_ctx L
H3 : {L |- tm M'}*
H4 : {L |- tm (N n1)}*
============================
 exists M'1, z1\app M' (N z1) = y\M'1

Subgoal 2 is:
 exists M', z1\abs T (R z1) = y\M'

Subgoal 3 is:
 exists M', M = y\M'

closed_tm_prune < apply IH to _ H4.

Subgoal 1:

Variables: L M' M'1
IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
H1 : tm_ctx L
H3 : {L |- tm M'}*
H4 : {L |- tm M'1}*
============================
 exists M'2, z1\app M' M'1 = y\M'2

Subgoal 2 is:
 exists M', z1\abs T (R z1) = y\M'

Subgoal 3 is:
 exists M', M = y\M'

closed_tm_prune < search.

Subgoal 2:

Variables: L R T
IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
H1 : tm_ctx L
H3 : {L, tm n2 |- tm (R n1 n2)}*
============================
 exists M', z1\abs T (R z1) = y\M'

Subgoal 3 is:
 exists M', M = y\M'

closed_tm_prune < apply IH to _ H3.

Subgoal 2:

Variables: L T M'
IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
H1 : tm_ctx L
H3 : {L, tm n2 |- tm (M' n2)}*
============================
 exists M'1, z1\abs T (z2\M' z2) = y\M'1

Subgoal 3 is:
 exists M', M = y\M'

closed_tm_prune < search.

Subgoal 3:

Variables: L M F
IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
H1 : tm_ctx L
H3 : {L, [F n1] |- tm (M n1)}*
H4 : member (F n1) L
============================
 exists M', M = y\M'

closed_tm_prune < apply tm_ctx_mem to _ H4.

Subgoal 3:

Variables: L M X
IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
H1 : tm_ctx L
H3 : {L, [tm (X n1)] |- tm (M n1)}*
H4 : member (tm (X n1)) L
H5 : name (X n1)
============================
 exists M', M = y\M'

closed_tm_prune < case H3.

Subgoal 3:

Variables: L M
IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
H1 : tm_ctx L
H4 : member (tm (M n1)) L
H5 : name (M n1)
============================
 exists M', M = y\M'

closed_tm_prune < case H5.

Subgoal 3.1:

Variables: L
IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
H1 : tm_ctx (L n2)
H4 : member (tm n2) (L n2)
============================
 exists M', z2\n2 = y\M'

Subgoal 3.2 is:
 exists M', z1\z1 = y\M'

closed_tm_prune < search.

Subgoal 3.2:

Variables: L
IH : forall L M, nabla x, tm_ctx L -> {L |- tm (M x)}* ->
       (exists M', M = y\M')
H1 : tm_ctx L
H4 : member (tm n1) L
============================
 exists M', z1\z1 = y\M'

closed_tm_prune < apply mem_tm_prune to H4.
Proof completed.

Abella < Theorem subst_closed_tm : 
forall M ML M', {tm M} -> subst ML M M' -> M = M'.

============================
 forall M ML M', {tm M} -> subst ML M M' -> M = M'

subst_closed_tm < induction on 2.

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

subst_closed_tm < intros.

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

subst_closed_tm < case H2.

Subgoal 1:

Variables: M'
IH : forall M ML M', {tm M} -> subst ML M M' * -> M = M'
H1 : {tm M'}
============================
 M' = M'

Subgoal 2 is:
 M n1 = M1

subst_closed_tm < search.

Subgoal 2:

Variables: M M1 ML1 V
IH : forall M ML M', {tm M} -> subst ML M M' * -> M = M'
H1 : {tm (M n1)}
H3 : subst ML1 (M V) M1 *
============================
 M n1 = M1

subst_closed_tm < apply closed_tm_prune to _ H1.

Subgoal 2:

Variables: M1 ML1 V M'1
IH : forall M ML M', {tm M} -> subst ML M M' * -> M = M'
H1 : {tm M'1}
H3 : subst ML1 M'1 M1 *
============================
 M'1 = M1

subst_closed_tm < apply IH to H1 H3.

Subgoal 2:

Variables: M1 ML1 V
IH : forall M ML M', {tm M} -> subst ML M M' * -> M = M'
H1 : {tm M1}
H3 : subst ML1 M1 M1 *
============================
 M1 = M1

subst_closed_tm < search.
Proof completed.

Abella < Theorem subst_inst : 
forall ML M M' V, nabla x, {tm V} -> subst ML (M x) (M' x) ->
  subst ML (M V) (M' V).

============================
 forall ML M M' V, nabla x, {tm V} -> subst ML (M x) (M' x) ->
   subst ML (M V) (M' V)

subst_inst < induction on 2.

IH : forall ML M M' V, nabla x, {tm V} -> subst ML (M x) (M' x) * ->
       subst ML (M V) (M' V)
============================
 forall ML M M' V, nabla x, {tm V} -> subst ML (M x) (M' x) @ ->
   subst ML (M V) (M' V)

subst_inst < intros.

Variables: ML M M' V
IH : forall ML M M' V, nabla x, {tm V} -> subst ML (M x) (M' x) * ->
       subst ML (M V) (M' V)
H1 : {tm V}
H2 : subst ML (M n1) (M' n1) @
============================
 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} -> subst ML (M x) (M' x) * ->
       subst ML (M V) (M' V)
H1 : {tm V}
============================
 subst mnil (M' V) (M' V)

Subgoal 2 is:
 subst (mcons (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} -> subst ML (M x) (M' x) * ->
       subst ML (M V) (M' V)
H1 : {tm (V n2)}
H3 : subst ML3 (M ML2 n1) (M2 n1) *
============================
 subst (mcons (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} -> subst ML (M x) (M' x) * ->
       subst ML (M V) (M' V)
H1 : {tm M'1}
H3 : subst ML3 (M ML2 n1) (M2 n1) *
============================
 subst (mcons (map n2 ML2) ML3) (M n2 M'1) (M2 M'1)

subst_inst < apply IH to _ H3.

Subgoal 2:

Variables: M M2 ML3 ML2 M'1
IH : forall ML M M' V, nabla x, {tm V} -> subst ML (M x) (M' x) * ->
       subst ML (M V) (M' V)
H1 : {tm M'1}
H3 : subst ML3 (M ML2 n1) (M2 n1) *
H4 : subst ML3 (M ML2 M'1) (M2 M'1)
============================
 subst (mcons (map n2 ML2) ML3) (M n2 M'1) (M2 M'1)

subst_inst < search.
Proof completed.

Abella < Theorem explct_meta_subst_assoc : 
forall ML M M' V, nabla n, {tm V} -> subst ML (M n) (M' n) ->
  subst (mcons (map n V) ML) (M n) (M' V).

============================
 forall ML M M' V, nabla n, {tm V} -> subst ML (M n) (M' n) ->
   subst (mcons (map n V) ML) (M n) (M' V)

explct_meta_subst_assoc < intros.

Variables: ML M M' V
H1 : {tm V}
H2 : subst ML (M n1) (M' n1)
============================
 subst (mcons (map n1 V) ML) (M n1) (M' V)

explct_meta_subst_assoc < unfold.

Variables: ML M M' V
H1 : {tm V}
H2 : subst ML (M n1) (M' n1)
============================
 subst ML (M V) (M' V)

explct_meta_subst_assoc < intros.

Variables: ML M M' V
H1 : {tm V}
H2 : subst ML (M n1) (M' n1)
============================
 subst ML (M V) (M' V)

explct_meta_subst_assoc < backchain subst_inst with M = M, M' = M', x = n1.
Proof completed.

Abella <