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

Abella < Theorem deduction : 
forall L A B, {L, comb A |- comb B} -> {L |- comb (imp A B)}.

1 subgoal(s).

  
  ============================
   forall L A B, {L, comb A |- comb B} -> {L |- comb (imp A B)}

deduction < induction on 1.

1 subgoal(s).

  
  IH : forall L A B, {L, comb A |- comb B}* -> {L |- comb (imp A B)}
  ============================
   forall L A B, {L, comb A |- comb B}@ -> {L |- comb (imp A B)}

deduction < intros.

1 subgoal(s).

  Variables: L, A, B
  IH : forall L A B, {L, comb A |- comb B}* -> {L |- comb (imp A B)}
  H1 : {L, comb A |- comb B}@
  ============================
   {L |- comb (imp A B)}

deduction < case H1.

4 subgoal(s).

  Variables: L, A, B
  IH : forall L A B, {L, comb A |- comb B}* -> {L |- comb (imp A B)}
  H2 : member (comb B) (comb A :: L)
  ============================
   {L |- comb (imp A B)}

subgoal 2 is:
 {L |- comb (imp A (imp A1 (imp B1 A1)))}

subgoal 3 is:
 {L |- comb (imp A (imp (imp A1 (imp B1 C)) (imp (imp A1 B1) (imp A1 C))))}

subgoal 4 is:
 {L |- comb (imp A B)}

deduction < case H2.

5 subgoal(s).

  Variables: L, A, B
  IH : forall L A B, {L, comb A |- comb B}* -> {L |- comb (imp A B)}
  ============================
   {L |- comb (imp A A)}

subgoal 2 is:
 {L |- comb (imp A B)}

subgoal 3 is:
 {L |- comb (imp A (imp A1 (imp B1 A1)))}

subgoal 4 is:
 {L |- comb (imp A (imp (imp A1 (imp B1 C)) (imp (imp A1 B1) (imp A1 C))))}

subgoal 5 is:
 {L |- comb (imp A B)}

deduction < search.

4 subgoal(s).

  Variables: L, A, B
  IH : forall L A B, {L, comb A |- comb B}* -> {L |- comb (imp A B)}
  H3 : member (comb B) L
  ============================
   {L |- comb (imp A B)}

subgoal 2 is:
 {L |- comb (imp A (imp A1 (imp B1 A1)))}

subgoal 3 is:
 {L |- comb (imp A (imp (imp A1 (imp B1 C)) (imp (imp A1 B1) (imp A1 C))))}

subgoal 4 is:
 {L |- comb (imp A B)}

deduction < search.

3 subgoal(s).

  Variables: L, A, B, B1, A1
  IH : forall L A B, {L, comb A |- comb B}* -> {L |- comb (imp A B)}
  ============================
   {L |- comb (imp A (imp A1 (imp B1 A1)))}

subgoal 2 is:
 {L |- comb (imp A (imp (imp A1 (imp B1 C)) (imp (imp A1 B1) (imp A1 C))))}

subgoal 3 is:
 {L |- comb (imp A B)}

deduction < search.

2 subgoal(s).

  Variables: L, A, B, C, B1, A1
  IH : forall L A B, {L, comb A |- comb B}* -> {L |- comb (imp A B)}
  ============================
   {L |- comb (imp A (imp (imp A1 (imp B1 C)) (imp (imp A1 B1) (imp A1 C))))}

subgoal 2 is:
 {L |- comb (imp A B)}

deduction < search.

1 subgoal(s).

  Variables: L, A, B, A1
  IH : forall L A B, {L, comb A |- comb B}* -> {L |- comb (imp A B)}
  H2 : {L, comb A |- comb (imp A1 B)}*
  H3 : {L, comb A |- comb A1}*
  ============================
   {L |- comb (imp A B)}

deduction < apply IH to H2.

1 subgoal(s).

  Variables: L, A, B, A1
  IH : forall L A B, {L, comb A |- comb B}* -> {L |- comb (imp A B)}
  H2 : {L, comb A |- comb (imp A1 B)}*
  H3 : {L, comb A |- comb A1}*
  H4 : {L |- comb (imp A (imp A1 B))}
  ============================
   {L |- comb (imp A B)}

deduction < apply IH to H3.

