Welcome to Abella 1.1.3-dev2 Reading clauses from focus.mod

Abella < Define ctx nil.

Abella < Define ctx (hyp B :: L) := {form B} /\ ctx L.

Abella < Theorem ctx_member : 
forall E L, ctx L -> member E L -> (exists B, E = hyp B /\ {form B}).

1 subgoal(s).

  
  ============================
   forall E L, ctx L -> member E L -> (exists B, E = hyp B /\ {form B})

ctx_member < induction on 1.

1 subgoal(s).

  
  IH : forall E L, ctx L * -> member E L -> (exists B, E = hyp B /\ {form B})
  ============================
   forall E L, ctx L @ -> member E L -> (exists B, E = hyp B /\ {form B})

ctx_member < intros.

1 subgoal(s).

  Variables: E, L
  IH : forall E L, ctx L * -> member E L -> (exists B, E = hyp B /\ {form B})
  H1 : ctx L @
  H2 : member E L
  ============================
   exists B, E = hyp B /\ {form B}

ctx_member < case H1.

2 subgoal(s).

  Variables: E, L
  IH : forall E L, ctx L * -> member E L -> (exists B, E = hyp B /\ {form B})
  H2 : member E nil
  ============================
   exists B, E = hyp B /\ {form B}

subgoal 2 is:
 exists B, E = hyp B /\ {form B}

ctx_member < case H2.

1 subgoal(s).

  Variables: E, L, L1, B
  IH : forall E L, ctx L * -> member E L -> (exists B, E = hyp B /\ {form B})
  H2 : member E (hyp B :: L1)
  H3 : {form B}
  H4 : ctx L1 *
  ============================
   exists B, E = hyp B /\ {form B}

ctx_member < case H2.

2 subgoal(s).

  Variables: E, L, L1, B
  IH : forall E L, ctx L * -> member E L -> (exists B, E = hyp B /\ {form B})
  H3 : {form B}
  H4 : ctx L1 *
  ============================
   exists B1, hyp B = hyp B1 /\ {form B1}

subgoal 2 is:
 exists B, E = hyp B /\ {form B}

ctx_member < search.

1 subgoal(s).

  Variables: E, L, L1, B
  IH : forall E L, ctx L * -> member E L -> (exists B, E = hyp B /\ {form B})
  H3 : {form B}
  H4 : ctx L1 *
  H5 : member E L1
  ============================
   exists B, E = hyp B /\ {form B}

ctx_member < apply IH to H4 H5.

1 subgoal(s).

  Variables: E, L, L1, B, B1
  IH : forall E L, ctx L * -> member E L -> (exists B, E = hyp B /\ {form B})
  H3 : {form B}
  H4 : ctx L1 *
  H5 : member (hyp B1) L1
  H6 : {form B1}
  ============================
   exists B, hyp B1 = hyp B /\ {form B}

ctx_member < search.
Proof completed.

Abella < Theorem hyp_form : 
forall L B, ctx L -> {L |- hyp B} -> {form B}.

1 subgoal(s).

  
  ============================
   forall L B, ctx L -> {L |- hyp B} -> {form B}

hyp_form < intros.

1 subgoal(s).

  Variables: L, B
  H1 : ctx L
  H2 : {L |- hyp B}
  ============================
   {form B}

hyp_form < case H2.

1 subgoal(s).

  Variables: L, B
  H1 : ctx L
  H3 : member (hyp B) L
  ============================
   {form B}

hyp_form < apply ctx_member to H1 H3.

1 subgoal(s).

  Variables: L, B, B1
  H1 : ctx L
  H3 : member (hyp B1) L
  H4 : {form B1}
  ============================
   {form B1}

hyp_form < search.
Proof completed.

Abella < Theorem hyp_imp_form : 
forall L B1 B2, ctx L -> {L |- hyp (imp B1 B2)} -> {form B1} /\ {form B2}.

1 subgoal(s).

  
  ============================
   forall L B1 B2, ctx L -> {L |- hyp (imp B1 B2)} -> {form B1} /\ {form B2}

hyp_imp_form < intros.

1 subgoal(s).

  Variables: L, B1, B2
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  ============================
   {form B1} /\ {form B2}

hyp_imp_form < apply hyp_form to H1 H2.

1 subgoal(s).

  Variables: L, B1, B2
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form (imp B1 B2)}
  ============================
   {form B1} /\ {form B2}

hyp_imp_form < case H3.

1 subgoal(s).

  Variables: L, B1, B2
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H4 : {form B1}
  H5 : {form B2}
  ============================
   {form B1} /\ {form B2}

