Welcome to Abella 2.0.5-dev.
Abella < Define remove : olist -> o -> olist -> prop by 
remove (A :: G) A G;
remove (B :: G) A (B :: D) := remove G A D.

Abella < Theorem remove_incl : 
forall G D A B, remove G A D -> member B D -> member B G.


============================
 forall G D A B, remove G A D -> member B D -> member B G

remove_incl < induction on 1.

IH : forall G D A B, remove G A D * -> member B D -> member B G
============================
 forall G D A B, remove G A D @ -> member B D -> member B G

remove_incl < intros.

Variables: G D A B
IH : forall G D A B, remove G A D * -> member B D -> member B G
H1 : remove G A D @
H2 : member B D
============================
 member B G

remove_incl < case H1.
Subgoal 1:

Variables: D A B
IH : forall G D A B, remove G A D * -> member B D -> member B G
H2 : member B D
============================
 member B (A :: D)

Subgoal 2 is:
 member B (B1 :: G1)

remove_incl < search.
Subgoal 2:

Variables: A B D1 B1 G1
IH : forall G D A B, remove G A D * -> member B D -> member B G
H2 : member B (B1 :: D1)
H3 : remove G1 A D1 *
============================
 member B (B1 :: G1)

remove_incl < case H2.
Subgoal 2.1:

Variables: A D1 B1 G1
IH : forall G D A B, remove G A D * -> member B D -> member B G
H3 : remove G1 A D1 *
============================
 member B1 (B1 :: G1)

Subgoal 2.2 is:
 member B (B1 :: G1)

remove_incl < search.
Subgoal 2.2:

Variables: A B D1 B1 G1
IH : forall G D A B, remove G A D * -> member B D -> member B G
H3 : remove G1 A D1 *
H4 : member B D1
============================
 member B (B1 :: G1)

remove_incl < apply IH to H3 H4.
Subgoal 2.2:

Variables: A B D1 B1 G1
IH : forall G D A B, remove G A D * -> member B D -> member B G
H3 : remove G1 A D1 *
H4 : member B D1
H5 : member B G1
============================
 member B (B1 :: G1)

remove_incl < search.
Proof completed.
Abella < Theorem remove_charac : 
forall G A D B, remove G A D -> member B G -> A = B \/ member B D.


============================
 forall G A D B, remove G A D -> member B G -> A = B \/ member B D

remove_charac < induction on 1.

IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
============================
 forall G A D B, remove G A D @ -> member B G -> A = B \/ member B D

remove_charac < intros.

Variables: G A D B
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove G A D @
H2 : member B G
============================
 A = B \/ member B D

remove_charac < case H1 (keep).
Subgoal 1:

Variables: A D B
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (A :: D) A D @
H2 : member B (A :: D)
============================
 A = B \/ member B D

Subgoal 2 is:
 A = B \/ member B (B1 :: D1)

remove_charac < case H2.
Subgoal 1.1:

Variables: A D
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (A :: D) A D @
============================
 A = A \/ member A D

Subgoal 1.2 is:
 A = B \/ member B D

Subgoal 2 is:
 A = B \/ member B (B1 :: D1)

remove_charac < search.
Subgoal 1.2:

Variables: A D B
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (A :: D) A D @
H3 : member B D
============================
 A = B \/ member B D

Subgoal 2 is:
 A = B \/ member B (B1 :: D1)

remove_charac < search.
Subgoal 2:

Variables: A B D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) A (B1 :: D1) @
H2 : member B (B1 :: G1)
H3 : remove G1 A D1 *
============================
 A = B \/ member B (B1 :: D1)

remove_charac < case H2.
Subgoal 2.1:

Variables: A D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) A (B1 :: D1) @
H3 : remove G1 A D1 *
============================
 A = B1 \/ member B1 (B1 :: D1)

Subgoal 2.2 is:
 A = B \/ member B (B1 :: D1)

remove_charac < search.
Subgoal 2.2:

Variables: A B D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) A (B1 :: D1) @
H3 : remove G1 A D1 *
H4 : member B G1
============================
 A = B \/ member B (B1 :: D1)

remove_charac < apply IH to H3 H4.
Subgoal 2.2:

Variables: A B D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) A (B1 :: D1) @
H3 : remove G1 A D1 *
H4 : member B G1
H5 : A = B \/ member B D1
============================
 A = B \/ member B (B1 :: D1)

remove_charac < case H5.
Subgoal 2.2.1:

Variables: B D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) B (B1 :: D1) @
H3 : remove G1 B D1 *
H4 : member B G1
============================
 B = B \/ member B (B1 :: D1)

Subgoal 2.2.2 is:
 A = B \/ member B (B1 :: D1)

remove_charac < search.
Subgoal 2.2.2:

Variables: A B D1 B1 G1
IH : forall G A D B, remove G A D * -> member B G -> A = B \/ member B D
H1 : remove (B1 :: G1) A (B1 :: D1) @
H3 : remove G1 A D1 *
H4 : member B G1
H6 : member B D1
============================
 A = B \/ member B (B1 :: D1)

remove_charac < search.
Proof completed.
Abella < Kind fm, tm type.

Abella < Type atm tm -> fm.

Abella < Type and fm -> fm -> fm.

Abella < Type top fm.

Abella < Type imp fm -> fm -> fm.

Abella < Type all (tm -> fm) -> fm.

Abella < Type $fm fm -> o.

Abella < Define is_fm : fm -> prop by 
is_fm (atm A);
is_fm (and A B) := is_fm A /\ is_fm B;
is_fm top;
is_fm (imp A B) := is_fm A /\ is_fm B;
is_fm (all A) := forall x, is_fm (A x).

Abella < Type prog fm -> prop.

Abella < Theorem prog_has_no_nablas : 
forall F, nabla n, prog (F n) -> (exists E, F = x\E).


============================
 forall F, nabla n, prog (F n) -> (exists E, F = x\E)

prog_has_no_nablas < skip.
Proof completed.
Abella < Define seq : olist -> fm -> prop,	
bch : olist -> fm -> tm -> prop by 
seq L (atm A) := exists F, member ($fm F) L /\ bch L F A;
seq L (atm A) := exists F, prog F /\ bch L F A;
seq L (and G1 G2) := seq L G1 /\ seq L G2;
seq L top;
seq L (imp F G) := seq ($fm F :: L) G;
seq L (all A) := nabla x, seq L (A x);
bch L (atm A) A;
bch L (and F1 F2) A := bch L F1 A \/ bch L F2 A;
bch L (imp G F) A := seq L G /\ bch L F A;
bch L (all F) A := exists t, bch L (F t) A.

