Welcome to Abella 1.3.6-dev1
Abella < Specification "cut".
Reading specification cut
Abella < Define ctx : olist -> prop by
ctx nil;
ctx (hyp A :: L) := ctx L.
Abella < Theorem ctx_lemma :
forall A L, ctx L -> member (conc A) L -> false.
============================
forall A L, ctx L -> member (conc A) L -> false
ctx_lemma < induction on 1.
IH : forall A L, ctx L * -> member (conc A) L -> false
============================
forall A L, ctx L @ -> member (conc A) L -> false
ctx_lemma < intros.
Variables: A, L
IH : forall A L, ctx L * -> member (conc A) L -> false
H1 : ctx L @
H2 : member (conc A) L
============================
false
ctx_lemma < case H1.
Subgoal 1:
Variables: A, L
IH : forall A L, ctx L * -> member (conc A) L -> false
H2 : member (conc A) nil
============================
false
Subgoal 2 is:
false
ctx_lemma < case H2.
Subgoal 2:
Variables: A, L, L1, A1
IH : forall A L, ctx L * -> member (conc A) L -> false
H2 : member (conc A) (hyp A1 :: L1)
H3 : ctx L1 *
============================
false
ctx_lemma < case H2.
Subgoal 2:
Variables: A, L, L1, A1
IH : forall A L, ctx L * -> member (conc A) L -> false
H3 : ctx L1 *
H4 : member (conc A) L1
============================
false
ctx_lemma < apply IH to H3 H4.
Proof completed.
Abella < Theorem bot_inv :
forall L C, ctx L -> {L |- conc bot} -> {L |- conc C}.
============================
forall L C, ctx L -> {L |- conc bot} -> {L |- conc C}
bot_inv < induction on 2.
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
============================
forall L C, ctx L -> {L |- conc bot}@ -> {L |- conc C}
bot_inv < intros.
Variables: L, C
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H2 : {L |- conc bot}@
============================
{L |- conc C}
bot_inv < case H2.
Subgoal 1:
Variables: L, C
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : member (conc bot) L
============================
{L |- conc C}
Subgoal 2 is:
{L |- conc C}
Subgoal 3 is:
{L |- conc C}
Subgoal 4 is:
{L |- conc C}
Subgoal 5 is:
{L |- conc C}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < apply ctx_lemma to H1 H3.
Subgoal 2:
Variables: L, C
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp bot}*
============================
{L |- conc C}
Subgoal 3 is:
{L |- conc C}
Subgoal 4 is:
{L |- conc C}
Subgoal 5 is:
{L |- conc C}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < search.
Subgoal 3:
Variables: L, C
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp bot}*
============================
{L |- conc C}
Subgoal 4 is:
{L |- conc C}
Subgoal 5 is:
{L |- conc C}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < search.
Subgoal 4:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc bot}*
============================
{L |- conc C}
Subgoal 5 is:
{L |- conc C}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < apply IH to _ H4 with C = C.
Subgoal 4:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc bot}*
H5 : {L, hyp A, hyp B |- conc C}
============================
{L |- conc C}
Subgoal 5 is:
{L |- conc C}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < search.
Subgoal 5:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc bot}*
H5 : {L, hyp B |- conc bot}*
============================
{L |- conc C}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < apply IH to _ H4 with C = C.
Subgoal 5:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc bot}*
H5 : {L, hyp B |- conc bot}*
H6 : {L, hyp A |- conc C}
============================
{L |- conc C}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < apply IH to _ H5 with C = C.
Subgoal 5:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc bot}*
H5 : {L, hyp B |- conc bot}*
H6 : {L, hyp A |- conc C}
H7 : {L, hyp B |- conc C}
============================
{L |- conc C}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < search.
Subgoal 6:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc bot}*
============================
{L |- conc C}
Subgoal 7 is:
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < apply IH to _ H5 with C = C.
Subgoal 6:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc bot}*
H6 : {L, hyp B |- conc C}
============================
{L |- conc C}
Subgoal 7 is:
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < search.
Subgoal 7:
Variables: L, C, T, A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc bot}*
============================
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < apply IH to _ H4 with C = C.
Subgoal 7:
Variables: L, C, T, A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc bot}*
H5 : {L, hyp (A T) |- conc C}
============================
{L |- conc C}
Subgoal 8 is:
{L |- conc C}
bot_inv < search.
Subgoal 8:
Variables: L, C, A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc bot}*
============================
{L |- conc C}
bot_inv < apply IH to _ H4 with C = C.
Subgoal 8:
Variables: L, C, A
IH : forall L C, ctx L -> {L |- conc bot}* -> {L |- conc C}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc bot}*
H5 : {L, hyp (A n1) |- conc C}
============================
{L |- conc C}
bot_inv < search.
Proof completed.
Abella < Theorem and_left_inv :
forall L C1 C2, ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C1}.
============================
forall L C1 C2, ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C1}
and_left_inv < induction on 2.
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
============================
forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}@ -> {L |- conc C1}
and_left_inv < intros.
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H2 : {L |- conc (and C1 C2)}@
============================
{L |- conc C1}
and_left_inv < case H2.
Subgoal 1:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : member (conc (and C1 C2)) L
============================
{L |- conc C1}
Subgoal 2 is:
{L |- conc C1}
Subgoal 3 is:
{L |- conc C1}
Subgoal 4 is:
{L |- conc C1}
Subgoal 5 is:
{L |- conc C1}
Subgoal 6 is:
{L |- conc C1}
Subgoal 7 is:
{L |- conc C1}
Subgoal 8 is:
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < apply ctx_lemma to H1 H3.
Subgoal 2:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (and C1 C2)}*
============================
{L |- conc C1}
Subgoal 3 is:
{L |- conc C1}
Subgoal 4 is:
{L |- conc C1}
Subgoal 5 is:
{L |- conc C1}
Subgoal 6 is:
{L |- conc C1}
Subgoal 7 is:
{L |- conc C1}
Subgoal 8 is:
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < search.
Subgoal 3:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp bot}*
============================
{L |- conc C1}
Subgoal 4 is:
{L |- conc C1}
Subgoal 5 is:
{L |- conc C1}
Subgoal 6 is:
{L |- conc C1}
Subgoal 7 is:
{L |- conc C1}
Subgoal 8 is:
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < search.
Subgoal 4:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- conc C1}*
H4 : {L |- conc C2}*
============================
{L |- conc C1}
Subgoal 5 is:
{L |- conc C1}
Subgoal 6 is:
{L |- conc C1}
Subgoal 7 is:
{L |- conc C1}
Subgoal 8 is:
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < search.
Subgoal 5:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (and C1 C2)}*
============================
{L |- conc C1}
Subgoal 6 is:
{L |- conc C1}
Subgoal 7 is:
{L |- conc C1}
Subgoal 8 is:
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < apply IH to _ H4.
Subgoal 5:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (and C1 C2)}*
H5 : {L, hyp A, hyp B |- conc C1}
============================
{L |- conc C1}
Subgoal 6 is:
{L |- conc C1}
Subgoal 7 is:
{L |- conc C1}
Subgoal 8 is:
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < search.
Subgoal 6:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
============================
{L |- conc C1}
Subgoal 7 is:
{L |- conc C1}
Subgoal 8 is:
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < apply IH to _ H4.
Subgoal 6:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp A |- conc C1}
============================
{L |- conc C1}
Subgoal 7 is:
{L |- conc C1}
Subgoal 8 is:
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < apply IH to _ H5.
Subgoal 6:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp A |- conc C1}
H7 : {L, hyp B |- conc C1}
============================
{L |- conc C1}
Subgoal 7 is:
{L |- conc C1}
Subgoal 8 is:
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < search.
Subgoal 7:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (and C1 C2)}*
============================
{L |- conc C1}
Subgoal 8 is:
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < apply IH to _ H5.
Subgoal 7:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp B |- conc C1}
============================
{L |- conc C1}
Subgoal 8 is:
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < search.
Subgoal 8:
Variables: L, C1, C2, T, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (and C1 C2)}*
============================
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < apply IH to _ H4.
Subgoal 8:
Variables: L, C1, C2, T, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (and C1 C2)}*
H5 : {L, hyp (A T) |- conc C1}
============================
{L |- conc C1}
Subgoal 9 is:
{L |- conc C1}
and_left_inv < search.
Subgoal 9:
Variables: L, C1, C2, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (and C1 C2)}*
============================
{L |- conc C1}
and_left_inv < apply IH to _ H4.
Subgoal 9:
Variables: L, C1, C2, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C1}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (and C1 C2)}*
H5 : {L, hyp (A n1) |- conc C1}
============================
{L |- conc C1}
and_left_inv < search.
Proof completed.
Abella < Theorem and_right_inv :
forall L C1 C2, ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C2}.
============================
forall L C1 C2, ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C2}
and_right_inv < induction on 2.
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
============================
forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}@ -> {L |- conc C2}
and_right_inv < intros.
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H2 : {L |- conc (and C1 C2)}@
============================
{L |- conc C2}
and_right_inv < case H2.
Subgoal 1:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : member (conc (and C1 C2)) L
============================
{L |- conc C2}
Subgoal 2 is:
{L |- conc C2}
Subgoal 3 is:
{L |- conc C2}
Subgoal 4 is:
{L |- conc C2}
Subgoal 5 is:
{L |- conc C2}
Subgoal 6 is:
{L |- conc C2}
Subgoal 7 is:
{L |- conc C2}
Subgoal 8 is:
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < apply ctx_lemma to H1 H3.
Subgoal 2:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (and C1 C2)}*
============================
{L |- conc C2}
Subgoal 3 is:
{L |- conc C2}
Subgoal 4 is:
{L |- conc C2}
Subgoal 5 is:
{L |- conc C2}
Subgoal 6 is:
{L |- conc C2}
Subgoal 7 is:
{L |- conc C2}
Subgoal 8 is:
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < search.
Subgoal 3:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp bot}*
============================
{L |- conc C2}
Subgoal 4 is:
{L |- conc C2}
Subgoal 5 is:
{L |- conc C2}
Subgoal 6 is:
{L |- conc C2}
Subgoal 7 is:
{L |- conc C2}
Subgoal 8 is:
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < search.
Subgoal 4:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- conc C1}*
H4 : {L |- conc C2}*
============================
{L |- conc C2}
Subgoal 5 is:
{L |- conc C2}
Subgoal 6 is:
{L |- conc C2}
Subgoal 7 is:
{L |- conc C2}
Subgoal 8 is:
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < search.
Subgoal 5:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (and C1 C2)}*
============================
{L |- conc C2}
Subgoal 6 is:
{L |- conc C2}
Subgoal 7 is:
{L |- conc C2}
Subgoal 8 is:
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < apply IH to _ H4.
Subgoal 5:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (and C1 C2)}*
H5 : {L, hyp A, hyp B |- conc C2}
============================
{L |- conc C2}
Subgoal 6 is:
{L |- conc C2}
Subgoal 7 is:
{L |- conc C2}
Subgoal 8 is:
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < search.
Subgoal 6:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
============================
{L |- conc C2}
Subgoal 7 is:
{L |- conc C2}
Subgoal 8 is:
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < apply IH to _ H4.
Subgoal 6:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp A |- conc C2}
============================
{L |- conc C2}
Subgoal 7 is:
{L |- conc C2}
Subgoal 8 is:
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < apply IH to _ H5.
Subgoal 6:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (and C1 C2)}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp A |- conc C2}
H7 : {L, hyp B |- conc C2}
============================
{L |- conc C2}
Subgoal 7 is:
{L |- conc C2}
Subgoal 8 is:
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < search.
Subgoal 7:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (and C1 C2)}*
============================
{L |- conc C2}
Subgoal 8 is:
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < apply IH to _ H5.
Subgoal 7:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (and C1 C2)}*
H6 : {L, hyp B |- conc C2}
============================
{L |- conc C2}
Subgoal 8 is:
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < search.
Subgoal 8:
Variables: L, C1, C2, T, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (and C1 C2)}*
============================
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < apply IH to _ H4.
Subgoal 8:
Variables: L, C1, C2, T, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (and C1 C2)}*
H5 : {L, hyp (A T) |- conc C2}
============================
{L |- conc C2}
Subgoal 9 is:
{L |- conc C2}
and_right_inv < search.
Subgoal 9:
Variables: L, C1, C2, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (and C1 C2)}*
============================
{L |- conc C2}
and_right_inv < apply IH to _ H4.
Subgoal 9:
Variables: L, C1, C2, A
IH : forall L C1 C2, ctx L -> {L |- conc (and C1 C2)}* -> {L |- conc C2}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (and C1 C2)}*
H5 : {L, hyp (A n1) |- conc C2}
============================
{L |- conc C2}
and_right_inv < search.
Proof completed.
Abella < Theorem imp_inv :
forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)} -> {L, hyp C1 |- conc C2}.
============================
forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)} -> {L, hyp C1 |- conc C2}
imp_inv < induction on 2.
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
============================
forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}@ ->
{L, hyp C1 |- conc C2}
imp_inv < intros.
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H2 : {L |- conc (imp C1 C2)}@
============================
{L, hyp C1 |- conc C2}
imp_inv < case H2.
Subgoal 1:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : member (conc (imp C1 C2)) L
============================
{L, hyp C1 |- conc C2}
Subgoal 2 is:
{L, hyp C1 |- conc C2}
Subgoal 3 is:
{L, hyp C1 |- conc C2}
Subgoal 4 is:
{L, hyp C1 |- conc C2}
Subgoal 5 is:
{L, hyp C1 |- conc C2}
Subgoal 6 is:
{L, hyp C1 |- conc C2}
Subgoal 7 is:
{L, hyp C1 |- conc C2}
Subgoal 8 is:
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < apply ctx_lemma to H1 H3.
Subgoal 2:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (imp C1 C2)}*
============================
{L, hyp C1 |- conc C2}
Subgoal 3 is:
{L, hyp C1 |- conc C2}
Subgoal 4 is:
{L, hyp C1 |- conc C2}
Subgoal 5 is:
{L, hyp C1 |- conc C2}
Subgoal 6 is:
{L, hyp C1 |- conc C2}
Subgoal 7 is:
{L, hyp C1 |- conc C2}
Subgoal 8 is:
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < search.
Subgoal 3:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp bot}*
============================
{L, hyp C1 |- conc C2}
Subgoal 4 is:
{L, hyp C1 |- conc C2}
Subgoal 5 is:
{L, hyp C1 |- conc C2}
Subgoal 6 is:
{L, hyp C1 |- conc C2}
Subgoal 7 is:
{L, hyp C1 |- conc C2}
Subgoal 8 is:
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < search.
Subgoal 4:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (imp C1 C2)}*
============================
{L, hyp C1 |- conc C2}
Subgoal 5 is:
{L, hyp C1 |- conc C2}
Subgoal 6 is:
{L, hyp C1 |- conc C2}
Subgoal 7 is:
{L, hyp C1 |- conc C2}
Subgoal 8 is:
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < apply IH to _ H4.
Subgoal 4:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (imp C1 C2)}*
H5 : {L, hyp A, hyp B, hyp C1 |- conc C2}
============================
{L, hyp C1 |- conc C2}
Subgoal 5 is:
{L, hyp C1 |- conc C2}
Subgoal 6 is:
{L, hyp C1 |- conc C2}
Subgoal 7 is:
{L, hyp C1 |- conc C2}
Subgoal 8 is:
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < search.
Subgoal 5:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (imp C1 C2)}*
H5 : {L, hyp B |- conc (imp C1 C2)}*
============================
{L, hyp C1 |- conc C2}
Subgoal 6 is:
{L, hyp C1 |- conc C2}
Subgoal 7 is:
{L, hyp C1 |- conc C2}
Subgoal 8 is:
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < apply IH to _ H4.
Subgoal 5:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (imp C1 C2)}*
H5 : {L, hyp B |- conc (imp C1 C2)}*
H6 : {L, hyp A, hyp C1 |- conc C2}
============================
{L, hyp C1 |- conc C2}
Subgoal 6 is:
{L, hyp C1 |- conc C2}
Subgoal 7 is:
{L, hyp C1 |- conc C2}
Subgoal 8 is:
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < apply IH to _ H5.
Subgoal 5:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (imp C1 C2)}*
H5 : {L, hyp B |- conc (imp C1 C2)}*
H6 : {L, hyp A, hyp C1 |- conc C2}
H7 : {L, hyp B, hyp C1 |- conc C2}
============================
{L, hyp C1 |- conc C2}
Subgoal 6 is:
{L, hyp C1 |- conc C2}
Subgoal 7 is:
{L, hyp C1 |- conc C2}
Subgoal 8 is:
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < search.
Subgoal 6:
Variables: L, C1, C2
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L, hyp C1 |- conc C2}*
============================
{L, hyp C1 |- conc C2}
Subgoal 7 is:
{L, hyp C1 |- conc C2}
Subgoal 8 is:
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < search.
Subgoal 7:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (imp C1 C2)}*
============================
{L, hyp C1 |- conc C2}
Subgoal 8 is:
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < apply IH to _ H5.
Subgoal 7:
Variables: L, C1, C2, B, A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (imp C1 C2)}*
H6 : {L, hyp B, hyp C1 |- conc C2}
============================
{L, hyp C1 |- conc C2}
Subgoal 8 is:
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < search.
Subgoal 8:
Variables: L, C1, C2, T, A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (imp C1 C2)}*
============================
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < apply IH to _ H4.
Subgoal 8:
Variables: L, C1, C2, T, A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (imp C1 C2)}*
H5 : {L, hyp (A T), hyp C1 |- conc C2}
============================
{L, hyp C1 |- conc C2}
Subgoal 9 is:
{L, hyp C1 |- conc C2}
imp_inv < search.
Subgoal 9:
Variables: L, C1, C2, A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (imp C1 C2)}*
============================
{L, hyp C1 |- conc C2}
imp_inv < apply IH to _ H4.
Subgoal 9:
Variables: L, C1, C2, A
IH : forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)}* ->
{L, hyp C1 |- conc C2}
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (imp C1 C2)}*
H5 : {L, hyp (A n1), hyp C1 |- conc C2}
============================
{L, hyp C1 |- conc C2}
imp_inv < search.
Proof completed.
Abella < Theorem all_inv :
forall L C, ctx L -> {L |- conc (all C)} -> (nabla x, {L |- conc (C x)}).
============================
forall L C, ctx L -> {L |- conc (all C)} -> (nabla x, {L |- conc (C x)})
all_inv < induction on 2.
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
============================
forall L C, ctx L -> {L |- conc (all C)}@ -> (nabla x, {L |- conc (C x)})
all_inv < intros.
Variables: L, C
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H2 : {L |- conc (all C)}@
============================
{L |- conc (C n1)}
all_inv < case H2.
Subgoal 1:
Variables: L, C
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : member (conc (all C)) L
============================
{L |- conc (C n1)}
Subgoal 2 is:
{L |- conc (C n1)}
Subgoal 3 is:
{L |- conc (C n1)}
Subgoal 4 is:
{L |- conc (C n1)}
Subgoal 5 is:
{L |- conc (C n1)}
Subgoal 6 is:
{L |- conc (C n1)}
Subgoal 7 is:
{L |- conc (C n1)}
Subgoal 8 is:
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < apply ctx_lemma to H1 H3.
Subgoal 2:
Variables: L, C
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (all C)}*
============================
{L |- conc (C n1)}
Subgoal 3 is:
{L |- conc (C n1)}
Subgoal 4 is:
{L |- conc (C n1)}
Subgoal 5 is:
{L |- conc (C n1)}
Subgoal 6 is:
{L |- conc (C n1)}
Subgoal 7 is:
{L |- conc (C n1)}
Subgoal 8 is:
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < search.
Subgoal 3:
Variables: L, C
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp bot}*
============================
{L |- conc (C n1)}
Subgoal 4 is:
{L |- conc (C n1)}
Subgoal 5 is:
{L |- conc (C n1)}
Subgoal 6 is:
{L |- conc (C n1)}
Subgoal 7 is:
{L |- conc (C n1)}
Subgoal 8 is:
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < search.
Subgoal 4:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (all C)}*
============================
{L |- conc (C n1)}
Subgoal 5 is:
{L |- conc (C n1)}
Subgoal 6 is:
{L |- conc (C n1)}
Subgoal 7 is:
{L |- conc (C n1)}
Subgoal 8 is:
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < apply IH to _ H4.
Subgoal 4:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (and A B)}*
H4 : {L, hyp A, hyp B |- conc (all C)}*
H5 : {L, hyp A, hyp B |- conc (C n1)}
============================
{L |- conc (C n1)}
Subgoal 5 is:
{L |- conc (C n1)}
Subgoal 6 is:
{L |- conc (C n1)}
Subgoal 7 is:
{L |- conc (C n1)}
Subgoal 8 is:
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < search.
Subgoal 5:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (all C)}*
H5 : {L, hyp B |- conc (all C)}*
============================
{L |- conc (C n1)}
Subgoal 6 is:
{L |- conc (C n1)}
Subgoal 7 is:
{L |- conc (C n1)}
Subgoal 8 is:
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < apply IH to _ H4.
Subgoal 5:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (all C)}*
H5 : {L, hyp B |- conc (all C)}*
H6 : {L, hyp A |- conc (C n1)}
============================
{L |- conc (C n1)}
Subgoal 6 is:
{L |- conc (C n1)}
Subgoal 7 is:
{L |- conc (C n1)}
Subgoal 8 is:
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < apply IH to _ H5.
Subgoal 5:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (or A B)}*
H4 : {L, hyp A |- conc (all C)}*
H5 : {L, hyp B |- conc (all C)}*
H6 : {L, hyp A |- conc (C n1)}
H7 : {L, hyp B |- conc (C n1)}
============================
{L |- conc (C n1)}
Subgoal 6 is:
{L |- conc (C n1)}
Subgoal 7 is:
{L |- conc (C n1)}
Subgoal 8 is:
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < search.
Subgoal 6:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (all C)}*
============================
{L |- conc (C n1)}
Subgoal 7 is:
{L |- conc (C n1)}
Subgoal 8 is:
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < apply IH to _ H5.
Subgoal 6:
Variables: L, C, B, A
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (imp A B)}*
H4 : {L |- conc A}*
H5 : {L, hyp B |- conc (all C)}*
H6 : {L, hyp B |- conc (C n1)}
============================
{L |- conc (C n1)}
Subgoal 7 is:
{L |- conc (C n1)}
Subgoal 8 is:
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < search.
Subgoal 7:
Variables: L, C
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- conc (C n1)}*
============================
{L |- conc (C n1)}
Subgoal 8 is:
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < search.
Subgoal 8:
Variables: L, C, T, A
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (all C)}*
============================
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < apply IH to _ H4.
Subgoal 8:
Variables: L, C, T, A
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (all A)}*
H4 : {L, hyp (A T) |- conc (all C)}*
H5 : {L, hyp (A T) |- conc (C n1)}
============================
{L |- conc (C n1)}
Subgoal 9 is:
{L |- conc (C n1)}
all_inv < search.
Subgoal 9:
Variables: L, C, A
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (all C)}*
============================
{L |- conc (C n1)}
all_inv < apply IH to _ H4.
Subgoal 9:
Variables: L, C, A
IH : forall L C, ctx L -> {L |- conc (all C)}* -> (nabla x,
{L |- conc (C x)})
H1 : ctx L
H3 : {L |- hyp (ex A)}*
H4 : {L, hyp (A n1) |- conc (all C)}*
H5 : {L, hyp (A n1) |- conc (C n2)}
============================
{L |- conc (C n1)}
all_inv < search.
Proof completed.
Abella < Theorem cut_admissibility :
forall L K C, {form K} -> ctx L -> {L |- conc K} -> {L, hyp K |- conc C} ->
{L |- conc C}.
============================
forall L K C, {form K} -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
cut_admissibility < induction on 1.
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
============================
forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
cut_admissibility < induction on 4.
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
============================
forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}@@ -> {L |- conc C}
cut_admissibility < intros.
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H4 : {L, hyp K |- conc C}@@
============================
{L |- conc C}
cut_admissibility < case H4.
Subgoal 1:
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : member (conc C) (hyp K :: L)
============================
{L |- conc C}
Subgoal 2 is:
{L |- conc C}
Subgoal 3 is:
{L |- conc top}
Subgoal 4 is:
{L |- conc C}
Subgoal 5 is:
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply ctx_lemma to _ H5.
Subgoal 2:
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp C}**
============================
{L |- conc C}
Subgoal 3 is:
{L |- conc top}
Subgoal 4 is:
{L |- conc C}
Subgoal 5 is:
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H5.
Subgoal 2:
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : member (hyp C) (hyp K :: L)
============================
{L |- conc C}
Subgoal 3 is:
{L |- conc top}
Subgoal 4 is:
{L |- conc C}
Subgoal 5 is:
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H6.
Subgoal 2.1:
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
============================
{L |- conc K}
Subgoal 2.2 is:
{L |- conc C}
Subgoal 3 is:
{L |- conc top}
Subgoal 4 is:
{L |- conc C}
Subgoal 5 is:
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 2.2:
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H7 : member (hyp C) L
============================
{L |- conc C}
Subgoal 3 is:
{L |- conc top}
Subgoal 4 is:
{L |- conc C}
Subgoal 5 is:
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 3:
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
============================
{L |- conc top}
Subgoal 4 is:
{L |- conc C}
Subgoal 5 is:
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 4:
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp bot}**
============================
{L |- conc C}
Subgoal 5 is:
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H5.
Subgoal 4:
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : member (hyp bot) (hyp K :: L)
============================
{L |- conc C}
Subgoal 5 is:
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H6.
Subgoal 4.1:
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form bot}@
H2 : ctx L
H3 : {L |- conc bot}
============================
{L |- conc C}
Subgoal 4.2 is:
{L |- conc C}
Subgoal 5 is:
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply bot_inv to H2 H3 with C = C.
Subgoal 4.1:
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form bot}@
H2 : ctx L
H3 : {L |- conc bot}
H7 : {L |- conc C}
============================
{L |- conc C}
Subgoal 4.2 is:
{L |- conc C}
Subgoal 5 is:
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 4.2:
Variables: L, K, C
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H7 : member (hyp bot) L
============================
{L |- conc C}
Subgoal 5 is:
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 5:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
H6 : {L, hyp K |- conc B}**
============================
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H5.
Subgoal 5:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
H6 : {L, hyp K |- conc B}**
H7 : {L |- conc A}
============================
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 5:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
H6 : {L, hyp K |- conc B}**
H7 : {L |- conc A}
H8 : {L |- conc B}
============================
{L |- conc (and A B)}
Subgoal 6 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 6:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (and A B)}**
H6 : {L, hyp K, hyp A, hyp B |- conc C}**
============================
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 6:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (and A B)}**
H6 : {L, hyp K, hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
============================
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H5.
Subgoal 6:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H8 : member (hyp (and A B)) (hyp K :: L)
============================
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H8.
Subgoal 6.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (and A B)}@
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
============================
{L |- conc C}
Subgoal 6.2 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply and_left_inv to _ H3.
Subgoal 6.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (and A B)}@
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H9 : {L |- conc A}
============================
{L |- conc C}
Subgoal 6.2 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply and_right_inv to _ H3.
Subgoal 6.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (and A B)}@
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H9 : {L |- conc A}
H10 : {L |- conc B}
============================
{L |- conc C}
Subgoal 6.2 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H1.
Subgoal 6.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H9 : {L |- conc A}
H10 : {L |- conc B}
H11 : {form A}*
H12 : {form B}*
============================
{L |- conc C}
Subgoal 6.2 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH to H11 _ H9 H7.
Subgoal 6.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H9 : {L |- conc A}
H10 : {L |- conc B}
H11 : {form A}*
H12 : {form B}*
H13 : {L, hyp B |- conc C}
============================
{L |- conc C}
Subgoal 6.2 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH to H12 _ H10 H13.
Subgoal 6.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (and A B)}
H6 : {L, hyp (and A B), hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H9 : {L |- conc A}
H10 : {L |- conc B}
H11 : {form A}*
H12 : {form B}*
H13 : {L, hyp B |- conc C}
H14 : {L |- conc C}
============================
{L |- conc C}
Subgoal 6.2 is:
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 6.2:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A, hyp B |- conc C}**
H7 : {L, hyp A, hyp B |- conc C}
H9 : member (hyp (and A B)) L
============================
{L |- conc C}
Subgoal 7 is:
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 7:
Variables: L, K, C, A, B
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
============================
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 H2 H3 H5.
Subgoal 7:
Variables: L, K, C, A, B
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
H6 : {L |- conc A}
============================
{L |- conc (or A B)}
Subgoal 8 is:
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 8:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc B}**
============================
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 H2 H3 H5.
Subgoal 8:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc B}**
H6 : {L |- conc B}
============================
{L |- conc (or A B)}
Subgoal 9 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 9:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (or A B)}**
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
============================
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 9:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (or A B)}**
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
============================
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H7.
Subgoal 9:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (or A B)}**
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
============================
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H5.
Subgoal 9:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
H10 : member (hyp (or A B)) (hyp K :: L)
============================
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H10.
Subgoal 9.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
============================
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < assert forall L D, ctx L -> {L |- conc (or A B)} -> {L, hyp A |- conc D} ->
{L, hyp B |- conc D} -> {L |- conc D}.
Subgoal 9.1.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
============================
forall L D, ctx L -> {L |- conc (or A B)} -> {L, hyp A |- conc D} ->
{L, hyp B |- conc D} -> {L |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < induction on 2.
Subgoal 9.1.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
============================
forall L D, ctx L -> {L |- conc (or A B)}@@@ -> {L, hyp A |- conc D} ->
{L, hyp B |- conc D} -> {L |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < intros.
Subgoal 9.1.1:
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H12 : {L1 |- conc (or A B)}@@@
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
============================
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H12.
Subgoal 9.1.1.1:
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : member (conc (or A B)) L1
============================
{L1 |- conc D}
Subgoal 9.1.1.2 is:
{L1 |- conc D}
Subgoal 9.1.1.3 is:
{L1 |- conc D}
Subgoal 9.1.1.4 is:
{L1 |- conc D}
Subgoal 9.1.1.5 is:
{L1 |- conc D}
Subgoal 9.1.1.6 is:
{L1 |- conc D}
Subgoal 9.1.1.7 is:
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply ctx_lemma to H11 H15.
Subgoal 9.1.1.2:
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (or A B)}***
============================
{L1 |- conc D}
Subgoal 9.1.1.3 is:
{L1 |- conc D}
Subgoal 9.1.1.4 is:
{L1 |- conc D}
Subgoal 9.1.1.5 is:
{L1 |- conc D}
Subgoal 9.1.1.6 is:
{L1 |- conc D}
Subgoal 9.1.1.7 is:
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 9.1.1.3:
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp bot}***
============================
{L1 |- conc D}
Subgoal 9.1.1.4 is:
{L1 |- conc D}
Subgoal 9.1.1.5 is:
{L1 |- conc D}
Subgoal 9.1.1.6 is:
{L1 |- conc D}
Subgoal 9.1.1.7 is:
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 9.1.1.4:
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (and A1 B1)}***
H16 : {L1, hyp A1, hyp B1 |- conc (or A B)}***
============================
{L1 |- conc D}
Subgoal 9.1.1.5 is:
{L1 |- conc D}
Subgoal 9.1.1.6 is:
{L1 |- conc D}
Subgoal 9.1.1.7 is:
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H16 H13 H14.
Subgoal 9.1.1.4:
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (and A1 B1)}***
H16 : {L1, hyp A1, hyp B1 |- conc (or A B)}***
H17 : {L1, hyp A1, hyp B1 |- conc D}
============================
{L1 |- conc D}
Subgoal 9.1.1.5 is:
{L1 |- conc D}
Subgoal 9.1.1.6 is:
{L1 |- conc D}
Subgoal 9.1.1.7 is:
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 9.1.1.5:
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- conc A}***
============================
{L1 |- conc D}
Subgoal 9.1.1.6 is:
{L1 |- conc D}
Subgoal 9.1.1.7 is:
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H1.
Subgoal 9.1.1.5:
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- conc A}***
H16 : {form A}*
H17 : {form B}*
============================
{L1 |- conc D}
Subgoal 9.1.1.6 is:
{L1 |- conc D}
Subgoal 9.1.1.7 is:
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH to H16 H11 H15 H13.
Subgoal 9.1.1.5:
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- conc A}***
H16 : {form A}*
H17 : {form B}*
H18 : {L1 |- conc D}
============================
{L1 |- conc D}
Subgoal 9.1.1.6 is:
{L1 |- conc D}
Subgoal 9.1.1.7 is:
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 9.1.1.6:
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- conc B}***
============================
{L1 |- conc D}
Subgoal 9.1.1.7 is:
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H1.
Subgoal 9.1.1.6:
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- conc B}***
H16 : {form A}*
H17 : {form B}*
============================
{L1 |- conc D}
Subgoal 9.1.1.7 is:
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH to H17 H11 H15 H14.
Subgoal 9.1.1.6:
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- conc B}***
H16 : {form A}*
H17 : {form B}*
H18 : {L1 |- conc D}
============================
{L1 |- conc D}
Subgoal 9.1.1.7 is:
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 9.1.1.7:
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (or A1 B1)}***
H16 : {L1, hyp A1 |- conc (or A B)}***
H17 : {L1, hyp B1 |- conc (or A B)}***
============================
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H16 H13 H14.
Subgoal 9.1.1.7:
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (or A1 B1)}***
H16 : {L1, hyp A1 |- conc (or A B)}***
H17 : {L1, hyp B1 |- conc (or A B)}***
H18 : {L1, hyp A1 |- conc D}
============================
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H17 H13 H14.
Subgoal 9.1.1.7:
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (or A1 B1)}***
H16 : {L1, hyp A1 |- conc (or A B)}***
H17 : {L1, hyp B1 |- conc (or A B)}***
H18 : {L1, hyp A1 |- conc D}
H19 : {L1, hyp B1 |- conc D}
============================
{L1 |- conc D}
Subgoal 9.1.1.8 is:
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 9.1.1.8:
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (imp A1 B1)}***
H16 : {L1 |- conc A1}***
H17 : {L1, hyp B1 |- conc (or A B)}***
============================
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H17 H13 H14.
Subgoal 9.1.1.8:
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (imp A1 B1)}***
H16 : {L1 |- conc A1}***
H17 : {L1, hyp B1 |- conc (or A B)}***
H18 : {L1, hyp B1 |- conc D}
============================
{L1 |- conc D}
Subgoal 9.1.1.9 is:
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 9.1.1.9:
Variables: L, K, C, B, A, L1, D, T, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (all A1)}***
H16 : {L1, hyp (A1 T) |- conc (or A B)}***
============================
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H16 H13 H14.
Subgoal 9.1.1.9:
Variables: L, K, C, B, A, L1, D, T, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (all A1)}***
H16 : {L1, hyp (A1 T) |- conc (or A B)}***
H17 : {L1, hyp (A1 T) |- conc D}
============================
{L1 |- conc D}
Subgoal 9.1.1.10 is:
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 9.1.1.10:
Variables: L, K, C, B, A, L1, D, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (ex A1)}***
H16 : {L1, hyp (A1 n1) |- conc (or A B)}***
============================
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H16 H13 H14.
Subgoal 9.1.1.10:
Variables: L, K, C, B, A, L1, D, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
IH2 : forall L D, ctx L -> {L |- conc (or A B)}*** ->
{L, hyp A |- conc D} -> {L, hyp B |- conc D} -> {L |- conc D}
H11 : ctx L1
H13 : {L1, hyp A |- conc D}
H14 : {L1, hyp B |- conc D}
H15 : {L1 |- hyp (ex A1)}***
H16 : {L1, hyp (A1 n1) |- conc (or A B)}***
H17 : {L1, hyp (A1 n1) |- conc D}
============================
{L1 |- conc D}
Subgoal 9.1 is:
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 9.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
H11 : forall L D, ctx L -> {L |- conc (or A B)} -> {L, hyp A |- conc D} ->
{L, hyp B |- conc D} -> {L |- conc D}
============================
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply H11 to H2 H3 H8 H9.
Subgoal 9.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (or A B)}@
H2 : ctx L
H3 : {L |- conc (or A B)}
H6 : {L, hyp (or A B), hyp A |- conc C}**
H7 : {L, hyp (or A B), hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
H11 : forall L D, ctx L -> {L |- conc (or A B)} -> {L, hyp A |- conc D} ->
{L, hyp B |- conc D} -> {L |- conc D}
H12 : {L |- conc C}
============================
{L |- conc C}
Subgoal 9.2 is:
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 9.2:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp A |- conc C}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L, hyp A |- conc C}
H9 : {L, hyp B |- conc C}
H11 : member (hyp (or A B)) L
============================
{L |- conc C}
Subgoal 10 is:
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 10:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K, hyp A |- conc B}**
============================
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H5.
Subgoal 10:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K, hyp A |- conc B}**
H6 : {L, hyp A |- conc B}
============================
{L |- conc (imp A B)}
Subgoal 11 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 11:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (imp A B)}**
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
============================
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 11:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (imp A B)}**
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L |- conc A}
============================
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H7.
Subgoal 11:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (imp A B)}**
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
============================
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H5.
Subgoal 11:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H10 : member (hyp (imp A B)) (hyp K :: L)
============================
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H10.
Subgoal 11.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (imp A B)}@
H2 : ctx L
H3 : {L |- conc (imp A B)}
H6 : {L, hyp (imp A B) |- conc A}**
H7 : {L, hyp (imp A B), hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
============================
{L |- conc C}
Subgoal 11.2 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply imp_inv to _ H3.
Subgoal 11.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (imp A B)}@
H2 : ctx L
H3 : {L |- conc (imp A B)}
H6 : {L, hyp (imp A B) |- conc A}**
H7 : {L, hyp (imp A B), hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H11 : {L, hyp A |- conc B}
============================
{L |- conc C}
Subgoal 11.2 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H1.
Subgoal 11.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (imp A B)}
H6 : {L, hyp (imp A B) |- conc A}**
H7 : {L, hyp (imp A B), hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H11 : {L, hyp A |- conc B}
H12 : {form A}*
H13 : {form B}*
============================
{L |- conc C}
Subgoal 11.2 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH to H12 _ H8 H11.
Subgoal 11.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (imp A B)}
H6 : {L, hyp (imp A B) |- conc A}**
H7 : {L, hyp (imp A B), hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H11 : {L, hyp A |- conc B}
H12 : {form A}*
H13 : {form B}*
H14 : {L |- conc B}
============================
{L |- conc C}
Subgoal 11.2 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH to H13 _ H14 H9.
Subgoal 11.1:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (imp A B)}
H6 : {L, hyp (imp A B) |- conc A}**
H7 : {L, hyp (imp A B), hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H11 : {L, hyp A |- conc B}
H12 : {form A}*
H13 : {form B}*
H14 : {L |- conc B}
H15 : {L |- conc C}
============================
{L |- conc C}
Subgoal 11.2 is:
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 11.2:
Variables: L, K, C, B, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K |- conc A}**
H7 : {L, hyp K, hyp B |- conc C}**
H8 : {L |- conc A}
H9 : {L, hyp B |- conc C}
H11 : member (hyp (imp A B)) L
============================
{L |- conc C}
Subgoal 12 is:
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 12:
Variables: L, K, C, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc (A n1)}**
============================
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H5.
Subgoal 12:
Variables: L, K, C, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc (A n1)}**
H6 : {L |- conc (A n1)}
============================
{L |- conc (all A)}
Subgoal 13 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 13:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (all A)}**
H6 : {L, hyp K, hyp (A T) |- conc C}**
============================
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 13:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (all A)}**
H6 : {L, hyp K, hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
============================
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H5.
Subgoal 13:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H8 : member (hyp (all A)) (hyp K :: L)
============================
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H8.
Subgoal 13.1:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (all A)}@
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
============================
{L |- conc C}
Subgoal 13.2 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply all_inv to _ H3.
Subgoal 13.1:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (all A)}@
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H9 : {L |- conc (A n1)}
============================
{L |- conc C}
Subgoal 13.2 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < case H1.
Subgoal 13.1:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H9 : {L |- conc (A n1)}
H10 : {form (A n1)}*
============================
{L |- conc C}
Subgoal 13.2 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < inst H9 with n1 = T.
Subgoal 13.1:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H9 : {L |- conc (A n1)}
H10 : {form (A n1)}*
H11 : {L |- conc (A T)}
============================
{L |- conc C}
Subgoal 13.2 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < inst H10 with n1 = T.
Subgoal 13.1:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H9 : {L |- conc (A n1)}
H10 : {form (A n1)}*
H11 : {L |- conc (A T)}
H12 : {form (A T)}*
============================
{L |- conc C}
Subgoal 13.2 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH to H12 _ H11 H7.
Subgoal 13.1:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (all A)}
H6 : {L, hyp (all A), hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H9 : {L |- conc (A n1)}
H10 : {form (A n1)}*
H11 : {L |- conc (A T)}
H12 : {form (A T)}*
H13 : {L |- conc C}
============================
{L |- conc C}
Subgoal 13.2 is:
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 13.2:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A T) |- conc C}**
H7 : {L, hyp (A T) |- conc C}
H9 : member (hyp (all A)) L
============================
{L |- conc C}
Subgoal 14 is:
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 14:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc (A T)}**
============================
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 H2 H3 H5.
Subgoal 14:
Variables: L, K, C, T, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc (A T)}**
H6 : {L |- conc (A T)}
============================
{L |- conc (ex A)}
Subgoal 15 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 15:
Variables: L, K, C, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (ex A)}**
H6 : {L, hyp K, hyp (A n1) |- conc C}**
============================
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H6.
Subgoal 15:
Variables: L, K, C, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp (ex A)}**
H6 : {L, hyp K, hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
============================
{L |- conc C}
cut_admissibility < case H5.
Subgoal 15:
Variables: L, K, C, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
H8 : member (hyp (ex A)) (hyp K :: L)
============================
{L |- conc C}
cut_admissibility < case H8.
Subgoal 15.1:
Variables: L, K, C, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
============================
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < assert forall L D, nabla x, ctx L -> {L |- conc (ex A)} ->
{L, hyp (A x) |- conc D} -> {L |- conc D}.
Subgoal 15.1.1:
Variables: L, K, C, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
============================
forall L D, nabla x, ctx L -> {L |- conc (ex A)} ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < induction on 2.
Subgoal 15.1.1:
Variables: L, K, C, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
============================
forall L D, nabla x, ctx L -> {L |- conc (ex A)}@@@ ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < intros.
Subgoal 15.1.1:
Variables: L, K, C, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H10 : {L1 |- conc (ex A)}@@@
H11 : {L1, hyp (A n1) |- conc D}
============================
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < case H10.
Subgoal 15.1.1.1:
Variables: L, K, C, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : member (conc (ex A)) L1
============================
{L1 |- conc D}
Subgoal 15.1.1.2 is:
{L1 |- conc D}
Subgoal 15.1.1.3 is:
{L1 |- conc D}
Subgoal 15.1.1.4 is:
{L1 |- conc D}
Subgoal 15.1.1.5 is:
{L1 |- conc D}
Subgoal 15.1.1.6 is:
{L1 |- conc D}
Subgoal 15.1.1.7 is:
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < apply ctx_lemma to H9 H12.
Subgoal 15.1.1.2:
Variables: L, K, C, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (ex A)}***
============================
{L1 |- conc D}
Subgoal 15.1.1.3 is:
{L1 |- conc D}
Subgoal 15.1.1.4 is:
{L1 |- conc D}
Subgoal 15.1.1.5 is:
{L1 |- conc D}
Subgoal 15.1.1.6 is:
{L1 |- conc D}
Subgoal 15.1.1.7 is:
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 15.1.1.3:
Variables: L, K, C, A, L1, D
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp bot}***
============================
{L1 |- conc D}
Subgoal 15.1.1.4 is:
{L1 |- conc D}
Subgoal 15.1.1.5 is:
{L1 |- conc D}
Subgoal 15.1.1.6 is:
{L1 |- conc D}
Subgoal 15.1.1.7 is:
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 15.1.1.4:
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (and A1 B)}***
H13 : {L1, hyp A1, hyp B |- conc (ex A)}***
============================
{L1 |- conc D}
Subgoal 15.1.1.5 is:
{L1 |- conc D}
Subgoal 15.1.1.6 is:
{L1 |- conc D}
Subgoal 15.1.1.7 is:
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H13 H11.
Subgoal 15.1.1.4:
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (and A1 B)}***
H13 : {L1, hyp A1, hyp B |- conc (ex A)}***
H14 : {L1, hyp A1, hyp B |- conc D}
============================
{L1 |- conc D}
Subgoal 15.1.1.5 is:
{L1 |- conc D}
Subgoal 15.1.1.6 is:
{L1 |- conc D}
Subgoal 15.1.1.7 is:
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 15.1.1.5:
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (or A1 B)}***
H13 : {L1, hyp A1 |- conc (ex A)}***
H14 : {L1, hyp B |- conc (ex A)}***
============================
{L1 |- conc D}
Subgoal 15.1.1.6 is:
{L1 |- conc D}
Subgoal 15.1.1.7 is:
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H13 H11.
Subgoal 15.1.1.5:
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (or A1 B)}***
H13 : {L1, hyp A1 |- conc (ex A)}***
H14 : {L1, hyp B |- conc (ex A)}***
H15 : {L1, hyp A1 |- conc D}
============================
{L1 |- conc D}
Subgoal 15.1.1.6 is:
{L1 |- conc D}
Subgoal 15.1.1.7 is:
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H14 H11.
Subgoal 15.1.1.5:
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (or A1 B)}***
H13 : {L1, hyp A1 |- conc (ex A)}***
H14 : {L1, hyp B |- conc (ex A)}***
H15 : {L1, hyp A1 |- conc D}
H16 : {L1, hyp B |- conc D}
============================
{L1 |- conc D}
Subgoal 15.1.1.6 is:
{L1 |- conc D}
Subgoal 15.1.1.7 is:
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 15.1.1.6:
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (imp A1 B)}***
H13 : {L1 |- conc A1}***
H14 : {L1, hyp B |- conc (ex A)}***
============================
{L1 |- conc D}
Subgoal 15.1.1.7 is:
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H14 H11.
Subgoal 15.1.1.6:
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (imp A1 B)}***
H13 : {L1 |- conc A1}***
H14 : {L1, hyp B |- conc (ex A)}***
H15 : {L1, hyp B |- conc D}
============================
{L1 |- conc D}
Subgoal 15.1.1.7 is:
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 15.1.1.7:
Variables: L, K, C, A, L1, D, T, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (all A1)}***
H13 : {L1, hyp (A1 T) |- conc (ex A)}***
============================
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H13 H11.
Subgoal 15.1.1.7:
Variables: L, K, C, A, L1, D, T, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (all A1)}***
H13 : {L1, hyp (A1 T) |- conc (ex A)}***
H14 : {L1, hyp (A1 T) |- conc D}
============================
{L1 |- conc D}
Subgoal 15.1.1.8 is:
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 15.1.1.8:
Variables: L, K, C, A, L1, D, T
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- conc (A T)}***
============================
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < case H1.
Subgoal 15.1.1.8:
Variables: L, K, C, A, L1, D, T
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- conc (A T)}***
H13 : {form (A n1)}*
============================
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < inst H13 with n1 = T.
Subgoal 15.1.1.8:
Variables: L, K, C, A, L1, D, T
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- conc (A T)}***
H13 : {form (A n1)}*
H14 : {form (A T)}*
============================
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < inst H11 with n1 = T.
Subgoal 15.1.1.8:
Variables: L, K, C, A, L1, D, T
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- conc (A T)}***
H13 : {form (A n1)}*
H14 : {form (A T)}*
H15 : {L1, hyp (A T) |- conc D}
============================
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < apply IH to H14 H9 H12 H15.
Subgoal 15.1.1.8:
Variables: L, K, C, A, L1, D, T
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- conc (A T)}***
H13 : {form (A n1)}*
H14 : {form (A T)}*
H15 : {L1, hyp (A T) |- conc D}
H16 : {L1 |- conc D}
============================
{L1 |- conc D}
Subgoal 15.1.1.9 is:
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 15.1.1.9:
Variables: L, K, C, A, L1, D, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (ex A1)}***
H13 : {L1, hyp (A1 n1) |- conc (ex A)}***
============================
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < assert {L1, hyp (A n2) |- conc D}.
Subgoal 15.1.1.9:
Variables: L, K, C, A, L1, D, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (ex A1)}***
H13 : {L1, hyp (A1 n1) |- conc (ex A)}***
H14 : {L1, hyp (A n2) |- conc D}
============================
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H13 H14.
Subgoal 15.1.1.9:
Variables: L, K, C, A, L1, D, A1
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
IH2 : forall L D, nabla x, ctx L -> {L |- conc (ex A)}*** ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H9 : ctx L1
H11 : {L1, hyp (A n1) |- conc D}
H12 : {L1 |- hyp (ex A1)}***
H13 : {L1, hyp (A1 n1) |- conc (ex A)}***
H14 : {L1, hyp (A n2) |- conc D}
H15 : {L1, hyp (A1 n1) |- conc D}
============================
{L1 |- conc D}
Subgoal 15.1 is:
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 15.1:
Variables: L, K, C, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
H9 : forall L D, nabla x, ctx L -> {L |- conc (ex A)} ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
============================
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < apply H9 to H2 H3 H7.
Subgoal 15.1:
Variables: L, K, C, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form (ex A)}@
H2 : ctx L
H3 : {L |- conc (ex A)}
H6 : {L, hyp (ex A), hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
H9 : forall L D, nabla x, ctx L -> {L |- conc (ex A)} ->
{L, hyp (A x) |- conc D} -> {L |- conc D}
H10 : {L |- conc C}
============================
{L |- conc C}
Subgoal 15.2 is:
{L |- conc C}
cut_admissibility < search.
Subgoal 15.2:
Variables: L, K, C, A
IH : forall L K C, {form K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {form K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {form K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : {L, hyp K, hyp (A n1) |- conc C}**
H7 : {L, hyp (A n1) |- conc C}
H9 : member (hyp (ex A)) L
============================
{L |- conc C}
cut_admissibility < search.
Proof completed.
Abella < Goodbye.