hyp_imp_form < search.
Proof completed.

Abella < Theorem sound : 
(forall L A B, ctx L -> {form B} -> {L |- focus B A} ->
  {L, hyp B |- conc (atom A)}) /\ (forall L B, ctx L -> {form B} ->
  {L |- unfocus B} -> {L |- conc B}).

1 subgoal(s).

  
  ============================
   (forall L A B, ctx L -> {form B} -> {L |- focus B A} ->
     {L, hyp B |- conc (atom A)}) /\ (forall L B, ctx L -> {form B} ->
     {L |- unfocus B} -> {L |- conc B})

sound < induction on 3 3.

1 subgoal(s).

  
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  ============================
   (forall L A B, ctx L -> {form B} -> {L |- focus B A}@ ->
     {L, hyp B |- conc (atom A)}) /\ (forall L B, ctx L -> {form B} ->
     {L |- unfocus B}@ -> {L |- conc B})

sound < split.

2 subgoal(s).

  
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  ============================
   forall L A B, ctx L -> {form B} -> {L |- focus B A}@ ->
     {L, hyp B |- conc (atom A)}

subgoal 2 is:
 forall L B, ctx L -> {form B} -> {L |- unfocus B}@ -> {L |- conc B}

sound < intros.

2 subgoal(s).

  Variables: L, A, B
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H2 : {form B}
  H3 : {L |- focus B A}@
  ============================
   {L, hyp B |- conc (atom A)}

subgoal 2 is:
 forall L B, ctx L -> {form B} -> {L |- unfocus B}@ -> {L |- conc B}

sound < case H3.

4 subgoal(s).

  Variables: L, A, B
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H2 : {form B}
  H4 : member (focus B A) L
  ============================
   {L, hyp B |- conc (atom A)}

subgoal 2 is:
 {L, hyp (atom A) |- conc (atom A)}

subgoal 3 is:
 {L, hyp (imp B1 C) |- conc (atom A)}

subgoal 4 is:
 forall L B, ctx L -> {form B} -> {L |- unfocus B}@ -> {L |- conc B}

sound < apply ctx_member to H1 H4.

3 subgoal(s).

  Variables: L, A, B
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H2 : {form (atom A)}
  ============================
   {L, hyp (atom A) |- conc (atom A)}

subgoal 2 is:
 {L, hyp (imp B1 C) |- conc (atom A)}

subgoal 3 is:
 forall L B, ctx L -> {form B} -> {L |- unfocus B}@ -> {L |- conc B}

sound < search.

2 subgoal(s).

  Variables: L, A, B, C, B1
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H2 : {form (imp B1 C)}
  H4 : {L |- unfocus B1}*
  H5 : {L, hyp C |- focus C A}*
  ============================
   {L, hyp (imp B1 C) |- conc (atom A)}

subgoal 2 is:
 forall L B, ctx L -> {form B} -> {L |- unfocus B}@ -> {L |- conc B}

sound < case H2.

2 subgoal(s).

  Variables: L, A, B, C, B1
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H4 : {L |- unfocus B1}*
  H5 : {L, hyp C |- focus C A}*
  H6 : {form B1}
  H7 : {form C}
  ============================
   {L, hyp (imp B1 C) |- conc (atom A)}

subgoal 2 is:
 forall L B, ctx L -> {form B} -> {L |- unfocus B}@ -> {L |- conc B}

sound < apply IH1 to H1 H6 H4.

2 subgoal(s).

  Variables: L, A, B, C, B1
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H4 : {L |- unfocus B1}*
  H5 : {L, hyp C |- focus C A}*
  H6 : {form B1}
  H7 : {form C}
  H8 : {L |- conc B1}
  ============================
   {L, hyp (imp B1 C) |- conc (atom A)}

subgoal 2 is:
 forall L B, ctx L -> {form B} -> {L |- unfocus B}@ -> {L |- conc B}

sound < apply IH to _ H7 H5.

2 subgoal(s).

  Variables: L, A, B, C, B1
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H4 : {L |- unfocus B1}*
  H5 : {L, hyp C |- focus C A}*
  H6 : {form B1}
  H7 : {form C}
  H8 : {L |- conc B1}
  H9 : {L, hyp C |- conc (atom A)}
  ============================
   {L, hyp (imp B1 C) |- conc (atom A)}

subgoal 2 is:
 forall L B, ctx L -> {form B} -> {L |- unfocus B}@ -> {L |- conc B}

sound < search.

1 subgoal(s).

  
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  ============================
   forall L B, ctx L -> {form B} -> {L |- unfocus B}@ -> {L |- conc B}