Abella < Theorem $monotone : 
(forall L L' C, (forall E, member E L -> member E L') -> seq L C -> seq L' C) /\
  (forall L L' F A, (forall E, member E L -> member E L') -> bch L F A ->
       bch L' F A).


============================
 (forall L L' C, (forall E, member E L -> member E L') -> seq L C ->
      seq L' C) /\
   (forall L L' F A, (forall E, member E L -> member E L') -> bch L F A ->
        bch L' F A)

$monotone < induction on 2 2.

IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
============================
 (forall L L' C, (forall E, member E L -> member E L') -> seq L C @ ->
      seq L' C) /\
   (forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
        bch L' F A)

$monotone < split.
Subgoal 1:

IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
============================
 forall L L' C, (forall E, member E L -> member E L') -> seq L C @ ->
   seq L' C

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < intros.
Subgoal 1:

Variables: L L' C
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L C @
============================
 seq L' C

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < case H2 (keep).
Subgoal 1.1:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (atm A) @
H3 : member ($fm F) L
H4 : bch L F A *
============================
 seq L' (atm A)

Subgoal 1.2 is:
 seq L' (atm A)

Subgoal 1.3 is:
 seq L' (and G1 G2)

Subgoal 1.4 is:
 seq L' top

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < apply IH1 to H1 H4.
Subgoal 1.1:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (atm A) @
H3 : member ($fm F) L
H4 : bch L F A *
H5 : bch L' F A
============================
 seq L' (atm A)

Subgoal 1.2 is:
 seq L' (atm A)

Subgoal 1.3 is:
 seq L' (and G1 G2)

Subgoal 1.4 is:
 seq L' top

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < apply H1 to H3.
Subgoal 1.1:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (atm A) @
H3 : member ($fm F) L
H4 : bch L F A *
H5 : bch L' F A
H6 : member ($fm F) L'
============================
 seq L' (atm A)

Subgoal 1.2 is:
 seq L' (atm A)

Subgoal 1.3 is:
 seq L' (and G1 G2)

Subgoal 1.4 is:
 seq L' top

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < search.
Subgoal 1.2:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (atm A) @
H3 : prog F
H4 : bch L F A *
============================
 seq L' (atm A)

Subgoal 1.3 is:
 seq L' (and G1 G2)

Subgoal 1.4 is:
 seq L' top

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < apply IH1 to H1 H4.
Subgoal 1.2:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (atm A) @
H3 : prog F
H4 : bch L F A *
H5 : bch L' F A
============================
 seq L' (atm A)

Subgoal 1.3 is:
 seq L' (and G1 G2)

Subgoal 1.4 is:
 seq L' top

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < search.
Subgoal 1.3:

Variables: L L' G2 G1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (and G1 G2) @
H3 : seq L G1 *
H4 : seq L G2 *
============================
 seq L' (and G1 G2)

Subgoal 1.4 is:
 seq L' top

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < apply IH to H1 H3.
Subgoal 1.3:

Variables: L L' G2 G1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (and G1 G2) @
H3 : seq L G1 *
H4 : seq L G2 *
H5 : seq L' G1
============================
 seq L' (and G1 G2)

Subgoal 1.4 is:
 seq L' top

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < apply IH to H1 H4.
Subgoal 1.3:

Variables: L L' G2 G1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (and G1 G2) @
H3 : seq L G1 *
H4 : seq L G2 *
H5 : seq L' G1
H6 : seq L' G2
============================
 seq L' (and G1 G2)

Subgoal 1.4 is:
 seq L' top

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < search.
Subgoal 1.4:

Variables: L L'
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L top @
============================
 seq L' top

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < search.
Subgoal 1.5:

Variables: L L' G F
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq ($fm F :: L) G *
============================
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < assert forall E, member E ($fm F :: L) -> member E ($fm F :: L').
Subgoal 1.5.1:

Variables: L L' G F
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq ($fm F :: L) G *
============================
 forall E, member E ($fm F :: L) -> member E ($fm F :: L')

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < intros.
Subgoal 1.5.1:

Variables: L L' G F E
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq ($fm F :: L) G *
H4 : member E ($fm F :: L)
============================
 member E ($fm F :: L')

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < case H4.
Subgoal 1.5.1.1:

Variables: L L' G F
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq ($fm F :: L) G *
============================
 member ($fm F) ($fm F :: L')

Subgoal 1.5.1.2 is:
 member E ($fm F :: L')

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < search.
Subgoal 1.5.1.2:

Variables: L L' G F E
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq ($fm F :: L) G *
H5 : member E L
============================
 member E ($fm F :: L')

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < apply H1 to H5.
Subgoal 1.5.1.2:

Variables: L L' G F E
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq ($fm F :: L) G *
H5 : member E L
H6 : member E L'
============================
 member E ($fm F :: L')

Subgoal 1.5 is:
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < search.
Subgoal 1.5:

Variables: L L' G F
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq ($fm F :: L) G *
H4 : forall E, member E ($fm F :: L) -> member E ($fm F :: L')
============================
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < apply IH to H4 H3.
Subgoal 1.5:

Variables: L L' G F
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (imp F G) @
H3 : seq ($fm F :: L) G *
H4 : forall E, member E ($fm F :: L) -> member E ($fm F :: L')
H5 : seq ($fm F :: L') G
============================
 seq L' (imp F G)

Subgoal 1.6 is:
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < search.
Subgoal 1.6:

Variables: L L' A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (all A) @
H3 : seq L (A n1) *
============================
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < apply IH to H1 H3.
Subgoal 1.6:

Variables: L L' A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : seq L (all A) @
H3 : seq L (A n1) *
H4 : seq L' (A n1)
============================
 seq L' (all A)

Subgoal 2 is:
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < search.
Subgoal 2:

IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
============================
 forall L L' F A, (forall E, member E L -> member E L') -> bch L F A @ ->
   bch L' F A

$monotone < intros.
Subgoal 2:

Variables: L L' F A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L F A @
============================
 bch L' F A

$monotone < case H2 (keep).
Subgoal 2.1:

Variables: L L' A
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (atm A) A @
============================
 bch L' (atm A) A

Subgoal 2.2 is:
 bch L' (and F1 F2) A

Subgoal 2.3 is:
 bch L' (imp G F1) A

Subgoal 2.4 is:
 bch L' (all F1) A

$monotone < search.
Subgoal 2.2:

Variables: L L' A F2 F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (and F1 F2) A @
H3 : bch L F1 A * \/ bch L F2 A *
============================
 bch L' (and F1 F2) A

Subgoal 2.3 is:
 bch L' (imp G F1) A

Subgoal 2.4 is:
 bch L' (all F1) A

$monotone < case H3.
Subgoal 2.2.1:

Variables: L L' A F2 F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (and F1 F2) A @
H4 : bch L F1 A *
============================
 bch L' (and F1 F2) A

Subgoal 2.2.2 is:
 bch L' (and F1 F2) A

Subgoal 2.3 is:
 bch L' (imp G F1) A

Subgoal 2.4 is:
 bch L' (all F1) A

$monotone < apply IH1 to H1 H4.
Subgoal 2.2.1:

Variables: L L' A F2 F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (and F1 F2) A @
H4 : bch L F1 A *
H5 : bch L' F1 A
============================
 bch L' (and F1 F2) A

Subgoal 2.2.2 is:
 bch L' (and F1 F2) A

Subgoal 2.3 is:
 bch L' (imp G F1) A

Subgoal 2.4 is:
 bch L' (all F1) A

$monotone < search.
Subgoal 2.2.2:

Variables: L L' A F2 F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (and F1 F2) A @
H4 : bch L F2 A *
============================
 bch L' (and F1 F2) A

Subgoal 2.3 is:
 bch L' (imp G F1) A

Subgoal 2.4 is:
 bch L' (all F1) A

$monotone < apply IH1 to H1 H4.
Subgoal 2.2.2:

Variables: L L' A F2 F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (and F1 F2) A @
H4 : bch L F2 A *
H5 : bch L' F2 A
============================
 bch L' (and F1 F2) A

Subgoal 2.3 is:
 bch L' (imp G F1) A

Subgoal 2.4 is:
 bch L' (all F1) A

$monotone < search.
Subgoal 2.3:

Variables: L L' A F1 G
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (imp G F1) A @
H3 : seq L G *
H4 : bch L F1 A *
============================
 bch L' (imp G F1) A

Subgoal 2.4 is:
 bch L' (all F1) A

$monotone < apply IH to H1 H3.
Subgoal 2.3:

Variables: L L' A F1 G
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (imp G F1) A @
H3 : seq L G *
H4 : bch L F1 A *
H5 : seq L' G
============================
 bch L' (imp G F1) A

Subgoal 2.4 is:
 bch L' (all F1) A

$monotone < apply IH1 to H1 H4.
Subgoal 2.3:

Variables: L L' A F1 G
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (imp G F1) A @
H3 : seq L G *
H4 : bch L F1 A *
H5 : seq L' G
H6 : bch L' F1 A
============================
 bch L' (imp G F1) A

Subgoal 2.4 is:
 bch L' (all F1) A

$monotone < search.
Subgoal 2.4:

Variables: L L' A t F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (all F1) A @
H3 : bch L (F1 t) A *
============================
 bch L' (all F1) A

$monotone < apply IH1 to H1 H3.
Subgoal 2.4:

Variables: L L' A t F1
IH : forall L L' C, (forall E, member E L -> member E L') -> seq L C * ->
       seq L' C
IH1 : forall L L' F A, (forall E, member E L -> member E L') ->
        bch L F A * -> bch L' F A
H1 : forall E, member E L -> member E L'
H2 : bch L (all F1) A @
H3 : bch L (F1 t) A *
H4 : bch L' (F1 t) A
============================
 bch L' (all F1) A

$monotone < search.
Proof completed.
Abella < Split $monotone as monotone_seq, monotone_bch.
Theorem monotone_seq :
  forall L L' C, (forall E, member E L -> member E L') -> seq L C -> seq L' C.
Theorem monotone_bch :
  forall L L' F A, (forall E, member E L -> member E L') -> bch L F A ->
    bch L' F A.

Abella < Theorem $weakening : 
(forall L L' B G, remove L' B L -> seq L G -> seq L' G) /\
  (forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A).


============================
 (forall L L' B G, remove L' B L -> seq L G -> seq L' G) /\
   (forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A)

$weakening < split.
Subgoal 1:

============================
 forall L L' B G, remove L' B L -> seq L G -> seq L' G

Subgoal 2 is:
 forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

$weakening < intros.
Subgoal 1:

Variables: L L' B G
H1 : remove L' B L
H2 : seq L G
============================
 seq L' G

Subgoal 2 is:
 forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

$weakening < assert forall E, member E L -> member E L'.
Subgoal 1.1:

Variables: L L' B G
H1 : remove L' B L
H2 : seq L G
============================
 forall E, member E L -> member E L'

Subgoal 1 is:
 seq L' G

Subgoal 2 is:
 forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

$weakening < intros.
Subgoal 1.1:

Variables: L L' B G E
H1 : remove L' B L
H2 : seq L G
H3 : member E L
============================
 member E L'

Subgoal 1 is:
 seq L' G

Subgoal 2 is:
 forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

$weakening < backchain remove_incl.
Subgoal 1:

Variables: L L' B G
H1 : remove L' B L
H2 : seq L G
H3 : forall E, member E L -> member E L'
============================
 seq L' G

Subgoal 2 is:
 forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

$weakening < backchain monotone_seq.
Subgoal 2:

============================
 forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A

$weakening < intros.
Subgoal 2:

Variables: L L' B F A
H1 : remove L' B L
H2 : bch L F A
============================
 bch L' F A

$weakening < assert forall E, member E L -> member E L'.
Subgoal 2.1:

Variables: L L' B F A
H1 : remove L' B L
H2 : bch L F A
============================
 forall E, member E L -> member E L'

Subgoal 2 is:
 bch L' F A

$weakening < intros.
Subgoal 2.1:

Variables: L L' B F A E
H1 : remove L' B L
H2 : bch L F A
H3 : member E L
============================
 member E L'

Subgoal 2 is:
 bch L' F A

$weakening < backchain remove_incl.
Subgoal 2:

Variables: L L' B F A
H1 : remove L' B L
H2 : bch L F A
H3 : forall E, member E L -> member E L'
============================
 bch L' F A

$weakening < backchain monotone_bch.
Proof completed.
Abella < Split $weakening as weakening_seq, weakening_bch.
Theorem weakening_seq : forall L L' B G, remove L' B L -> seq L G -> seq L' G.
Theorem weakening_bch :
  forall L L' B F A, remove L' B L -> bch L F A -> bch L' F A.

Abella < Theorem member_inst : 
forall F L, nabla n, member (F n) (L n) -> (forall t, member (F t) (L t)).


============================
 forall F L, nabla n, member (F n) (L n) -> (forall t, member (F t) (L t))

member_inst < induction on 1.

IH : forall F L, nabla n, member (F n) (L n) * ->
       (forall t, member (F t) (L t))
============================
 forall F L, nabla n, member (F n) (L n) @ -> (forall t, member (F t) (L t))

member_inst < intros.

Variables: F L t
IH : forall F L, nabla n, member (F n) (L n) * ->
       (forall t, member (F t) (L t))
H1 : member (F n1) (L n1) @
============================
 member (F t) (L t)

member_inst < case H1.
Subgoal 1:

Variables: F t L1
IH : forall F L, nabla n, member (F n) (L n) * ->
       (forall t, member (F t) (L t))
============================
 member (F t) (F t :: L1 t)

Subgoal 2 is:
 member (F t) (B t :: L1 t)

member_inst < search.
Subgoal 2:

Variables: F t L1 B
IH : forall F L, nabla n, member (F n) (L n) * ->
       (forall t, member (F t) (L t))
H2 : member (F n1) (L1 n1) *
============================
 member (F t) (B t :: L1 t)

member_inst < apply IH to H2.
Subgoal 2:

Variables: F t L1 B
IH : forall F L, nabla n, member (F n) (L n) * ->
       (forall t, member (F t) (L t))
H2 : member (F n1) (L1 n1) *
H3 : forall t, member (F t) (L1 t)
============================
 member (F t) (B t :: L1 t)

member_inst < apply H3 with t = t.
Subgoal 2:

Variables: F t L1 B
IH : forall F L, nabla n, member (F n) (L n) * ->
       (forall t, member (F t) (L t))
H2 : member (F n1) (L1 n1) *
H3 : forall t, member (F t) (L1 t)
H4 : member (F t) (L1 t)
============================
 member (F t) (B t :: L1 t)

member_inst < search.
Proof completed.
Abella < Theorem $inst : 
(forall L G, nabla n, seq (L n) (G n) -> (forall t, seq (L t) (G t))) /\
  (forall L F A, nabla n, bch (L n) (F n) (A n) ->
       (forall t, bch (L t) (F t) (A t))).


============================
 (forall L G, nabla n, seq (L n) (G n) -> (forall t, seq (L t) (G t))) /\
   (forall L F A, nabla n, bch (L n) (F n) (A n) ->
        (forall t, bch (L t) (F t) (A t)))

$inst < induction on 1 1.

IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
============================
 (forall L G, nabla n, seq (L n) (G n) @ -> (forall t, seq (L t) (G t))) /\
   (forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
        (forall t, bch (L t) (F t) (A t)))

$inst < split.
Subgoal 1:

IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
============================
 forall L G, nabla n, seq (L n) (G n) @ -> (forall t, seq (L t) (G t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < intros.
Subgoal 1:

Variables: L G t
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H1 : seq (L n1) (G n1) @
============================
 seq (L t) (G t)

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < case H1.
Subgoal 1.1:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : member ($fm (F n1)) (L n1)
H3 : bch (L n1) (F n1) (A n1) *
============================
 seq (L t) (atm (A t))

Subgoal 1.2 is:
 seq (L t) (atm (A t))

Subgoal 1.3 is:
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply IH1 to H3.
Subgoal 1.1:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : member ($fm (F n1)) (L n1)
H3 : bch (L n1) (F n1) (A n1) *
H4 : forall t, bch (L t) (F t) (A t)
============================
 seq (L t) (atm (A t))

Subgoal 1.2 is:
 seq (L t) (atm (A t))

Subgoal 1.3 is:
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply member_inst to H2.
Subgoal 1.1:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : member ($fm (F n1)) (L n1)
H3 : bch (L n1) (F n1) (A n1) *
H4 : forall t, bch (L t) (F t) (A t)
H5 : forall t, member ($fm (F t)) (L t)
============================
 seq (L t) (atm (A t))

Subgoal 1.2 is:
 seq (L t) (atm (A t))

Subgoal 1.3 is:
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply H4 with t = t.
Subgoal 1.1:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : member ($fm (F n1)) (L n1)
H3 : bch (L n1) (F n1) (A n1) *
H4 : forall t, bch (L t) (F t) (A t)
H5 : forall t, member ($fm (F t)) (L t)
H6 : bch (L t) (F t) (A t)
============================
 seq (L t) (atm (A t))

Subgoal 1.2 is:
 seq (L t) (atm (A t))

Subgoal 1.3 is:
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply H5 with t = t.
Subgoal 1.1:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : member ($fm (F n1)) (L n1)
H3 : bch (L n1) (F n1) (A n1) *
H4 : forall t, bch (L t) (F t) (A t)
H5 : forall t, member ($fm (F t)) (L t)
H6 : bch (L t) (F t) (A t)
H7 : member ($fm (F t)) (L t)
============================
 seq (L t) (atm (A t))

Subgoal 1.2 is:
 seq (L t) (atm (A t))

Subgoal 1.3 is:
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < search.
Subgoal 1.2:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : prog (F n1)
H3 : bch (L n1) (F n1) (A n1) *
============================
 seq (L t) (atm (A t))

Subgoal 1.3 is:
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply IH1 to H3.
Subgoal 1.2:

Variables: L t F A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : prog (F n1)
H3 : bch (L n1) (F n1) (A n1) *
H4 : forall t, bch (L t) (F t) (A t)
============================
 seq (L t) (atm (A t))

Subgoal 1.3 is:
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply prog_has_no_nablas to H2.
Subgoal 1.2:

Variables: L t A E
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : prog E
H3 : bch (L n1) E (A n1) *
H4 : forall t, bch (L t) E (A t)
============================
 seq (L t) (atm (A t))

Subgoal 1.3 is:
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply H4 with t = t.
Subgoal 1.2:

Variables: L t A E
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : prog E
H3 : bch (L n1) E (A n1) *
H4 : forall t, bch (L t) E (A t)
H5 : bch (L t) E (A t)
============================
 seq (L t) (atm (A t))

Subgoal 1.3 is:
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < search.
Subgoal 1.3:

Variables: L t G2 G1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G1 n1) *
H3 : seq (L n1) (G2 n1) *
============================
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply IH to H2.
Subgoal 1.3:

Variables: L t G2 G1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G1 n1) *
H3 : seq (L n1) (G2 n1) *
H4 : forall t, seq (L t) (G1 t)
============================
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply IH to H3.
Subgoal 1.3:

Variables: L t G2 G1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G1 n1) *
H3 : seq (L n1) (G2 n1) *
H4 : forall t, seq (L t) (G1 t)
H5 : forall t, seq (L t) (G2 t)
============================
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply H4 with t = t.
Subgoal 1.3:

Variables: L t G2 G1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G1 n1) *
H3 : seq (L n1) (G2 n1) *
H4 : forall t, seq (L t) (G1 t)
H5 : forall t, seq (L t) (G2 t)
H6 : seq (L t) (G1 t)
============================
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply H5 with t = t.
Subgoal 1.3:

Variables: L t G2 G1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G1 n1) *
H3 : seq (L n1) (G2 n1) *
H4 : forall t, seq (L t) (G1 t)
H5 : forall t, seq (L t) (G2 t)
H6 : seq (L t) (G1 t)
H7 : seq (L t) (G2 t)
============================
 seq (L t) (and (G1 t) (G2 t))

Subgoal 1.4 is:
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < search.
Subgoal 1.4:

Variables: L t
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
============================
 seq (L t) top

Subgoal 1.5 is:
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < search.
Subgoal 1.5:

Variables: L t G1 F
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq ($fm (F n1) :: L n1) (G1 n1) *
============================
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply IH to H2.
Subgoal 1.5:

Variables: L t G1 F
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq ($fm (F n1) :: L n1) (G1 n1) *
H3 : forall t, seq ($fm (F t) :: L t) (G1 t)
============================
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply H3 with t = t.
Subgoal 1.5:

Variables: L t G1 F
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq ($fm (F n1) :: L n1) (G1 n1) *
H3 : forall t, seq ($fm (F t) :: L t) (G1 t)
H4 : seq ($fm (F t) :: L t) (G1 t)
============================
 seq (L t) (imp (F t) (G1 t))

Subgoal 1.6 is:
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < search.
Subgoal 1.6:

Variables: L t A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (A n1 n2) *
============================
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply IH to H2.
Subgoal 1.6:

Variables: L t A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (A n1 n2) *
H3 : forall t, seq (L t) (A t n2)
============================
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < apply H3 with t = t.
Subgoal 1.6:

Variables: L t A
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (A n1 n2) *
H3 : forall t, seq (L t) (A t n2)
H4 : seq (L t) (A t n2)
============================
 seq (L t) (all (A t))

Subgoal 2 is:
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < search.
Subgoal 2:

IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
============================
 forall L F A, nabla n, bch (L n) (F n) (A n) @ ->
   (forall t, bch (L t) (F t) (A t))

$inst < intros.
Subgoal 2:

Variables: L F A t
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H1 : bch (L n1) (F n1) (A n1) @
============================
 bch (L t) (F t) (A t)

$inst < case H1.
Subgoal 2.1:

Variables: L A t
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
============================
 bch (L t) (atm (A t)) (A t)

Subgoal 2.2 is:
 bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < search.
Subgoal 2.2:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : bch (L n1) (F1 n1) (A n1) * \/ bch (L n1) (F2 n1) (A n1) *
============================
 bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < case H2.
Subgoal 2.2.1:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F1 n1) (A n1) *
============================
 bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.2.2 is:
 bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < apply IH1 to H3.
Subgoal 2.2.1:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, bch (L t) (F1 t) (A t)
============================
 bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.2.2 is:
 bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < apply H4 with t = t.
Subgoal 2.2.1:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, bch (L t) (F1 t) (A t)
H5 : bch (L t) (F1 t) (A t)
============================
 bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.2.2 is:
 bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < search.
Subgoal 2.2.2:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F2 n1) (A n1) *
============================
 bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < apply IH1 to H3.
Subgoal 2.2.2:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F2 n1) (A n1) *
H4 : forall t, bch (L t) (F2 t) (A t)
============================
 bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < apply H4 with t = t.
Subgoal 2.2.2:

Variables: L A t F2 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H3 : bch (L n1) (F2 n1) (A n1) *
H4 : forall t, bch (L t) (F2 t) (A t)
H5 : bch (L t) (F2 t) (A t)
============================
 bch (L t) (and (F1 t) (F2 t)) (A t)

Subgoal 2.3 is:
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < search.
Subgoal 2.3:

Variables: L A t F1 G
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G n1) *
H3 : bch (L n1) (F1 n1) (A n1) *
============================
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < apply IH to H2.
Subgoal 2.3:

Variables: L A t F1 G
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G n1) *
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, seq (L t) (G t)
============================
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < apply IH1 to H3.
Subgoal 2.3:

Variables: L A t F1 G
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G n1) *
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, seq (L t) (G t)
H5 : forall t, bch (L t) (F1 t) (A t)
============================
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < apply H4 with t = t.
Subgoal 2.3:

Variables: L A t F1 G
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G n1) *
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, seq (L t) (G t)
H5 : forall t, bch (L t) (F1 t) (A t)
H6 : seq (L t) (G t)
============================
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < apply H5 with t = t.
Subgoal 2.3:

Variables: L A t F1 G
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : seq (L n1) (G n1) *
H3 : bch (L n1) (F1 n1) (A n1) *
H4 : forall t, seq (L t) (G t)
H5 : forall t, bch (L t) (F1 t) (A t)
H6 : seq (L t) (G t)
H7 : bch (L t) (F1 t) (A t)
============================
 bch (L t) (imp (G t) (F1 t)) (A t)

Subgoal 2.4 is:
 bch (L t) (all (F1 t)) (A t)

$inst < search.
Subgoal 2.4:

Variables: L A t t1 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : bch (L n1) (F1 n1 (t1 n1)) (A n1) *
============================
 bch (L t) (all (F1 t)) (A t)

$inst < apply IH1 to H2.
Subgoal 2.4:

Variables: L A t t1 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : bch (L n1) (F1 n1 (t1 n1)) (A n1) *
H3 : forall t, bch (L t) (F1 t (t1 t)) (A t)
============================
 bch (L t) (all (F1 t)) (A t)