1 subgoal(s).

  Variables: L, A, B, A1
  IH : forall L A B, {L, comb A |- comb B}* -> {L |- comb (imp A B)}
  H2 : {L, comb A |- comb (imp A1 B)}*
  H3 : {L, comb A |- comb A1}*
  H4 : {L |- comb (imp A (imp A1 B))}
  H5 : {L |- comb (imp A A1)}
  ============================
   {L |- comb (imp A B)}

deduction < search.
Proof completed.

Abella < Define fold nil B B.

Abella < Define fold (comb A :: L) B B' := fold L (imp A B) B'.

Abella < Theorem deduction_generalized : 
forall L B B', fold L B B' -> {L |- comb B} -> {comb B'}.

1 subgoal(s).

  
  ============================
   forall L B B', fold L B B' -> {L |- comb B} -> {comb B'}

deduction_generalized < induction on 1.

1 subgoal(s).

  
  IH : forall L B B', fold L B B' * -> {L |- comb B} -> {comb B'}
  ============================
   forall L B B', fold L B B' @ -> {L |- comb B} -> {comb B'}

deduction_generalized < intros.

1 subgoal(s).

  Variables: L, B, B'
  IH : forall L B B', fold L B B' * -> {L |- comb B} -> {comb B'}
  H1 : fold L B B' @
  H2 : {L |- comb B}
  ============================
   {comb B'}

deduction_generalized < case H1.

2 subgoal(s).

  Variables: L, B, B'
  IH : forall L B B', fold L B B' * -> {L |- comb B} -> {comb B'}
  H2 : {comb B'}
  ============================
   {comb B'}

subgoal 2 is:
 {comb B'}

deduction_generalized < search.

1 subgoal(s).

  Variables: L, B, B', L1, A
  IH : forall L B B', fold L B B' * -> {L |- comb B} -> {comb B'}
  H2 : {L1, comb A |- comb B}
  H3 : fold L1 (imp A B) B' *
  ============================
   {comb B'}

deduction_generalized < apply deduction to H2.

1 subgoal(s).

  Variables: L, B, B', L1, A
  IH : forall L B B', fold L B B' * -> {L |- comb B} -> {comb B'}
  H2 : {L1, comb A |- comb B}
  H3 : fold L1 (imp A B) B' *
  H4 : {L1 |- comb (imp A B)}
  ============================
   {comb B'}

deduction_generalized < apply IH to H3 H4.

1 subgoal(s).

  Variables: L, B, B', L1, A
  IH : forall L B B', fold L B B' * -> {L |- comb B} -> {comb B'}
  H2 : {L1, comb A |- comb B}
  H3 : fold L1 (imp A B) B' *
  H4 : {L1 |- comb (imp A B)}
  H5 : {comb B'}
  ============================
   {comb B'}

deduction_generalized < search.
Proof completed.

Abella < Define ctxs nil nil.

Abella < Define ctxs (nd D :: L) (comb D :: K) := ctxs L K.

Abella < Theorem ctxs_world : 
forall L K D, ctxs L K -> member (nd D) L -> member (comb D) K.

1 subgoal(s).

  
  ============================
   forall L K D, ctxs L K -> member (nd D) L -> member (comb D) K

ctxs_world < induction on 2.

1 subgoal(s).

  
  IH : forall L K D, ctxs L K -> member (nd D) L * -> member (comb D) K
  ============================
   forall L K D, ctxs L K -> member (nd D) L @ -> member (comb D) K

ctxs_world < intros.

1 subgoal(s).

  Variables: L, K, D
  IH : forall L K D, ctxs L K -> member (nd D) L * -> member (comb D) K
  H1 : ctxs L K
  H2 : member (nd D) L @
  ============================
   member (comb D) K

ctxs_world < case H2.

2 subgoal(s).

  Variables: L, K, D, L1
  IH : forall L K D, ctxs L K -> member (nd D) L * -> member (comb D) K
  H1 : ctxs (nd D :: L1) K
  ============================
   member (comb D) K

subgoal 2 is:
 member (comb D) K

ctxs_world < case H1.

2 subgoal(s).

  Variables: L, K, D, L1, K1
  IH : forall L K D, ctxs L K -> member (nd D) L * -> member (comb D) K
  H3 : ctxs L1 K1
  ============================
   member (comb D) (comb D :: K1)

subgoal 2 is:
 member (comb D) K

ctxs_world < search.

1 subgoal(s).

  Variables: L, K, D, L1, B
  IH : forall L K D, ctxs L K -> member (nd D) L * -> member (comb D) K
  H1 : ctxs (B :: L1) K
  H3 : member (nd D) L1 *
  ============================
   member (comb D) K

ctxs_world < case H1.

1 subgoal(s).

  Variables: L, K, D, L1, B, K1, D1
  IH : forall L K D, ctxs L K -> member (nd D) L * -> member (comb D) K
  H3 : member (nd D) L1 *
  H4 : ctxs L1 K1
  ============================
   member (comb D) (comb D1 :: K1)

ctxs_world < apply IH to H4 H3.

1 subgoal(s).

  Variables: L, K, D, L1, B, K1, D1
  IH : forall L K D, ctxs L K -> member (nd D) L * -> member (comb D) K
  H3 : member (nd D) L1 *
  H4 : ctxs L1 K1
  H5 : member (comb D) K1
  ============================
   member (comb D) (comb D1 :: K1)

ctxs_world < search.
Proof completed.

Abella < Theorem nd_implies_comb_generalize : 
forall L K D, ctxs L K -> {L |- nd D} -> {K |- comb D}.

1 subgoal(s).

  
  ============================
   forall L K D, ctxs L K -> {L |- nd D} -> {K |- comb D}

nd_implies_comb_generalize < induction on 2.

1 subgoal(s).

  
  IH : forall L K D, ctxs L K -> {L |- nd D}* -> {K |- comb D}
  ============================
   forall L K D, ctxs L K -> {L |- nd D}@ -> {K |- comb D}

nd_implies_comb_generalize < intros.

1 subgoal(s).

  Variables: L, K, D
  IH : forall L K D, ctxs L K -> {L |- nd D}* -> {K |- comb D}
  H1 : ctxs L K
  H2 : {L |- nd D}@
  ============================
   {K |- comb D}

nd_implies_comb_generalize < case H2.

3 subgoal(s).

  Variables: L, K, D
  IH : forall L K D, ctxs L K -> {L |- nd D}* -> {K |- comb D}
  H1 : ctxs L K
  H3 : member (nd D) L
  ============================
   {K |- comb D}

subgoal 2 is:
 {K |- comb (imp A B)}

subgoal 3 is:
 {K |- comb D}

nd_implies_comb_generalize < apply ctxs_world to H1 H3.

3 subgoal(s).

  Variables: L, K, D
  IH : forall L K D, ctxs L K -> {L |- nd D}* -> {K |- comb D}
  H1 : ctxs L K
  H3 : member (nd D) L
  H4 : member (comb D) K
  ============================
   {K |- comb D}

subgoal 2 is:
 {K |- comb (imp A B)}

subgoal 3 is:
 {K |- comb D}

nd_implies_comb_generalize < search.

2 subgoal(s).

  Variables: L, K, D, B, A
  IH : forall L K D, ctxs L K -> {L |- nd D}* -> {K |- comb D}
  H1 : ctxs L K
  H3 : {L, nd A |- nd B}*
  ============================
   {K |- comb (imp A B)}

subgoal 2 is:
 {K |- comb D}

nd_implies_comb_generalize < apply IH to _ H3.

2 subgoal(s).

  Variables: L, K, D, B, A
  IH : forall L K D, ctxs L K -> {L |- nd D}* -> {K |- comb D}
  H1 : ctxs L K
  H3 : {L, nd A |- nd B}*
  H4 : {K, comb A |- comb B}
  ============================
   {K |- comb (imp A B)}

subgoal 2 is:
 {K |- comb D}

nd_implies_comb_generalize < apply deduction to H4.

2 subgoal(s).

  Variables: L, K, D, B, A
  IH : forall L K D, ctxs L K -> {L |- nd D}* -> {K |- comb D}
  H1 : ctxs L K
  H3 : {L, nd A |- nd B}*
  H4 : {K, comb A |- comb B}
  H5 : {K |- comb (imp A B)}
  ============================
   {K |- comb (imp A B)}

subgoal 2 is:
 {K |- comb D}

nd_implies_comb_generalize < search.

1 subgoal(s).

  Variables: L, K, D, A
  IH : forall L K D, ctxs L K -> {L |- nd D}* -> {K |- comb D}
  H1 : ctxs L K
  H3 : {L |- nd (imp A D)}*
  H4 : {L |- nd A}*
  ============================
   {K |- comb D}

nd_implies_comb_generalize < apply IH to H1 H3.

1 subgoal(s).

  Variables: L, K, D, A
  IH : forall L K D, ctxs L K -> {L |- nd D}* -> {K |- comb D}
  H1 : ctxs L K
  H3 : {L |- nd (imp A D)}*
  H4 : {L |- nd A}*
  H5 : {K |- comb (imp A D)}
  ============================
   {K |- comb D}

nd_implies_comb_generalize < apply IH to H1 H4.

1 subgoal(s).

  Variables: L, K, D, A
  IH : forall L K D, ctxs L K -> {L |- nd D}* -> {K |- comb D}
  H1 : ctxs L K
  H3 : {L |- nd (imp A D)}*
  H4 : {L |- nd A}*
  H5 : {K |- comb (imp A D)}
  H6 : {K |- comb A}
  ============================
   {K |- comb D}

nd_implies_comb_generalize < search.
Proof completed.

Abella < Theorem nd_implies_comb : 
forall D, {nd D} -> {comb D}.

1 subgoal(s).

  
  ============================
   forall D, {nd D} -> {comb D}

nd_implies_comb < intros.

1 subgoal(s).

  Variables: D
  H1 : {nd D}
  ============================
   {comb D}

nd_implies_comb < apply nd_implies_comb_generalize to _ H1.

1 subgoal(s).

  Variables: D
  H1 : {nd D}
  H2 : {comb D}
  ============================
   {comb D}

nd_implies_comb < search.
Proof completed.

Abella < Theorem comb_implies_nd : 
forall D, {comb D} -> {nd D}.

1 subgoal(s).

  
  ============================
   forall D, {comb D} -> {nd D}

comb_implies_nd < induction on 1.

1 subgoal(s).

  
  IH : forall D, {comb D}* -> {nd D}
  ============================
   forall D, {comb D}@ -> {nd D}

comb_implies_nd < intros.

1 subgoal(s).

  Variables: D
  IH : forall D, {comb D}* -> {nd D}
  H1 : {comb D}@
  ============================
   {nd D}

comb_implies_nd < case H1.

3 subgoal(s).

  Variables: D, B, A
  IH : forall D, {comb D}* -> {nd D}
  ============================
   {nd (imp A (imp B A))}

subgoal 2 is:
 {nd (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))}

subgoal 3 is:
 {nd D}

comb_implies_nd < search.

2 subgoal(s).

  Variables: D, C, B, A
  IH : forall D, {comb D}* -> {nd D}
  ============================
   {nd (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))}

subgoal 2 is:
 {nd D}

comb_implies_nd < assert {nd (imp A (imp B C)), nd (imp A B), nd A |- nd C}.

2 subgoal(s).

  Variables: D, C, B, A
  IH : forall D, {comb D}* -> {nd D}
  H2 : {nd (imp A (imp B C)), nd (imp A B), nd A |- nd C}
  ============================
   {nd (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))}

subgoal 2 is:
 {nd D}

comb_implies_nd < search.

1 subgoal(s).

  Variables: D, A
  IH : forall D, {comb D}* -> {nd D}
  H2 : {comb (imp A D)}*
  H3 : {comb A}*
  ============================
   {nd D}

comb_implies_nd < apply IH to H2.

1 subgoal(s).

  Variables: D, A
  IH : forall D, {comb D}* -> {nd D}
  H2 : {comb (imp A D)}*
  H3 : {comb A}*
  H4 : {nd (imp A D)}
  ============================
   {nd D}

comb_implies_nd < apply IH to H3.

1 subgoal(s).

  Variables: D, A
  IH : forall D, {comb D}* -> {nd D}
  H2 : {comb (imp A D)}*
  H3 : {comb A}*
  H4 : {nd (imp A D)}
  H5 : {nd A}
  ============================
   {nd D}

comb_implies_nd < search.
Proof completed.

Abella < Goodbye.