sound < intros.

1 subgoal(s).

  Variables: L, B
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H2 : {form B}
  H3 : {L |- unfocus B}@
  ============================
   {L |- conc B}

sound < case H3.

3 subgoal(s).

  Variables: L, B
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H2 : {form B}
  H4 : member (unfocus B) L
  ============================
   {L |- conc B}

subgoal 2 is:
 {L |- conc (imp B1 C)}

subgoal 3 is:
 {L |- conc (atom A)}

sound < apply ctx_member to H1 H4.

2 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H2 : {form (imp B1 C)}
  H4 : {L, hyp B1 |- unfocus C}*
  ============================
   {L |- conc (imp B1 C)}

subgoal 2 is:
 {L |- conc (atom A)}

sound < case H2.

2 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H4 : {L, hyp B1 |- unfocus C}*
  H5 : {form B1}
  H6 : {form C}
  ============================
   {L |- conc (imp B1 C)}

subgoal 2 is:
 {L |- conc (atom A)}

sound < apply IH1 to _ H6 H4.

2 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H4 : {L, hyp B1 |- unfocus C}*
  H5 : {form B1}
  H6 : {form C}
  H7 : {L, hyp B1 |- conc C}
  ============================
   {L |- conc (imp B1 C)}

subgoal 2 is:
 {L |- conc (atom A)}

sound < search.

1 subgoal(s).

  Variables: L, B, B1, A
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H2 : {form (atom A)}
  H4 : {L |- hyp B1}*
  H5 : {L |- focus B1 A}*
  ============================
   {L |- conc (atom A)}

sound < apply hyp_form to H1 H4.

1 subgoal(s).

  Variables: L, B, B1, A
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H2 : {form (atom A)}
  H4 : {L |- hyp B1}*
  H5 : {L |- focus B1 A}*
  H6 : {form B1}
  ============================
   {L |- conc (atom A)}

sound < apply IH to H1 H6 H5.

1 subgoal(s).

  Variables: L, B, B1, A
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H2 : {form (atom A)}
  H4 : {L |- hyp B1}*
  H5 : {L |- focus B1 A}*
  H6 : {form B1}
  H7 : {L, hyp B1 |- conc (atom A)}
  ============================
   {L |- conc (atom A)}

sound < cut H7 with H4.

1 subgoal(s).

  Variables: L, B, B1, A
  IH : forall L A B, ctx L -> {form B} -> {L |- focus B A}* ->
         {L, hyp B |- conc (atom A)}
  IH1 : forall L B, ctx L -> {form B} -> {L |- unfocus B}* -> {L |- conc B}
  H1 : ctx L
  H2 : {form (atom A)}
  H4 : {L |- hyp B1}*
  H5 : {L |- focus B1 A}*
  H6 : {form B1}
  H7 : {L, hyp B1 |- conc (atom A)}
  H8 : {L |- conc (atom A)}
  ============================
   {L |- conc (atom A)}

sound < search.
Proof completed.

Abella < Theorem soundness : 
forall L B, ctx L -> {form B} -> {L |- unfocus B} -> {L |- conc B}.

1 subgoal(s).

  
  ============================
   forall L B, ctx L -> {form B} -> {L |- unfocus B} -> {L |- conc B}

soundness < apply sound.

1 subgoal(s).

  
  H1 : forall L A B, ctx L -> {form B} -> {L |- focus B A} ->
         {L, hyp B |- conc (atom A)}
  H2 : forall L B, ctx L -> {form B} -> {L |- unfocus B} -> {L |- conc B}
  ============================
   forall L B, ctx L -> {form B} -> {L |- unfocus B} -> {L |- conc B}

soundness < search.
Proof completed.

Abella < Theorem init_form : 
forall L B, {form B} -> member (hyp B) L -> {L |- conc-i B}.

1 subgoal(s).

  
  ============================
   forall L B, {form B} -> member (hyp B) L -> {L |- conc-i B}

init_form < induction on 1.

1 subgoal(s).

  
  IH : forall L B, {form B}* -> member (hyp B) L -> {L |- conc-i B}
  ============================
   forall L B, {form B}@ -> member (hyp B) L -> {L |- conc-i B}

init_form < intros.

1 subgoal(s).

  Variables: L, B
  IH : forall L B, {form B}* -> member (hyp B) L -> {L |- conc-i B}
  H1 : {form B}@
  H2 : member (hyp B) L
  ============================
   {L |- conc-i B}

init_form < case H1.

