Welcome to Abella 2.0.3-dev

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

Abella < Theorem ty_indep_tm_simp : 
forall T, nabla x, {tm x |- ty (T x)} -> (exists T', T = y\T' /\ {ty T'}).

============================
 forall T, nabla x, {tm x |- ty (T x)} -> (exists T', T = y\T' /\ {ty T'})

ty_indep_tm_simp < induction on 1.

IH : forall T, nabla x, {tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {ty T'})
============================
 forall T, nabla x, {tm x |- ty (T x)}@ -> (exists T', T = y\T' /\ {ty T'})

ty_indep_tm_simp < intros.

Variables: T
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {ty T'})
H1 : {tm n1 |- ty (T n1)}@
============================
 exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < case H1.

Subgoal 1:

IH : forall T, nabla x, {tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {ty T'})
============================
 exists T', z1\b = y\T' /\ {ty T'}

Subgoal 2 is:
 exists T', z1\arr (T1 z1) (T2 z1) = y\T' /\ {ty T'}

Subgoal 3 is:
 exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < search.

Subgoal 2:

Variables: T2 T1
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {ty T'})
H2 : {tm n1 |- ty (T1 n1)}*
H3 : {tm n1 |- ty (T2 n1)}*
============================
 exists T', z1\arr (T1 z1) (T2 z1) = y\T' /\ {ty T'}

Subgoal 3 is:
 exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < apply IH to H2.

Subgoal 2:

Variables: T2 T'
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {ty T'})
H2 : {tm n1 |- ty T'}*
H3 : {tm n1 |- ty (T2 n1)}*
H4 : {ty T'}
============================
 exists T'1, z1\arr T' (T2 z1) = y\T'1 /\ {ty T'1}

Subgoal 3 is:
 exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < apply IH to H3.

Subgoal 2:

Variables: T' T'1
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {ty T'})
H2 : {tm n1 |- ty T'}*
H3 : {tm n1 |- ty T'1}*
H4 : {ty T'}
H5 : {ty T'1}
============================
 exists T'2, z1\arr T' T'1 = y\T'2 /\ {ty T'2}

Subgoal 3 is:
 exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < search.

Subgoal 3:

Variables: T F
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {ty T'})
H2 : {tm n1, [F n1] |- ty (T n1)}*
H3 : member (F n1) (tm n1 :: nil)
============================
 exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < case H3.

Subgoal 3.1:

Variables: T
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {ty T'})
H2 : {tm n1, [tm n1] |- ty (T n1)}*
============================
 exists T', T = y\T' /\ {ty T'}

Subgoal 3.2 is:
 exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < case H2.

Subgoal 3.2:

Variables: T F
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {ty T'})
H2 : {tm n1, [F n1] |- ty (T n1)}*
H4 : member (F n1) nil
============================
 exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < case H4.
Proof completed.

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

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

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

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

ctx_mem < induction on 2.

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

ctx_mem < intros.

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

ctx_mem < case H2.

Subgoal 1:

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

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

ctx_mem < case H1.

Subgoal 1:

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

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

ctx_mem < search.

Subgoal 2:

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

ctx_mem < case H1.

Subgoal 2:

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

ctx_mem < apply IH to H4 H3.

Subgoal 2:

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

ctx_mem < search.
Proof completed.

Abella < Theorem ty_indep_tm : 
forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)} ->
  (exists T', T = y\T' /\ {L |- ty T'}).

============================
 forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)} ->
   (exists T', T = y\T' /\ {L |- ty T'})

ty_indep_tm < induction on 2.

IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {L |- ty T'})
============================
 forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}@ ->
   (exists T', T = y\T' /\ {L |- ty T'})

ty_indep_tm < intros.

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

ty_indep_tm < case H2.

Subgoal 1:

Variables: L
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
============================
 exists T', z1\b = y\T' /\ {L |- ty T'}

Subgoal 2 is:
 exists T', z1\arr (T1 z1) (T2 z1) = y\T' /\ {L |- ty T'}

Subgoal 3 is:
 exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < search.

Subgoal 2:

Variables: L T2 T1
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1 |- ty (T1 n1)}*
H4 : {L, tm n1 |- ty (T2 n1)}*
============================
 exists T', z1\arr (T1 z1) (T2 z1) = y\T' /\ {L |- ty T'}

Subgoal 3 is:
 exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < apply IH to _ H3.

Subgoal 2:

Variables: L T2 T'
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1 |- ty T'}*
H4 : {L, tm n1 |- ty (T2 n1)}*
H5 : {L |- ty T'}
============================
 exists T'1, z1\arr T' (T2 z1) = y\T'1 /\ {L |- ty T'1}

Subgoal 3 is:
 exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < apply IH to _ H4.

Subgoal 2:

Variables: L T' T'1
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1 |- ty T'}*
H4 : {L, tm n1 |- ty T'1}*
H5 : {L |- ty T'}
H6 : {L |- ty T'1}
============================
 exists T'2, z1\arr T' T'1 = y\T'2 /\ {L |- ty T'2}

Subgoal 3 is:
 exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < search.

Subgoal 3:

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

ty_indep_tm < case H4.

Subgoal 3.1:

Variables: L T
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1, [tm n1] |- ty (T n1)}*
============================
 exists T', T = y\T' /\ {L |- ty T'}

Subgoal 3.2 is:
 exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < case H3.

Subgoal 3.2:

Variables: L T F
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1, [F n1] |- ty (T n1)}*
H5 : member (F n1) L
============================
 exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < apply ctx_mem to H1 H5.

Subgoal 3.2:

Variables: L T X
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
       (exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1, [tm (X n1)] |- ty (T n1)}*
H5 : member (tm (X n1)) L
H6 : name (X n1)
============================
 exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < case H3.
Proof completed.

Abella < Goodbye.