$inst < apply H3 with t = t.
Subgoal 2.4:

Variables: L A t t1 F1
IH : forall L G, nabla n, seq (L n) (G n) * -> (forall t, seq (L t) (G t))
IH1 : forall L F A, nabla n, bch (L n) (F n) (A n) * ->
        (forall t, bch (L t) (F t) (A t))
H2 : bch (L n1) (F1 n1 (t1 n1)) (A n1) *
H3 : forall t, bch (L t) (F1 t (t1 t)) (A t)
H4 : bch (L t) (F1 t (t1 t)) (A t)
============================
 bch (L t) (all (F1 t)) (A t)

$inst < search.
Proof completed.
Abella < Split $inst as inst_seq, inst_bch.
Theorem inst_seq :
  forall L G, nabla n, seq (L n) (G n) -> (forall t, seq (L t) (G t)).
Theorem inst_bch :
  forall L F A, nabla n, bch (L n) (F n) (A n) ->
    (forall t, bch (L t) (F t) (A t)).

Abella < Theorem $cut : 
(forall L K F G, is_fm F -> seq K F -> remove L ($fm F) K -> seq L G ->
     seq K G) /\
  (forall L K F F' A, is_fm F -> seq K F -> remove L ($fm F) K ->
       bch L F' A -> bch K F' A) /\
  (forall L F A, is_fm F -> seq L F -> bch L F A -> seq L (atm A)).