2 subgoal(s).

  Variables: L, B, A
  IH : forall L B, {form B}* -> member (hyp B) L -> {L |- conc-i B}
  H2 : member (hyp (atom A)) L
  ============================
   {L |- conc-i (atom A)}

subgoal 2 is:
 {L |- conc-i (imp B1 C)}

init_form < search.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, {form B}* -> member (hyp B) L -> {L |- conc-i B}
  H2 : member (hyp (imp B1 C)) L
  H3 : {form B1}*
  H4 : {form C}*
  ============================
   {L |- conc-i (imp B1 C)}

init_form < apply IH to H3 _ with L = hyp B1 :: L.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, {form B}* -> member (hyp B) L -> {L |- conc-i B}
  H2 : member (hyp (imp B1 C)) L
  H3 : {form B1}*
  H4 : {form C}*
  H5 : {L, hyp B1 |- conc-i B1}
  ============================
   {L |- conc-i (imp B1 C)}

init_form < apply IH to H4 _ with L = hyp C :: L.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, {form B}* -> member (hyp B) L -> {L |- conc-i B}
  H2 : member (hyp (imp B1 C)) L
  H3 : {form B1}*
  H4 : {form C}*
  H5 : {L, hyp B1 |- conc-i B1}
  H6 : {L, hyp C |- conc-i C}
  ============================
   {L |- conc-i (imp B1 C)}

init_form < search.
Proof completed.

Abella < Theorem restrict_init : 
forall L B, ctx L -> {form B} -> {L |- conc B} -> {L |- conc-i B}.

1 subgoal(s).

  
  ============================
   forall L B, ctx L -> {form B} -> {L |- conc B} -> {L |- conc-i B}

restrict_init < induction on 3.

1 subgoal(s).

  
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  ============================
   forall L B, ctx L -> {form B} -> {L |- conc B}@ -> {L |- conc-i B}

restrict_init < intros.

1 subgoal(s).

  Variables: L, B
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H2 : {form B}
  H3 : {L |- conc B}@
  ============================
   {L |- conc-i B}

restrict_init < case H3.

4 subgoal(s).

  Variables: L, B
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H2 : {form B}
  H4 : member (conc B) L
  ============================
   {L |- conc-i B}

subgoal 2 is:
 {L |- conc-i B}

subgoal 3 is:
 {L |- conc-i (imp B1 C)}

subgoal 4 is:
 {L |- conc-i B}

restrict_init < apply ctx_member to H1 H4.

3 subgoal(s).

  Variables: L, B
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H2 : {form B}
  H4 : {L |- hyp B}*
  ============================
   {L |- conc-i B}

subgoal 2 is:
 {L |- conc-i (imp B1 C)}

subgoal 3 is:
 {L |- conc-i B}

restrict_init < case H4.

3 subgoal(s).

  Variables: L, B
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H2 : {form B}
  H5 : member (hyp B) L
  ============================
   {L |- conc-i B}

subgoal 2 is:
 {L |- conc-i (imp B1 C)}

subgoal 3 is:
 {L |- conc-i B}

restrict_init < apply ctx_member to H1 H5.

3 subgoal(s).

  Variables: L, B, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H2 : {form B1}
  H5 : member (hyp B1) L
  H6 : {form B1}
  ============================
   {L |- conc-i B1}

subgoal 2 is:
 {L |- conc-i (imp B1 C)}

subgoal 3 is:
 {L |- conc-i B}

restrict_init < apply init_form to H6 H5.

3 subgoal(s).

  Variables: L, B, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H2 : {form B1}
  H5 : member (hyp B1) L
  H6 : {form B1}
  H7 : {L |- conc-i B1}
  ============================
   {L |- conc-i B1}

subgoal 2 is:
 {L |- conc-i (imp B1 C)}

subgoal 3 is:
 {L |- conc-i B}

restrict_init < search.

2 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H2 : {form (imp B1 C)}
  H4 : {L, hyp B1 |- conc C}*
  ============================
   {L |- conc-i (imp B1 C)}

subgoal 2 is:
 {L |- conc-i B}

restrict_init < case H2.

2 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H4 : {L, hyp B1 |- conc C}*
  H5 : {form B1}
  H6 : {form C}
  ============================
   {L |- conc-i (imp B1 C)}

subgoal 2 is:
 {L |- conc-i B}

restrict_init < apply IH to _ H6 H4.

2 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H4 : {L, hyp B1 |- conc C}*
  H5 : {form B1}
  H6 : {form C}
  H7 : {L, hyp B1 |- conc-i C}
  ============================
   {L |- conc-i (imp B1 C)}

