Welcome to Abella 2.0.3-dev

Abella < Specification "str1".
Reading specification "str1"

Abella < Define ctx : olist ->
prop by 
ctx nil;
ctx ((p => q) :: L) := ctx L.

Abella < Theorem ctx_mem : 
forall L E, ctx L -> member E L -> E = p => q.

============================
 forall L E, ctx L -> member E L -> E = p => q

ctx_mem < induction on 2.

IH : forall L E, ctx L -> member E L * -> E = p => q
============================
 forall L E, ctx L -> member E L @ -> E = p => q

ctx_mem < intros.

Variables: L E
IH : forall L E, ctx L -> member E L * -> E = p => q
H1 : ctx L
H2 : member E L @
============================
 E = p => q

ctx_mem < case H2.

Subgoal 1:

Variables: E L1
IH : forall L E, ctx L -> member E L * -> E = p => q
H1 : ctx (E :: L1)
============================
 E = p => q

Subgoal 2 is:
 E = p => q

ctx_mem < case H1.

Subgoal 1:

Variables: L1
IH : forall L E, ctx L -> member E L * -> E = p => q
H3 : ctx L1
============================
 p => q = p => q

Subgoal 2 is:
 E = p => q

ctx_mem < search.

Subgoal 2:

Variables: E L1 B
IH : forall L E, ctx L -> member E L * -> E = p => q
H1 : ctx (B :: L1)
H3 : member E L1 *
============================
 E = p => q

ctx_mem < case H1.

Subgoal 2:

Variables: E L1
IH : forall L E, ctx L -> member E L * -> E = p => q
H3 : member E L1 *
H4 : ctx L1
============================
 E = p => q

ctx_mem < apply IH to H4 H3.

Subgoal 2:

Variables: L1
IH : forall L E, ctx L -> member E L * -> E = p => q
H3 : member (p => q) L1 *
H4 : ctx L1
============================
 p => q = p => q

ctx_mem < search.
Proof completed.

Abella < Theorem indep : 
(forall L, ctx L -> {L, p |- p} -> {L |- p}) /\
  (forall L, ctx L -> {L, p |- q} -> {L |- q}) /\
  (forall L, ctx L -> {L, p |- r} -> {L |- r}).

============================
 (forall L, ctx L -> {L, p |- p} -> {L |- p}) /\
   (forall L, ctx L -> {L, p |- q} -> {L |- q}) /\
   (forall L, ctx L -> {L, p |- r} -> {L |- r})

indep < induction on 2 2 2.

IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
============================
 (forall L, ctx L -> {L, p |- p}@ -> {L |- p}) /\
   (forall L, ctx L -> {L, p |- q}@ -> {L |- q}) /\
   (forall L, ctx L -> {L, p |- r}@ -> {L |- r})

indep < intros.

IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
============================
 (forall L, ctx L -> {L, p |- p}@ -> {L |- p}) /\
   (forall L, ctx L -> {L, p |- q}@ -> {L |- q}) /\
   (forall L, ctx L -> {L, p |- r}@ -> {L |- r})

indep < split.

Subgoal 1:

IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
============================
 forall L, ctx L -> {L, p |- p}@ -> {L |- p}

Subgoal 2 is:
 forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < intros.

Subgoal 1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H2 : {L, p |- p}@
============================
 {L |- p}

Subgoal 2 is:
 forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H2.

Subgoal 1:

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- p}*
H4 : member F (p :: L)
============================
 {L |- p}

Subgoal 2 is:
 forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H4.

Subgoal 1.1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p] |- p}*
============================
 {L |- p}

Subgoal 1.2 is:
 {L |- p}

Subgoal 2 is:
 forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H3.

Subgoal 1.1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
============================
 {L |- p}

Subgoal 1.2 is:
 {L |- p}

Subgoal 2 is:
 forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < skip.

Subgoal 1.2:

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- p}*
H5 : member F L
============================
 {L |- p}

Subgoal 2 is:
 forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < apply ctx_mem to _ H5.

Subgoal 1.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p => q] |- p}*
H5 : member (p => q) L
============================
 {L |- p}

Subgoal 2 is:
 forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H3.

Subgoal 2:

IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
============================
 forall L, ctx L -> {L, p |- q}@ -> {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < intros.

Subgoal 2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H2 : {L, p |- q}@
============================
 {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H2.

Subgoal 2:

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- q}*
H4 : member F (p :: L)
============================
 {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H4.

Subgoal 2.1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p] |- q}*
============================
 {L |- q}

Subgoal 2.2 is:
 {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H3.

Subgoal 2.2:

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- q}*
H5 : member F L
============================
 {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < apply ctx_mem to _ H5.

Subgoal 2.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p => q] |- q}*
H5 : member (p => q) L
============================
 {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < case H3.

Subgoal 2.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H5 : member (p => q) L
H6 : {L, p |- p}*
============================
 {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < apply IH to _ H6.

Subgoal 2.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H5 : member (p => q) L
H6 : {L, p |- p}*
H7 : {L |- p}
============================
 {L |- q}

Subgoal 3 is:
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < search.

Subgoal 3:

IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
============================
 forall L, ctx L -> {L, p |- r}@ -> {L |- r}

indep < intros.

Subgoal 3:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H2 : {L, p |- r}@
============================
 {L |- r}

indep < case H2.

Subgoal 3.1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, p => q |- r}*
============================
 {L |- r}

Subgoal 3.2 is:
 {L |- r}

Subgoal 3.3 is:
 {L |- r}

indep < apply IH2 to _ H3.

Subgoal 3.1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, p => q |- r}*
H4 : {L, p => q |- r}
============================
 {L |- r}

Subgoal 3.2 is:
 {L |- r}

Subgoal 3.3 is:
 {L |- r}

indep < search.

Subgoal 3.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p |- q}*
============================
 {L |- r}

Subgoal 3.3 is:
 {L |- r}

indep < apply IH1 to _ H3.

Subgoal 3.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p |- q}*
H4 : {L |- q}
============================
 {L |- r}

Subgoal 3.3 is:
 {L |- r}

indep < search.

Subgoal 3.3:

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- r}*
H4 : member F (p :: L)
============================
 {L |- r}

indep < case H4.

Subgoal 3.3.1:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p] |- r}*
============================
 {L |- r}

Subgoal 3.3.2 is:
 {L |- r}

indep < case H3.

Subgoal 3.3.2:

Variables: L F
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [F] |- r}*
H5 : member F L
============================
 {L |- r}

indep < apply ctx_mem to _ H5.

Subgoal 3.3.2:

Variables: L
IH : forall L, ctx L -> {L, p |- p}* -> {L |- p}
IH1 : forall L, ctx L -> {L, p |- q}* -> {L |- q}
IH2 : forall L, ctx L -> {L, p |- r}* -> {L |- r}
H1 : ctx L
H3 : {L, p, [p => q] |- r}*
H5 : member (p => q) L
============================
 {L |- r}

indep < case H3.
Proof completed.

Abella < Goodbye.