============================
 (forall L K F G, is_fm F -> seq K F -> remove L ($fm F) K -> seq L G ->
      seq K G) /\
   (forall L K F F' A, is_fm F -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A) /\
   (forall L F A, is_fm F -> seq L F -> bch L F A -> seq L (atm A))

$cut < induction on 1 1 1.

IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
============================
 (forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K -> seq L G ->
      seq K G) /\
   (forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A) /\
   (forall L F A, is_fm F @ -> seq L F -> bch L F A -> seq L (atm A))

$cut < induction on 4 4 3.

IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
============================
 (forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K -> seq L G @@ ->
      seq K G) /\
   (forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A @@ -> bch K F' A) /\
   (forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A))

$cut < split.
Subgoal 1:

IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
============================
 forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K -> seq L G @@ ->
   seq K G

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < intros.
Subgoal 1:

Variables: L K F G
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L G @@
============================
 seq K G

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H4 (keep).
Subgoal 1.1:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (atm A) @@
H5 : member ($fm F1) L
H6 : bch L F1 A **
============================
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply remove_charac to H3 H5.
Subgoal 1.1:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (atm A) @@
H5 : member ($fm F1) L
H6 : bch L F1 A **
H7 : $fm F = $fm F1 \/ member ($fm F1) K
============================
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H7.
Subgoal 1.1.1:

Variables: L K F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F1 @
H2 : seq K F1
H3 : remove L ($fm F1) K
H4 : seq L (atm A) @@
H5 : member ($fm F1) L
H6 : bch L F1 A **
============================
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H1 (keep).
Subgoal 1.1.1.1:

Variables: L K A A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (atm A1) @
H2 : seq K (atm A1)
H3 : remove L ($fm (atm A1)) K
H4 : seq L (atm A) @@
H5 : member ($fm (atm A1)) L
H6 : bch L (atm A1) A **
============================
 seq K (atm A)

Subgoal 1.1.1.2 is:
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H6.
Subgoal 1.1.1.1:

Variables: L K A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (atm A) @
H2 : seq K (atm A)
H3 : remove L ($fm (atm A)) K
H4 : seq L (atm A) @@
H5 : member ($fm (atm A)) L
============================
 seq K (atm A)

Subgoal 1.1.1.2 is:
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 1.1.1.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L ($fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
============================
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H6 (keep).
Subgoal 1.1.1.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L ($fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H10 : bch L A1 A ** \/ bch L B A **
============================
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H10.
Subgoal 1.1.1.2.1:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L ($fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L A1 A **
============================
 seq K (atm A)

Subgoal 1.1.1.2.2 is:
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH4 to H1 H2 H3 H11.
Subgoal 1.1.1.2.1:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L ($fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L A1 A **
H12 : bch K A1 A
============================
 seq K (atm A)

Subgoal 1.1.1.2.2 is:
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H2.
Subgoal 1.1.1.2.1:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H3 : remove L ($fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L A1 A **
H12 : bch K A1 A
H13 : seq K A1
H14 : seq K B
============================
 seq K (atm A)

Subgoal 1.1.1.2.2 is:
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH2 to H8 H13 H12.
Subgoal 1.1.1.2.1:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H3 : remove L ($fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L A1 A **
H12 : bch K A1 A
H13 : seq K A1
H14 : seq K B
H15 : seq K (atm A)
============================
 seq K (atm A)

Subgoal 1.1.1.2.2 is:
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 1.1.1.2.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L ($fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L B A **
============================
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH4 to H1 H2 H3 H11.
Subgoal 1.1.1.2.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H2 : seq K (and A1 B)
H3 : remove L ($fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L B A **
H12 : bch K B A
============================
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H2.
Subgoal 1.1.1.2.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H3 : remove L ($fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L B A **
H12 : bch K B A
H13 : seq K A1
H14 : seq K B
============================
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH2 to H9 H14 H12.
Subgoal 1.1.1.2.2:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and A1 B) @
H3 : remove L ($fm (and A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (and A1 B)) L
H6 : bch L (and A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
H11 : bch L B A **
H12 : bch K B A
H13 : seq K A1
H14 : seq K B
H15 : seq K (atm A)
============================
 seq K (atm A)

Subgoal 1.1.1.3 is:
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 1.1.1.3:

Variables: L K A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm top @
H2 : seq K top
H3 : remove L ($fm top) K
H4 : seq L (atm A) @@
H5 : member ($fm top) L
H6 : bch L top A **
============================
 seq K (atm A)

Subgoal 1.1.1.4 is:
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H6.
Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L ($fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (imp A1 B)) L
H6 : bch L (imp A1 B) A **
H8 : is_fm A1 *
H9 : is_fm B *
============================
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H6.
Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L ($fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
============================
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH3 to H1 H2 H3 H10.
Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L ($fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
H12 : seq K A1
============================
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH4 to H1 H2 H3 H11.
Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L ($fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
H12 : seq K A1
H13 : bch K B A
============================
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H2 (keep).
Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L ($fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
H12 : seq K A1
H13 : bch K B A
H14 : seq ($fm A1 :: K) B
============================
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH to H8 H12 _ H14.
Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L ($fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
H12 : seq K A1
H13 : bch K B A
H14 : seq ($fm A1 :: K) B
H15 : seq K B
============================
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH2 to H9 H15 H13.
Subgoal 1.1.1.4:

Variables: L K A B A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp A1 B) @
H2 : seq K (imp A1 B)
H3 : remove L ($fm (imp A1 B)) K
H4 : seq L (atm A) @@
H5 : member ($fm (imp A1 B)) L
H8 : is_fm A1 *
H9 : is_fm B *
H10 : seq L A1 **
H11 : bch L B A **
H12 : seq K A1
H13 : bch K B A
H14 : seq ($fm A1 :: K) B
H15 : seq K B
H16 : seq K (atm A)
============================
 seq K (atm A)

Subgoal 1.1.1.5 is:
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 1.1.1.5:

Variables: L K A A1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H2 : seq K (all A1)
H3 : remove L ($fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member ($fm (all A1)) L
H6 : bch L (all A1) A **
H8 : forall x, is_fm (A1 x) *
============================
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H6.
Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H2 : seq K (all A1)
H3 : remove L ($fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member ($fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
============================
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH4 to H1 H2 H3 H9.
Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H2 : seq K (all A1)
H3 : remove L ($fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member ($fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
============================
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H2.
Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H3 : remove L ($fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member ($fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
H11 : seq K (A1 n1)
============================
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply inst_seq to H11.
Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H3 : remove L ($fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member ($fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
H11 : seq K (A1 n1)
H12 : forall t, seq K (A1 t)
============================
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply H12 with t = t.
Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H3 : remove L ($fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member ($fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
H11 : seq K (A1 n1)
H12 : forall t, seq K (A1 t)
H13 : seq K (A1 t)
============================
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply H8 with x = t.
Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H3 : remove L ($fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member ($fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
H11 : seq K (A1 n1)
H12 : forall t, seq K (A1 t)
H13 : seq K (A1 t)
H14 : is_fm (A1 t) *
============================
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH2 to H14 H13 H10.
Subgoal 1.1.1.5:

Variables: L K A A1 t
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all A1) @
H3 : remove L ($fm (all A1)) K
H4 : seq L (atm A) @@
H5 : member ($fm (all A1)) L
H8 : forall x, is_fm (A1 x) *
H9 : bch L (A1 t) A **
H10 : bch K (A1 t) A
H11 : seq K (A1 n1)
H12 : forall t, seq K (A1 t)
H13 : seq K (A1 t)
H14 : is_fm (A1 t) *
H15 : seq K (atm A)
============================
 seq K (atm A)

Subgoal 1.1.2 is:
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 1.1.2:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (atm A) @@
H5 : member ($fm F1) L
H6 : bch L F1 A **
H8 : member ($fm F1) K
============================
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH4 to H1 H2 H3 H6.
Subgoal 1.1.2:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (atm A) @@
H5 : member ($fm F1) L
H6 : bch L F1 A **
H8 : member ($fm F1) K
H9 : bch K F1 A
============================
 seq K (atm A)

Subgoal 1.2 is:
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 1.2:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (atm A) @@
H5 : prog F1
H6 : bch L F1 A **
============================
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH4 to H1 H2 H3 H6.
Subgoal 1.2:

Variables: L K F F1 A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (atm A) @@
H5 : prog F1
H6 : bch L F1 A **
H7 : bch K F1 A
============================
 seq K (atm A)

Subgoal 1.3 is:
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 1.3:

Variables: L K F G2 G1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (and G1 G2) @@
H5 : seq L G1 **
H6 : seq L G2 **
============================
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH3 to H1 H2 H3 H5.
Subgoal 1.3:

Variables: L K F G2 G1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (and G1 G2) @@
H5 : seq L G1 **
H6 : seq L G2 **
H7 : seq K G1
============================
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH3 to H1 H2 H3 H6.
Subgoal 1.3:

Variables: L K F G2 G1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (and G1 G2) @@
H5 : seq L G1 **
H6 : seq L G2 **
H7 : seq K G1
H8 : seq K G2
============================
 seq K (and G1 G2)

Subgoal 1.4 is:
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 1.4:

Variables: L K F
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L top @@
============================
 seq K top

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 1.5:

Variables: L K F G1 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (imp F1 G1) @@
H5 : seq ($fm F1 :: L) G1 **
============================
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < assert remove ($fm F1 :: L) ($fm F) ($fm F1 :: K).
Subgoal 1.5:

Variables: L K F G1 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (imp F1 G1) @@
H5 : seq ($fm F1 :: L) G1 **
H6 : remove ($fm F1 :: L) ($fm F) ($fm F1 :: K)
============================
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < assert seq ($fm F1 :: K) F.
Subgoal 1.5.1:

Variables: L K F G1 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (imp F1 G1) @@
H5 : seq ($fm F1 :: L) G1 **
H6 : remove ($fm F1 :: L) ($fm F) ($fm F1 :: K)
============================
 seq ($fm F1 :: K) F

Subgoal 1.5 is:
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < backchain weakening_seq.
Subgoal 1.5:

Variables: L K F G1 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (imp F1 G1) @@
H5 : seq ($fm F1 :: L) G1 **
H6 : remove ($fm F1 :: L) ($fm F) ($fm F1 :: K)
H7 : seq ($fm F1 :: K) F
============================
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH3 to H1 H7 H6 H5.
Subgoal 1.5:

Variables: L K F G1 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (imp F1 G1) @@
H5 : seq ($fm F1 :: L) G1 **
H6 : remove ($fm F1 :: L) ($fm F) ($fm F1 :: K)
H7 : seq ($fm F1 :: K) F
H8 : seq ($fm F1 :: K) G1
============================
 seq K (imp F1 G1)

Subgoal 1.6 is:
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 1.6:

Variables: L K F A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (all A) @@
H5 : seq L (A n1) **
============================
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH3 to H1 H2 H3 H5.
Subgoal 1.6:

Variables: L K F A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : seq L (all A) @@
H5 : seq L (A n1) **
H6 : seq K (A n1)
============================
 seq K (all A)

Subgoal 2 is:
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 2:

IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
============================
 forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
   bch L F' A @@ -> bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < intros.
Subgoal 2:

Variables: L K F F' A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L F' A @@
============================
 bch K F' A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H4 (keep).
Subgoal 2.1:

Variables: L K F A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L (atm A) A @@
============================
 bch K (atm A) A

Subgoal 2.2 is:
 bch K (and F1 F2) A

Subgoal 2.3 is:
 bch K (imp G F1) A

Subgoal 2.4 is:
 bch K (all F1) A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 2.2:

Variables: L K F A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L (and F1 F2) A @@
H5 : bch L F1 A ** \/ bch L F2 A **
============================
 bch K (and F1 F2) A

Subgoal 2.3 is:
 bch K (imp G F1) A

Subgoal 2.4 is:
 bch K (all F1) A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < case H5.
Subgoal 2.2.1:

Variables: L K F A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L (and F1 F2) A @@
H6 : bch L F1 A **
============================
 bch K (and F1 F2) A

Subgoal 2.2.2 is:
 bch K (and F1 F2) A

Subgoal 2.3 is:
 bch K (imp G F1) A

Subgoal 2.4 is:
 bch K (all F1) A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH4 to H1 H2 H3 H6.
Subgoal 2.2.1:

Variables: L K F A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L (and F1 F2) A @@
H6 : bch L F1 A **
H7 : bch K F1 A
============================
 bch K (and F1 F2) A

Subgoal 2.2.2 is:
 bch K (and F1 F2) A

Subgoal 2.3 is:
 bch K (imp G F1) A

Subgoal 2.4 is:
 bch K (all F1) A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 2.2.2:

Variables: L K F A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L (and F1 F2) A @@
H6 : bch L F2 A **
============================
 bch K (and F1 F2) A

Subgoal 2.3 is:
 bch K (imp G F1) A

Subgoal 2.4 is:
 bch K (all F1) A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH4 to H1 H2 H3 H6.
Subgoal 2.2.2:

Variables: L K F A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L (and F1 F2) A @@
H6 : bch L F2 A **
H7 : bch K F2 A
============================
 bch K (and F1 F2) A

Subgoal 2.3 is:
 bch K (imp G F1) A

Subgoal 2.4 is:
 bch K (all F1) A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 2.3:

Variables: L K F A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L (imp G F1) A @@
H5 : seq L G **
H6 : bch L F1 A **
============================
 bch K (imp G F1) A

Subgoal 2.4 is:
 bch K (all F1) A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH3 to H1 H2 H3 H5.
Subgoal 2.3:

Variables: L K F A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L (imp G F1) A @@
H5 : seq L G **
H6 : bch L F1 A **
H7 : seq K G
============================
 bch K (imp G F1) A

Subgoal 2.4 is:
 bch K (all F1) A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH4 to H1 H2 H3 H6.
Subgoal 2.3:

Variables: L K F A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L (imp G F1) A @@
H5 : seq L G **
H6 : bch L F1 A **
H7 : seq K G
H8 : bch K F1 A
============================
 bch K (imp G F1) A

Subgoal 2.4 is:
 bch K (all F1) A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 2.4:

Variables: L K F A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L (all F1) A @@
H5 : bch L (F1 t) A **
============================
 bch K (all F1) A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < apply IH4 to H1 H2 H3 H5.
Subgoal 2.4:

Variables: L K F A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq K F
H3 : remove L ($fm F) K
H4 : bch L (all F1) A @@
H5 : bch L (F1 t) A **
H6 : bch K (F1 t) A
============================
 bch K (all F1) A

Subgoal 3 is:
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < search.
Subgoal 3:

IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
============================
 forall L F A, is_fm F @ -> seq L F -> bch L F A @@ -> seq L (atm A)

$cut < intros.
Subgoal 3:

Variables: L F A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm F @
H2 : seq L F
H3 : bch L F A @@
============================
 seq L (atm A)

$cut < case H3 (keep).
Subgoal 3.1:

Variables: L A
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (atm A) @
H2 : seq L (atm A)
H3 : bch L (atm A) A @@
============================
 seq L (atm A)

Subgoal 3.2 is:
 seq L (atm A)

Subgoal 3.3 is:
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < search.
Subgoal 3.2:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H4 : bch L F1 A ** \/ bch L F2 A **
============================
 seq L (atm A)

Subgoal 3.3 is:
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < case H4.
Subgoal 3.2.1:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F1 A **
============================
 seq L (atm A)

Subgoal 3.2.2 is:
 seq L (atm A)

Subgoal 3.3 is:
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < case H1 (keep).
Subgoal 3.2.1:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F1 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
============================
 seq L (atm A)

Subgoal 3.2.2 is:
 seq L (atm A)

Subgoal 3.3 is:
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < case H2 (keep).
Subgoal 3.2.1:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F1 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
H8 : seq L F1
H9 : seq L F2
============================
 seq L (atm A)

Subgoal 3.2.2 is:
 seq L (atm A)

Subgoal 3.3 is:
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < apply IH2 to H6 H8 H5.
Subgoal 3.2.1:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F1 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
H8 : seq L F1
H9 : seq L F2
H10 : seq L (atm A)
============================
 seq L (atm A)

Subgoal 3.2.2 is:
 seq L (atm A)

Subgoal 3.3 is:
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < search.
Subgoal 3.2.2:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F2 A **
============================
 seq L (atm A)

Subgoal 3.3 is:
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < case H1 (keep).
Subgoal 3.2.2:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F2 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
============================
 seq L (atm A)

Subgoal 3.3 is:
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < case H2 (keep).
Subgoal 3.2.2:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F2 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
H8 : seq L F1
H9 : seq L F2
============================
 seq L (atm A)

Subgoal 3.3 is:
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < apply IH2 to H7 H9 H5.
Subgoal 3.2.2:

Variables: L A F2 F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (and F1 F2) @
H2 : seq L (and F1 F2)
H3 : bch L (and F1 F2) A @@
H5 : bch L F2 A **
H6 : is_fm F1 *
H7 : is_fm F2 *
H8 : seq L F1
H9 : seq L F2
H10 : seq L (atm A)
============================
 seq L (atm A)

Subgoal 3.3 is:
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < search.
Subgoal 3.3:

Variables: L A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp G F1) @
H2 : seq L (imp G F1)
H3 : bch L (imp G F1) A @@
H4 : seq L G **
H5 : bch L F1 A **
============================
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < case H1 (keep).
Subgoal 3.3:

Variables: L A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp G F1) @
H2 : seq L (imp G F1)
H3 : bch L (imp G F1) A @@
H4 : seq L G **
H5 : bch L F1 A **
H6 : is_fm G *
H7 : is_fm F1 *
============================
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < case H2 (keep).
Subgoal 3.3:

Variables: L A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp G F1) @
H2 : seq L (imp G F1)
H3 : bch L (imp G F1) A @@
H4 : seq L G **
H5 : bch L F1 A **
H6 : is_fm G *
H7 : is_fm F1 *
H8 : seq ($fm G :: L) F1
============================
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < apply IH to H6 H4 _ H8.
Subgoal 3.3:

Variables: L A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp G F1) @
H2 : seq L (imp G F1)
H3 : bch L (imp G F1) A @@
H4 : seq L G **
H5 : bch L F1 A **
H6 : is_fm G *
H7 : is_fm F1 *
H8 : seq ($fm G :: L) F1
H9 : seq L F1
============================
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < apply IH2 to H7 H9 H5.
Subgoal 3.3:

Variables: L A F1 G
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (imp G F1) @
H2 : seq L (imp G F1)
H3 : bch L (imp G F1) A @@
H4 : seq L G **
H5 : bch L F1 A **
H6 : is_fm G *
H7 : is_fm F1 *
H8 : seq ($fm G :: L) F1
H9 : seq L F1
H10 : seq L (atm A)
============================
 seq L (atm A)

Subgoal 3.4 is:
 seq L (atm A)

$cut < search.
Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
============================
 seq L (atm A)

$cut < case H1 (keep).
Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
============================
 seq L (atm A)

$cut < case H2 (keep).
Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
H6 : seq L (F1 n1)
============================
 seq L (atm A)

$cut < apply H5 with x = t.
Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
H6 : seq L (F1 n1)
H7 : is_fm (F1 t) *
============================
 seq L (atm A)

$cut < apply inst_seq to H6.
Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
H6 : seq L (F1 n1)
H7 : is_fm (F1 t) *
H8 : forall t, seq L (F1 t)
============================
 seq L (atm A)

$cut < apply H8 with t = t.
Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
H6 : seq L (F1 n1)
H7 : is_fm (F1 t) *
H8 : forall t, seq L (F1 t)
H9 : seq L (F1 t)
============================
 seq L (atm A)

$cut < apply IH2 to H7 H9 H4.
Subgoal 3.4:

Variables: L A t F1
IH : forall L K F G, is_fm F * -> seq K F -> remove L ($fm F) K -> seq L G ->
       seq K G
IH1 : forall L K F F' A, is_fm F * -> seq K F -> remove L ($fm F) K ->
        bch L F' A -> bch K F' A
IH2 : forall L F A, is_fm F * -> seq L F -> bch L F A -> seq L (atm A)
IH3 : forall L K F G, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        seq L G ** -> seq K G
IH4 : forall L K F F' A, is_fm F @ -> seq K F -> remove L ($fm F) K ->
        bch L F' A ** -> bch K F' A
IH5 : forall L F A, is_fm F @ -> seq L F -> bch L F A ** -> seq L (atm A)
H1 : is_fm (all F1) @
H2 : seq L (all F1)
H3 : bch L (all F1) A @@
H4 : bch L (F1 t) A **
H5 : forall x, is_fm (F1 x) *
H6 : seq L (F1 n1)
H7 : is_fm (F1 t) *
H8 : forall t, seq L (F1 t)
H9 : seq L (F1 t)
H10 : seq L (atm A)
============================
 seq L (atm A)

$cut < search.
Proof completed.
Abella < Split $cut as cut, cut_commutative, cut_principal.
Theorem cut :
  forall L K F G, is_fm F -> seq K F -> remove L ($fm F) K -> seq L G ->
    seq K G.
Theorem cut_commutative :
  forall L K F F' A, is_fm F -> seq K F -> remove L ($fm F) K ->
    bch L F' A -> bch K F' A.
Theorem cut_principal :
  forall L F A, is_fm F -> seq L F -> bch L F A -> seq L (atm A).

Abella <