subgoal 2 is:
 {L |- conc-i B}

restrict_init < search.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H2 : {form B}
  H4 : {L |- hyp (imp B1 C)}*
  H5 : {L |- conc B1}*
  H6 : {L, hyp C |- conc B}*
  ============================
   {L |- conc-i B}

restrict_init < apply hyp_imp_form to H1 H4.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H2 : {form B}
  H4 : {L |- hyp (imp B1 C)}*
  H5 : {L |- conc B1}*
  H6 : {L, hyp C |- conc B}*
  H7 : {form B1}
  H8 : {form C}
  ============================
   {L |- conc-i B}

restrict_init < apply IH to H1 H7 H5.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H2 : {form B}
  H4 : {L |- hyp (imp B1 C)}*
  H5 : {L |- conc B1}*
  H6 : {L, hyp C |- conc B}*
  H7 : {form B1}
  H8 : {form C}
  H9 : {L |- conc-i B1}
  ============================
   {L |- conc-i B}

restrict_init < apply IH to _ H2 H6.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc B}* -> {L |- conc-i B}
  H1 : ctx L
  H2 : {form B}
  H4 : {L |- hyp (imp B1 C)}*
  H5 : {L |- conc B1}*
  H6 : {L, hyp C |- conc B}*
  H7 : {form B1}
  H8 : {form C}
  H9 : {L |- conc-i B1}
  H10 : {L, hyp C |- conc-i B}
  ============================
   {L |- conc-i B}

restrict_init < search.
Proof completed.

Abella < Theorem lemma : 
forall B2, (forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
  {L |- unfocus B1} -> {L, hyp B2 |- unfocus C} -> {L |- unfocus C}) /\
  (forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
  {L |- unfocus B1} -> {L, hyp B2 |- focus B A} -> {L |- focus B A}).

1 subgoal(s).

  
  ============================
   forall B2, (forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
     {L |- unfocus B1} -> {L, hyp B2 |- unfocus C} -> {L |- unfocus C}) /\
     (forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
     {L |- unfocus B1} -> {L, hyp B2 |- focus B A} -> {L |- focus B A})

lemma < intros.

1 subgoal(s).

  Variables: B2
  ============================
   (forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
     {L |- unfocus B1} -> {L, hyp B2 |- unfocus C} -> {L |- unfocus C}) /\
     (forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
     {L |- unfocus B1} -> {L, hyp B2 |- focus B A} -> {L |- focus B A})

lemma < induction on 5 5.

1 subgoal(s).

  Variables: B2
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  ============================
   (forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
     {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}@ -> {L |- unfocus C}) /\
     (forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
     {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A})

lemma < split.

2 subgoal(s).

  Variables: B2
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  ============================
   forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
     {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}@ -> {L |- unfocus C}

subgoal 2 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < intros.

2 subgoal(s).

  Variables: B2, L, B1, C
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form C}
  H4 : {L |- unfocus B1}
  H5 : {L, hyp B2 |- unfocus C}@
  ============================
   {L |- unfocus C}

subgoal 2 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < case H5.

4 subgoal(s).

  Variables: B2, L, B1, C
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form C}
  H4 : {L |- unfocus B1}
  H6 : member (unfocus C) (hyp B2 :: L)
  ============================
   {L |- unfocus C}

subgoal 2 is:
 {L |- unfocus (imp B C1)}

subgoal 3 is:
 {L |- unfocus (atom A)}

subgoal 4 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < case H6.

4 subgoal(s).

  Variables: B2, L, B1, C
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form C}
  H4 : {L |- unfocus B1}
  H7 : member (unfocus C) L
  ============================
   {L |- unfocus C}

subgoal 2 is:
 {L |- unfocus (imp B C1)}

subgoal 3 is:
 {L |- unfocus (atom A)}

subgoal 4 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < apply ctx_member to H1 H7.

3 subgoal(s).

  Variables: B2, L, B1, C, C1, B
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form (imp B C1)}
  H4 : {L |- unfocus B1}
  H6 : {L, hyp B2, hyp B |- unfocus C1}*
  ============================
   {L |- unfocus (imp B C1)}

subgoal 2 is:
 {L |- unfocus (atom A)}

subgoal 3 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < case H3.

3 subgoal(s).

  Variables: B2, L, B1, C, C1, B
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H4 : {L |- unfocus B1}
  H6 : {L, hyp B2, hyp B |- unfocus C1}*
  H7 : {form B}
  H8 : {form C1}
  ============================
   {L |- unfocus (imp B C1)}

subgoal 2 is:
 {L |- unfocus (atom A)}

subgoal 3 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < apply IH to _ _ H8 _ H6.

3 subgoal(s).

  Variables: B2, L, B1, C, C1, B
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H4 : {L |- unfocus B1}
  H6 : {L, hyp B2, hyp B |- unfocus C1}*
  H7 : {form B}
  H8 : {form C1}
  H9 : {L, hyp B |- unfocus C1}
  ============================
   {L |- unfocus (imp B C1)}

subgoal 2 is:
 {L |- unfocus (atom A)}

subgoal 3 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < search.

2 subgoal(s).

  Variables: B2, L, B1, C, B, A
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form (atom A)}
  H4 : {L |- unfocus B1}
  H6 : {L, hyp B2 |- hyp B}*
  H7 : {L, hyp B2 |- focus B A}*
  ============================
   {L |- unfocus (atom A)}

subgoal 2 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < case H6.

2 subgoal(s).

  Variables: B2, L, B1, C, B, A
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form (atom A)}
  H4 : {L |- unfocus B1}
  H7 : {L, hyp B2 |- focus B A}*
  H8 : member (hyp B) (hyp B2 :: L)
  ============================
   {L |- unfocus (atom A)}

subgoal 2 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < case H8.

3 subgoal(s).

  Variables: B2, L, B1, C, B, A
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form (atom A)}
  H4 : {L |- unfocus B1}
  H7 : {L, hyp B2 |- focus B2 A}*
  ============================
   {L |- unfocus (atom A)}

subgoal 2 is:
 {L |- unfocus (atom A)}

subgoal 3 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < search.

2 subgoal(s).

  Variables: B2, L, B1, C, B, A
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form (atom A)}
  H4 : {L |- unfocus B1}
  H7 : {L, hyp B2 |- focus B A}*
  H9 : member (hyp B) L
  ============================
   {L |- unfocus (atom A)}

subgoal 2 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < apply ctx_member to H1 H9.

2 subgoal(s).

  Variables: B2, L, B1, C, B, A, B3
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form (atom A)}
  H4 : {L |- unfocus B1}
  H7 : {L, hyp B2 |- focus B3 A}*
  H9 : member (hyp B3) L
  H10 : {form B3}
  ============================
   {L |- unfocus (atom A)}

subgoal 2 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < apply IH1 to H1 H2 H10 H4 H7.

2 subgoal(s).

  Variables: B2, L, B1, C, B, A, B3
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form (atom A)}
  H4 : {L |- unfocus B1}
  H7 : {L, hyp B2 |- focus B3 A}*
  H9 : member (hyp B3) L
  H10 : {form B3}
  H11 : {L |- focus B3 A}
  ============================
   {L |- unfocus (atom A)}

subgoal 2 is:
 forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
   {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < search.

1 subgoal(s).

  Variables: B2
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  ============================
   forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
     {L |- unfocus B1} -> {L, hyp B2 |- focus B A}@ -> {L |- focus B A}

lemma < intros.

1 subgoal(s).

  Variables: B2, L, B1, A, B
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form B}
  H4 : {L |- unfocus B1}
  H5 : {L, hyp B2 |- focus B A}@
  ============================
   {L |- focus B A}

lemma < case H5.

3 subgoal(s).

  Variables: B2, L, B1, A, B
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form B}
  H4 : {L |- unfocus B1}
  H6 : member (focus B A) (hyp B2 :: L)
  ============================
   {L |- focus B A}

subgoal 2 is:
 {L |- focus (atom A) A}

subgoal 3 is:
 {L |- focus (imp B3 C) A}

lemma < case H6.

3 subgoal(s).

  Variables: B2, L, B1, A, B
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form B}
  H4 : {L |- unfocus B1}
  H7 : member (focus B A) L
  ============================
   {L |- focus B A}

subgoal 2 is:
 {L |- focus (atom A) A}

subgoal 3 is:
 {L |- focus (imp B3 C) A}

lemma < apply ctx_member to H1 H7.

2 subgoal(s).

  Variables: B2, L, B1, A, B
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form (atom A)}
  H4 : {L |- unfocus B1}
  ============================
   {L |- focus (atom A) A}

subgoal 2 is:
 {L |- focus (imp B3 C) A}

lemma < search.

1 subgoal(s).

  Variables: B2, L, B1, A, B, C, B3
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H3 : {form (imp B3 C)}
  H4 : {L |- unfocus B1}
  H6 : {L, hyp B2 |- unfocus B3}*
  H7 : {L, hyp B2, hyp C |- focus C A}*
  ============================
   {L |- focus (imp B3 C) A}

lemma < case H3.

1 subgoal(s).

  Variables: B2, L, B1, A, B, C, B3
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H4 : {L |- unfocus B1}
  H6 : {L, hyp B2 |- unfocus B3}*
  H7 : {L, hyp B2, hyp C |- focus C A}*
  H8 : {form B3}
  H9 : {form C}
  ============================
   {L |- focus (imp B3 C) A}

lemma < apply hyp_imp_form to H1 H2.

1 subgoal(s).

  Variables: B2, L, B1, A, B, C, B3
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H4 : {L |- unfocus B1}
  H6 : {L, hyp B2 |- unfocus B3}*
  H7 : {L, hyp B2, hyp C |- focus C A}*
  H8 : {form B3}
  H9 : {form C}
  H10 : {form B1}
  H11 : {form B2}
  ============================
   {L |- focus (imp B3 C) A}

lemma < apply IH to _ _ H8 _ H6.

1 subgoal(s).

  Variables: B2, L, B1, A, B, C, B3
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H4 : {L |- unfocus B1}
  H6 : {L, hyp B2 |- unfocus B3}*
  H7 : {L, hyp B2, hyp C |- focus C A}*
  H8 : {form B3}
  H9 : {form C}
  H10 : {form B1}
  H11 : {form B2}
  H12 : {L |- unfocus B3}
  ============================
   {L |- focus (imp B3 C) A}

lemma < apply IH1 to _ _ H9 _ H7.

1 subgoal(s).

  Variables: B2, L, B1, A, B, C, B3
  IH : forall L B1 C, ctx L -> {L |- hyp (imp B1 B2)} -> {form C} ->
         {L |- unfocus B1} -> {L, hyp B2 |- unfocus C}* -> {L |- unfocus C}
  IH1 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 B2)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp B2 |- focus B A}* -> {L |- focus B A}
  H1 : ctx L
  H2 : {L |- hyp (imp B1 B2)}
  H4 : {L |- unfocus B1}
  H6 : {L, hyp B2 |- unfocus B3}*
  H7 : {L, hyp B2, hyp C |- focus C A}*
  H8 : {form B3}
  H9 : {form C}
  H10 : {form B1}
  H11 : {form B2}
  H12 : {L |- unfocus B3}
  H13 : {L, hyp C |- focus C A}
  ============================
   {L |- focus (imp B3 C) A}

lemma < search.
Proof completed.

Abella < Theorem conc-i_complete : 
forall L B, ctx L -> {form B} -> {L |- conc-i B} -> {L |- unfocus B}.

1 subgoal(s).

  
  ============================
   forall L B, ctx L -> {form B} -> {L |- conc-i B} -> {L |- unfocus B}

conc-i_complete < induction on 3.

1 subgoal(s).

  
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  ============================
   forall L B, ctx L -> {form B} -> {L |- conc-i B}@ -> {L |- unfocus B}

conc-i_complete < intros.

1 subgoal(s).

  Variables: L, B
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H2 : {form B}
  H3 : {L |- conc-i B}@
  ============================
   {L |- unfocus B}

conc-i_complete < case H3.

4 subgoal(s).

  Variables: L, B
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H2 : {form B}
  H4 : member (conc-i B) L
  ============================
   {L |- unfocus B}

subgoal 2 is:
 {L |- unfocus (atom A)}

subgoal 3 is:
 {L |- unfocus (imp B1 C)}

subgoal 4 is:
 {L |- unfocus B}

conc-i_complete < apply ctx_member to H1 H4.

3 subgoal(s).

  Variables: L, B, A
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H2 : {form (atom A)}
  H4 : {L |- hyp (atom A)}*
  ============================
   {L |- unfocus (atom A)}

subgoal 2 is:
 {L |- unfocus (imp B1 C)}

subgoal 3 is:
 {L |- unfocus B}

conc-i_complete < search.

2 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H2 : {form (imp B1 C)}
  H4 : {L, hyp B1 |- conc-i C}*
  ============================
   {L |- unfocus (imp B1 C)}

subgoal 2 is:
 {L |- unfocus B}

conc-i_complete < case H2.

2 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H4 : {L, hyp B1 |- conc-i C}*
  H5 : {form B1}
  H6 : {form C}
  ============================
   {L |- unfocus (imp B1 C)}

subgoal 2 is:
 {L |- unfocus B}

conc-i_complete < apply IH to _ H6 H4.

2 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H4 : {L, hyp B1 |- conc-i C}*
  H5 : {form B1}
  H6 : {form C}
  H7 : {L, hyp B1 |- unfocus C}
  ============================
   {L |- unfocus (imp B1 C)}

subgoal 2 is:
 {L |- unfocus B}

conc-i_complete < search.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H2 : {form B}
  H4 : {L |- hyp (imp B1 C)}*
  H5 : {L |- conc-i B1}*
  H6 : {L, hyp C |- conc-i B}*
  ============================
   {L |- unfocus B}

conc-i_complete < apply hyp_imp_form to H1 H4.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H2 : {form B}
  H4 : {L |- hyp (imp B1 C)}*
  H5 : {L |- conc-i B1}*
  H6 : {L, hyp C |- conc-i B}*
  H7 : {form B1}
  H8 : {form C}
  ============================
   {L |- unfocus B}

conc-i_complete < apply IH to H1 H7 H5.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H2 : {form B}
  H4 : {L |- hyp (imp B1 C)}*
  H5 : {L |- conc-i B1}*
  H6 : {L, hyp C |- conc-i B}*
  H7 : {form B1}
  H8 : {form C}
  H9 : {L |- unfocus B1}
  ============================
   {L |- unfocus B}

conc-i_complete < apply IH to _ H2 H6.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H2 : {form B}
  H4 : {L |- hyp (imp B1 C)}*
  H5 : {L |- conc-i B1}*
  H6 : {L, hyp C |- conc-i B}*
  H7 : {form B1}
  H8 : {form C}
  H9 : {L |- unfocus B1}
  H10 : {L, hyp C |- unfocus B}
  ============================
   {L |- unfocus B}

conc-i_complete < apply lemma with B2 = C.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H2 : {form B}
  H4 : {L |- hyp (imp B1 C)}*
  H5 : {L |- conc-i B1}*
  H6 : {L, hyp C |- conc-i B}*
  H7 : {form B1}
  H8 : {form C}
  H9 : {L |- unfocus B1}
  H10 : {L, hyp C |- unfocus B}
  H11 : forall L B1 C1, ctx L -> {L |- hyp (imp B1 C)} -> {form C1} ->
          {L |- unfocus B1} -> {L, hyp C |- unfocus C1} -> {L |- unfocus C1}
  H12 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 C)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp C |- focus B A} -> {L |- focus B A}
  ============================
   {L |- unfocus B}

conc-i_complete < apply H11 to H1 H4 H2 H9 H10.

1 subgoal(s).

  Variables: L, B, C, B1
  IH : forall L B, ctx L -> {form B} -> {L |- conc-i B}* -> {L |- unfocus B}
  H1 : ctx L
  H2 : {form B}
  H4 : {L |- hyp (imp B1 C)}*
  H5 : {L |- conc-i B1}*
  H6 : {L, hyp C |- conc-i B}*
  H7 : {form B1}
  H8 : {form C}
  H9 : {L |- unfocus B1}
  H10 : {L, hyp C |- unfocus B}
  H11 : forall L B1 C1, ctx L -> {L |- hyp (imp B1 C)} -> {form C1} ->
          {L |- unfocus B1} -> {L, hyp C |- unfocus C1} -> {L |- unfocus C1}
  H12 : forall L B1 A B, ctx L -> {L |- hyp (imp B1 C)} -> {form B} ->
          {L |- unfocus B1} -> {L, hyp C |- focus B A} -> {L |- focus B A}
  H13 : {L |- unfocus B}
  ============================
   {L |- unfocus B}

conc-i_complete < search.
Proof completed.

Abella < Theorem completeness : 
forall L B, ctx L -> {form B} -> {L |- conc B} -> {L |- unfocus B}.

1 subgoal(s).

  
  ============================
   forall L B, ctx L -> {form B} -> {L |- conc B} -> {L |- unfocus B}

completeness < intros.

1 subgoal(s).

  Variables: L, B
  H1 : ctx L
  H2 : {form B}
  H3 : {L |- conc B}
  ============================
   {L |- unfocus B}

completeness < apply restrict_init to H1 H2 H3.

1 subgoal(s).

  Variables: L, B
  H1 : ctx L
  H2 : {form B}
  H3 : {L |- conc B}
  H4 : {L |- conc-i B}
  ============================
   {L |- unfocus B}

completeness < apply conc-i_complete to H1 H2 H4.

1 subgoal(s).

  Variables: L, B
  H1 : ctx L
  H2 : {form B}
  H3 : {L |- conc B}
  H4 : {L |- conc-i B}
  H5 : {L |- unfocus B}
  ============================
   {L |- unfocus B}

completeness < search.
Proof completed.

Abella < Goodbye.