Welcome to Abella 1.1.3-dev2
Reading clauses from cut.mod
Abella < Define ctx nil.
Abella < Define ctx (hyp A :: L) := ctx L.
Abella < Theorem ctx_lemma :
forall A L, ctx L -> member (conc A) L -> false.
1 subgoal(s).
============================
forall A L, ctx L -> member (conc A) L -> false
ctx_lemma < induction on 1.
1 subgoal(s).
IH : forall A L, ctx L * -> member (conc A) L -> false
============================
forall A L, ctx L @ -> member (conc A) L -> false
ctx_lemma < intros.
1 subgoal(s).
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.
2 subgoal(s).
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.
1 subgoal(s).
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.
1 subgoal(s).
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}.
1 subgoal(s).
============================
forall L C, ctx L -> {L |- conc bot} -> {L |- conc C}
bot_inv < induction on 2.
1 subgoal(s).
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.
1 subgoal(s).
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.
8 subgoal(s).
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.
7 subgoal(s).
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 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}
bot_inv < search.
6 subgoal(s).
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 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}
bot_inv < search.
5 subgoal(s).
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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc C}
bot_inv < apply IH to _ H4 with C = C.
5 subgoal(s).
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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc C}
bot_inv < search.
4 subgoal(s).
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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc C}
bot_inv < apply IH to _ H4 with C = C.
4 subgoal(s).
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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc C}
bot_inv < apply IH to _ H5 with C = C.
4 subgoal(s).
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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc C}
bot_inv < search.
3 subgoal(s).
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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
bot_inv < apply IH to _ H5 with C = C.
3 subgoal(s).
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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
bot_inv < search.
2 subgoal(s).
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 2 is:
{L |- conc C}
bot_inv < apply IH to _ H4 with C = C.
2 subgoal(s).
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 2 is:
{L |- conc C}
bot_inv < search.
1 subgoal(s).
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.
1 subgoal(s).
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}.
1 subgoal(s).
============================
forall L C1 C2, ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C1}
and_left_inv < induction on 2.
1 subgoal(s).
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.
1 subgoal(s).
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.
9 subgoal(s).
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.
8 subgoal(s).
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 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}
and_left_inv < search.
7 subgoal(s).
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 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}
and_left_inv < search.
6 subgoal(s).
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 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}
and_left_inv < search.
5 subgoal(s).
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 2 is:
{L |- conc C1}
subgoal 3 is:
{L |- conc C1}
subgoal 4 is:
{L |- conc C1}
subgoal 5 is:
{L |- conc C1}
and_left_inv < apply IH to _ H4.
5 subgoal(s).
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 2 is:
{L |- conc C1}
subgoal 3 is:
{L |- conc C1}
subgoal 4 is:
{L |- conc C1}
subgoal 5 is:
{L |- conc C1}
and_left_inv < search.
4 subgoal(s).
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 2 is:
{L |- conc C1}
subgoal 3 is:
{L |- conc C1}
subgoal 4 is:
{L |- conc C1}
and_left_inv < apply IH to _ H4.
4 subgoal(s).
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 2 is:
{L |- conc C1}
subgoal 3 is:
{L |- conc C1}
subgoal 4 is:
{L |- conc C1}
and_left_inv < apply IH to _ H5.
4 subgoal(s).
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 2 is:
{L |- conc C1}
subgoal 3 is:
{L |- conc C1}
subgoal 4 is:
{L |- conc C1}
and_left_inv < search.
3 subgoal(s).
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 2 is:
{L |- conc C1}
subgoal 3 is:
{L |- conc C1}
and_left_inv < apply IH to _ H5.
3 subgoal(s).
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 2 is:
{L |- conc C1}
subgoal 3 is:
{L |- conc C1}
and_left_inv < search.
2 subgoal(s).
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 2 is:
{L |- conc C1}
and_left_inv < apply IH to _ H4.
2 subgoal(s).
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 2 is:
{L |- conc C1}
and_left_inv < search.
1 subgoal(s).
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.
1 subgoal(s).
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}.
1 subgoal(s).
============================
forall L C1 C2, ctx L -> {L |- conc (and C1 C2)} -> {L |- conc C2}
and_right_inv < induction on 2.
1 subgoal(s).
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.
1 subgoal(s).
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.
9 subgoal(s).
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.
8 subgoal(s).
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 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}
and_right_inv < search.
7 subgoal(s).
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 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}
and_right_inv < search.
6 subgoal(s).
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 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}
and_right_inv < search.
5 subgoal(s).
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 2 is:
{L |- conc C2}
subgoal 3 is:
{L |- conc C2}
subgoal 4 is:
{L |- conc C2}
subgoal 5 is:
{L |- conc C2}
and_right_inv < apply IH to _ H4.
5 subgoal(s).
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 2 is:
{L |- conc C2}
subgoal 3 is:
{L |- conc C2}
subgoal 4 is:
{L |- conc C2}
subgoal 5 is:
{L |- conc C2}
and_right_inv < search.
4 subgoal(s).
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 2 is:
{L |- conc C2}
subgoal 3 is:
{L |- conc C2}
subgoal 4 is:
{L |- conc C2}
and_right_inv < apply IH to _ H4.
4 subgoal(s).
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 2 is:
{L |- conc C2}
subgoal 3 is:
{L |- conc C2}
subgoal 4 is:
{L |- conc C2}
and_right_inv < apply IH to _ H5.
4 subgoal(s).
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 2 is:
{L |- conc C2}
subgoal 3 is:
{L |- conc C2}
subgoal 4 is:
{L |- conc C2}
and_right_inv < search.
3 subgoal(s).
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 2 is:
{L |- conc C2}
subgoal 3 is:
{L |- conc C2}
and_right_inv < apply IH to _ H5.
3 subgoal(s).
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 2 is:
{L |- conc C2}
subgoal 3 is:
{L |- conc C2}
and_right_inv < search.
2 subgoal(s).
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 2 is:
{L |- conc C2}
and_right_inv < apply IH to _ H4.
2 subgoal(s).
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 2 is:
{L |- conc C2}
and_right_inv < search.
1 subgoal(s).
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.
1 subgoal(s).
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}.
1 subgoal(s).
============================
forall L C1 C2, ctx L -> {L |- conc (imp C1 C2)} -> {L, hyp C1 |- conc C2}
imp_inv < induction on 2.
1 subgoal(s).
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.
1 subgoal(s).
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.
9 subgoal(s).
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.
8 subgoal(s).
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 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}
imp_inv < search.
7 subgoal(s).
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 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}
imp_inv < search.
6 subgoal(s).
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 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}
imp_inv < apply IH to _ H4.
6 subgoal(s).
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 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}
imp_inv < search.
5 subgoal(s).
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 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}
imp_inv < apply IH to _ H4.
5 subgoal(s).
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 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}
imp_inv < apply IH to _ H5.
5 subgoal(s).
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 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}
imp_inv < search.
4 subgoal(s).
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 2 is:
{L, hyp C1 |- conc C2}
subgoal 3 is:
{L, hyp C1 |- conc C2}
subgoal 4 is:
{L, hyp C1 |- conc C2}
imp_inv < search.
3 subgoal(s).
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 2 is:
{L, hyp C1 |- conc C2}
subgoal 3 is:
{L, hyp C1 |- conc C2}
imp_inv < apply IH to _ H5.
3 subgoal(s).
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 2 is:
{L, hyp C1 |- conc C2}
subgoal 3 is:
{L, hyp C1 |- conc C2}
imp_inv < search.
2 subgoal(s).
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 2 is:
{L, hyp C1 |- conc C2}
imp_inv < apply IH to _ H4.
2 subgoal(s).
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 2 is:
{L, hyp C1 |- conc C2}
imp_inv < search.
1 subgoal(s).
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.
1 subgoal(s).
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)}).
1 subgoal(s).
============================
forall L C, ctx L -> {L |- conc (all C)} -> (nabla x, {L |- conc (C x)})
all_inv < induction on 2.
1 subgoal(s).
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.
1 subgoal(s).
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.
9 subgoal(s).
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.
8 subgoal(s).
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 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)}
all_inv < search.
7 subgoal(s).
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 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)}
all_inv < search.
6 subgoal(s).
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 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)}
all_inv < apply IH to _ H4.
6 subgoal(s).
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 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)}
all_inv < search.
5 subgoal(s).
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 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)}
all_inv < apply IH to _ H4.
5 subgoal(s).
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 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)}
all_inv < apply IH to _ H5.
5 subgoal(s).
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 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)}
all_inv < search.
4 subgoal(s).
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 2 is:
{L |- conc (C n1)}
subgoal 3 is:
{L |- conc (C n1)}
subgoal 4 is:
{L |- conc (C n1)}
all_inv < apply IH to _ H5.
4 subgoal(s).
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 2 is:
{L |- conc (C n1)}
subgoal 3 is:
{L |- conc (C n1)}
subgoal 4 is:
{L |- conc (C n1)}
all_inv < search.
3 subgoal(s).
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 2 is:
{L |- conc (C n1)}
subgoal 3 is:
{L |- conc (C n1)}
all_inv < search.
2 subgoal(s).
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 2 is:
{L |- conc (C n1)}
all_inv < apply IH to _ H4.
2 subgoal(s).
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 2 is:
{L |- conc (C n1)}
all_inv < search.
1 subgoal(s).
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.
1 subgoal(s).
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, {prop K} -> ctx L -> {L |- conc K} -> {L, hyp K |- conc C} ->
{L |- conc C}.
1 subgoal(s).
============================
forall L K C, {prop K} -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
cut_admissibility < induction on 1.
1 subgoal(s).
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
============================
forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
cut_admissibility < induction on 4.
1 subgoal(s).
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
============================
forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}@@ -> {L |- conc C}
cut_admissibility < intros.
1 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H4 : {L, hyp K |- conc C}@@
============================
{L |- conc C}
cut_admissibility < case H4.
15 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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.
14 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp C}**
============================
{L |- conc C}
subgoal 2 is:
{L |- conc top}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (and A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (or A B)}
subgoal 7 is:
{L |- conc (or A B)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (imp A B)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (all A)}
subgoal 12 is:
{L |- conc C}
subgoal 13 is:
{L |- conc (ex A)}
subgoal 14 is:
{L |- conc C}
cut_admissibility < case H5.
14 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : member (hyp C) (hyp K :: L)
============================
{L |- conc C}
subgoal 2 is:
{L |- conc top}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (and A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (or A B)}
subgoal 7 is:
{L |- conc (or A B)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (imp A B)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (all A)}
subgoal 12 is:
{L |- conc C}
subgoal 13 is:
{L |- conc (ex A)}
subgoal 14 is:
{L |- conc C}
cut_admissibility < case H6.
15 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
============================
{L |- conc K}
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 < search.
14 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H7 : member (hyp C) L
============================
{L |- conc C}
subgoal 2 is:
{L |- conc top}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (and A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (or A B)}
subgoal 7 is:
{L |- conc (or A B)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (imp A B)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (all A)}
subgoal 12 is:
{L |- conc C}
subgoal 13 is:
{L |- conc (ex A)}
subgoal 14 is:
{L |- conc C}
cut_admissibility < search.
13 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
============================
{L |- conc top}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (and A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (or A B)}
subgoal 6 is:
{L |- conc (or A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (imp A B)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (all A)}
subgoal 11 is:
{L |- conc C}
subgoal 12 is:
{L |- conc (ex A)}
subgoal 13 is:
{L |- conc C}
cut_admissibility < search.
12 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- hyp bot}**
============================
{L |- conc C}
subgoal 2 is:
{L |- conc (and A B)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc (or A B)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (imp A B)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (all A)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (ex A)}
subgoal 12 is:
{L |- conc C}
cut_admissibility < case H5.
12 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H6 : member (hyp bot) (hyp K :: L)
============================
{L |- conc C}
subgoal 2 is:
{L |- conc (and A B)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc (or A B)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (imp A B)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (all A)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (ex A)}
subgoal 12 is:
{L |- conc C}
cut_admissibility < case H6.
13 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop bot}@
H2 : ctx L
H3 : {L |- conc bot}
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (and A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (or A B)}
subgoal 6 is:
{L |- conc (or A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (imp A B)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (all A)}
subgoal 11 is:
{L |- conc C}
subgoal 12 is:
{L |- conc (ex A)}
subgoal 13 is:
{L |- conc C}
cut_admissibility < apply bot_inv to H2 H3 with C = C.
13 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop bot}@
H2 : ctx L
H3 : {L |- conc bot}
H7 : {L |- conc C}
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (and A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (or A B)}
subgoal 6 is:
{L |- conc (or A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (imp A B)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (all A)}
subgoal 11 is:
{L |- conc C}
subgoal 12 is:
{L |- conc (ex A)}
subgoal 13 is:
{L |- conc C}
cut_admissibility < search.
12 subgoal(s).
Variables: L, K, C
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H7 : member (hyp bot) L
============================
{L |- conc C}
subgoal 2 is:
{L |- conc (and A B)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc (or A B)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (imp A B)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (all A)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (ex A)}
subgoal 12 is:
{L |- conc C}
cut_admissibility < search.
11 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (imp A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (all A)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (ex A)}
subgoal 11 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H5.
11 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (imp A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (all A)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (ex A)}
subgoal 11 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H6.
11 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (imp A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (all A)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (ex A)}
subgoal 11 is:
{L |- conc C}
cut_admissibility < search.
10 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (or A B)}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (imp A B)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (all A)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (ex A)}
subgoal 10 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H6.
10 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (or A B)}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (imp A B)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (all A)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (ex A)}
subgoal 10 is:
{L |- conc C}
cut_admissibility < case H5.
10 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (or A B)}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (imp A B)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (all A)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (ex A)}
subgoal 10 is:
{L |- conc C}
cut_admissibility < case H8.
11 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (imp A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (all A)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (ex A)}
subgoal 11 is:
{L |- conc C}
cut_admissibility < apply and_left_inv to _ H3.
11 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (imp A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (all A)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (ex A)}
subgoal 11 is:
{L |- conc C}
cut_admissibility < apply and_right_inv to _ H3.
11 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (imp A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (all A)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (ex A)}
subgoal 11 is:
{L |- conc C}
cut_admissibility < case H1.
11 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop A}*
H12 : {prop B}*
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (imp A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (all A)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (ex A)}
subgoal 11 is:
{L |- conc C}
cut_admissibility < apply IH to H11 _ H9 H7.
11 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop A}*
H12 : {prop B}*
H13 : {L, hyp B |- conc C}
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (imp A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (all A)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (ex A)}
subgoal 11 is:
{L |- conc C}
cut_admissibility < apply IH to H12 _ H10 H13.
11 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop A}*
H12 : {prop B}*
H13 : {L, hyp B |- conc C}
H14 : {L |- conc C}
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc (or A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (imp A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (all A)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (ex A)}
subgoal 11 is:
{L |- conc C}
cut_admissibility < search.
10 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (or A B)}
subgoal 3 is:
{L |- conc (or A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (imp A B)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (all A)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (ex A)}
subgoal 10 is:
{L |- conc C}
cut_admissibility < search.
9 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
============================
{L |- conc (or A B)}
subgoal 2 is:
{L |- conc (or A B)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (imp A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (all A)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (ex A)}
subgoal 9 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 H2 H3 H5.
9 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc A}**
H6 : {L |- conc A}
============================
{L |- conc (or A B)}
subgoal 2 is:
{L |- conc (or A B)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (imp A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (all A)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (ex A)}
subgoal 9 is:
{L |- conc C}
cut_admissibility < search.
8 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc B}**
============================
{L |- conc (or A B)}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (imp A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (all A)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (ex A)}
subgoal 8 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 H2 H3 H5.
8 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc B}**
H6 : {L |- conc B}
============================
{L |- conc (or A B)}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (imp A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (all A)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (ex A)}
subgoal 8 is:
{L |- conc C}
cut_admissibility < search.
7 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (imp A B)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (all A)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (ex A)}
subgoal 7 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H6.
7 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (imp A B)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (all A)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (ex A)}
subgoal 7 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H7.
7 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (imp A B)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (all A)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (ex A)}
subgoal 7 is:
{L |- conc C}
cut_admissibility < case H5.
7 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (imp A B)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (all A)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (ex A)}
subgoal 7 is:
{L |- conc C}
cut_admissibility < case H10.
8 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (imp A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (all A)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (ex A)}
subgoal 8 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}.
9 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (imp A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (all A)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (ex A)}
subgoal 9 is:
{L |- conc C}
cut_admissibility < induction on 2.
9 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (imp A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (all A)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (ex A)}
subgoal 9 is:
{L |- conc C}
cut_admissibility < intros.
9 subgoal(s).
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (imp A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (all A)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (ex A)}
subgoal 9 is:
{L |- conc C}
cut_admissibility < case H12.
18 subgoal(s).
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L1 |- conc D}
subgoal 8 is:
{L1 |- conc D}
subgoal 9 is:
{L1 |- conc D}
subgoal 10 is:
{L1 |- conc D}
subgoal 11 is:
{L |- conc C}
subgoal 12 is:
{L |- conc C}
subgoal 13 is:
{L |- conc (imp A B)}
subgoal 14 is:
{L |- conc C}
subgoal 15 is:
{L |- conc (all A)}
subgoal 16 is:
{L |- conc C}
subgoal 17 is:
{L |- conc (ex A)}
subgoal 18 is:
{L |- conc C}
cut_admissibility < apply ctx_lemma to H11 H15.
17 subgoal(s).
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L1 |- conc D}
subgoal 8 is:
{L1 |- conc D}
subgoal 9 is:
{L1 |- conc D}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc C}
subgoal 12 is:
{L |- conc (imp A B)}
subgoal 13 is:
{L |- conc C}
subgoal 14 is:
{L |- conc (all A)}
subgoal 15 is:
{L |- conc C}
subgoal 16 is:
{L |- conc (ex A)}
subgoal 17 is:
{L |- conc C}
cut_admissibility < search.
16 subgoal(s).
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L1 |- conc D}
subgoal 8 is:
{L1 |- conc D}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (imp A B)}
subgoal 12 is:
{L |- conc C}
subgoal 13 is:
{L |- conc (all A)}
subgoal 14 is:
{L |- conc C}
subgoal 15 is:
{L |- conc (ex A)}
subgoal 16 is:
{L |- conc C}
cut_admissibility < search.
15 subgoal(s).
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L1 |- conc D}
subgoal 8 is:
{L |- conc C}
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 IH2 to _ H16 H13 H14.
15 subgoal(s).
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L1 |- conc D}
subgoal 8 is:
{L |- conc C}
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.
14 subgoal(s).
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (imp A B)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (all A)}
subgoal 12 is:
{L |- conc C}
subgoal 13 is:
{L |- conc (ex A)}
subgoal 14 is:
{L |- conc C}
cut_admissibility < case H1.
14 subgoal(s).
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop A}*
H17 : {prop B}*
============================
{L1 |- conc D}
subgoal 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (imp A B)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (all A)}
subgoal 12 is:
{L |- conc C}
subgoal 13 is:
{L |- conc (ex A)}
subgoal 14 is:
{L |- conc C}
cut_admissibility < apply IH to H16 H11 H15 H13.
14 subgoal(s).
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop A}*
H17 : {prop B}*
H18 : {L1 |- conc D}
============================
{L1 |- conc D}
subgoal 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (imp A B)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (all A)}
subgoal 12 is:
{L |- conc C}
subgoal 13 is:
{L |- conc (ex A)}
subgoal 14 is:
{L |- conc C}
cut_admissibility < search.
13 subgoal(s).
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (imp A B)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (all A)}
subgoal 11 is:
{L |- conc C}
subgoal 12 is:
{L |- conc (ex A)}
subgoal 13 is:
{L |- conc C}
cut_admissibility < case H1.
13 subgoal(s).
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop A}*
H17 : {prop B}*
============================
{L1 |- conc D}
subgoal 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (imp A B)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (all A)}
subgoal 11 is:
{L |- conc C}
subgoal 12 is:
{L |- conc (ex A)}
subgoal 13 is:
{L |- conc C}
cut_admissibility < apply IH to H17 H11 H15 H14.
13 subgoal(s).
Variables: L, K, C, B, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop A}*
H17 : {prop B}*
H18 : {L1 |- conc D}
============================
{L1 |- conc D}
subgoal 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (imp A B)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (all A)}
subgoal 11 is:
{L |- conc C}
subgoal 12 is:
{L |- conc (ex A)}
subgoal 13 is:
{L |- conc C}
cut_admissibility < search.
12 subgoal(s).
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (imp A B)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (all A)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (ex A)}
subgoal 12 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H16 H13 H14.
12 subgoal(s).
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (imp A B)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (all A)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (ex A)}
subgoal 12 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H17 H13 H14.
12 subgoal(s).
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (imp A B)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (all A)}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc (ex A)}
subgoal 12 is:
{L |- conc C}
cut_admissibility < search.
11 subgoal(s).
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (imp A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (all A)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (ex A)}
subgoal 11 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H17 H13 H14.
11 subgoal(s).
Variables: L, K, C, B, A, L1, D, B1, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (imp A B)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (all A)}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc (ex A)}
subgoal 11 is:
{L |- conc C}
cut_admissibility < search.
10 subgoal(s).
Variables: L, K, C, B, A, L1, D, T, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (imp A B)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (all A)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (ex A)}
subgoal 10 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H16 H13 H14.
10 subgoal(s).
Variables: L, K, C, B, A, L1, D, T, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (imp A B)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (all A)}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc (ex A)}
subgoal 10 is:
{L |- conc C}
cut_admissibility < search.
9 subgoal(s).
Variables: L, K, C, B, A, L1, D, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (imp A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (all A)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (ex A)}
subgoal 9 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H16 H13 H14.
9 subgoal(s).
Variables: L, K, C, B, A, L1, D, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (imp A B)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (all A)}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc (ex A)}
subgoal 9 is:
{L |- conc C}
cut_admissibility < search.
8 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (imp A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (all A)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (ex A)}
subgoal 8 is:
{L |- conc C}
cut_admissibility < apply H11 to H2 H3 H8 H9.
8 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (imp A B)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (all A)}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc (ex A)}
subgoal 8 is:
{L |- conc C}
cut_admissibility < search.
7 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (imp A B)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (all A)}
subgoal 5 is:
{L |- conc C}
subgoal 6 is:
{L |- conc (ex A)}
subgoal 7 is:
{L |- conc C}
cut_admissibility < search.
6 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K, hyp A |- conc B}**
============================
{L |- conc (imp A B)}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (all A)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (ex A)}
subgoal 6 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H5.
6 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (all A)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (ex A)}
subgoal 6 is:
{L |- conc C}
cut_admissibility < search.
5 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (all A)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (ex A)}
subgoal 5 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H6.
5 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (all A)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (ex A)}
subgoal 5 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H7.
5 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (all A)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (ex A)}
subgoal 5 is:
{L |- conc C}
cut_admissibility < case H5.
5 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (all A)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (ex A)}
subgoal 5 is:
{L |- conc C}
cut_admissibility < case H10.
6 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (all A)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (ex A)}
subgoal 6 is:
{L |- conc C}
cut_admissibility < apply imp_inv to _ H3.
6 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (all A)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (ex A)}
subgoal 6 is:
{L |- conc C}
cut_admissibility < case H1.
6 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop A}*
H13 : {prop B}*
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (all A)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (ex A)}
subgoal 6 is:
{L |- conc C}
cut_admissibility < apply IH to H12 _ H8 H11.
6 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop A}*
H13 : {prop B}*
H14 : {L |- conc B}
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (all A)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (ex A)}
subgoal 6 is:
{L |- conc C}
cut_admissibility < apply IH to H13 _ H14 H9.
6 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop A}*
H13 : {prop B}*
H14 : {L |- conc B}
H15 : {L |- conc C}
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (all A)}
subgoal 4 is:
{L |- conc C}
subgoal 5 is:
{L |- conc (ex A)}
subgoal 6 is:
{L |- conc C}
cut_admissibility < search.
5 subgoal(s).
Variables: L, K, C, B, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (all A)}
subgoal 3 is:
{L |- conc C}
subgoal 4 is:
{L |- conc (ex A)}
subgoal 5 is:
{L |- conc C}
cut_admissibility < search.
4 subgoal(s).
Variables: L, K, C, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc (A n1)}**
============================
{L |- conc (all A)}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (ex A)}
subgoal 4 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H5.
4 subgoal(s).
Variables: L, K, C, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (ex A)}
subgoal 4 is:
{L |- conc C}
cut_admissibility < search.
3 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (ex A)}
subgoal 3 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 _ H3 H6.
3 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (ex A)}
subgoal 3 is:
{L |- conc C}
cut_admissibility < case H5.
3 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (ex A)}
subgoal 3 is:
{L |- conc C}
cut_admissibility < case H8.
4 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (ex A)}
subgoal 4 is:
{L |- conc C}
cut_admissibility < apply all_inv to _ H3.
4 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (ex A)}
subgoal 4 is:
{L |- conc C}
cut_admissibility < case H1.
4 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop (A n1)}*
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (ex A)}
subgoal 4 is:
{L |- conc C}
cut_admissibility < inst H9 with n1 = T.
4 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop (A n1)}*
H11 : {L |- conc (A T)}
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (ex A)}
subgoal 4 is:
{L |- conc C}
cut_admissibility < inst H10 with n1 = T.
4 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop (A n1)}*
H11 : {L |- conc (A T)}
H12 : {prop (A T)}*
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (ex A)}
subgoal 4 is:
{L |- conc C}
cut_admissibility < apply IH to H12 _ H11 H7.
4 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop 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 : {prop (A n1)}*
H11 : {L |- conc (A T)}
H12 : {prop (A T)}*
H13 : {L |- conc C}
============================
{L |- conc C}
subgoal 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc (ex A)}
subgoal 4 is:
{L |- conc C}
cut_admissibility < search.
3 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc (ex A)}
subgoal 3 is:
{L |- conc C}
cut_admissibility < search.
2 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop K}@
H2 : ctx L
H3 : {L |- conc K}
H5 : {L, hyp K |- conc (A T)}**
============================
{L |- conc (ex A)}
subgoal 2 is:
{L |- conc C}
cut_admissibility < apply IH1 to H1 H2 H3 H5.
2 subgoal(s).
Variables: L, K, C, T, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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 2 is:
{L |- conc C}
cut_admissibility < search.
1 subgoal(s).
Variables: L, K, C, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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.
1 subgoal(s).
Variables: L, K, C, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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.
1 subgoal(s).
Variables: L, K, C, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop 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.
2 subgoal(s).
Variables: L, K, C, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 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}.
3 subgoal(s).
Variables: L, K, C, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
cut_admissibility < induction on 2.
3 subgoal(s).
Variables: L, K, C, A
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
cut_admissibility < intros.
3 subgoal(s).
Variables: L, K, C, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L |- conc C}
subgoal 3 is:
{L |- conc C}
cut_admissibility < case H10.
11 subgoal(s).
Variables: L, K, C, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L1 |- conc D}
subgoal 8 is:
{L1 |- conc D}
subgoal 9 is:
{L1 |- conc D}
subgoal 10 is:
{L |- conc C}
subgoal 11 is:
{L |- conc C}
cut_admissibility < apply ctx_lemma to H9 H12.
10 subgoal(s).
Variables: L, K, C, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L1 |- conc D}
subgoal 8 is:
{L1 |- conc D}
subgoal 9 is:
{L |- conc C}
subgoal 10 is:
{L |- conc C}
cut_admissibility < search.
9 subgoal(s).
Variables: L, K, C, A, L1, D
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L1 |- conc D}
subgoal 8 is:
{L |- conc C}
subgoal 9 is:
{L |- conc C}
cut_admissibility < search.
8 subgoal(s).
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H13 H11.
8 subgoal(s).
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L1 |- conc D}
subgoal 7 is:
{L |- conc C}
subgoal 8 is:
{L |- conc C}
cut_admissibility < search.
7 subgoal(s).
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H13 H11.
7 subgoal(s).
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc C}
cut_admissibility < apply IH2 to _ H14 H11.
7 subgoal(s).
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C}** -> {L |- conc C}
H1 : {prop (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 2 is:
{L1 |- conc D}
subgoal 3 is:
{L1 |- conc D}
subgoal 4 is:
{L1 |- conc D}
subgoal 5 is:
{L1 |- conc D}
subgoal 6 is:
{L |- conc C}
subgoal 7 is:
{L |- conc C}
cut_admissibility < search.
6 subgoal(s).
Variables: L, K, C, A, L1, D, B, A1
IH : forall L K C, {prop K}* -> ctx L -> {L |- conc K} ->
{L, hyp K |- conc C} -> {L |- conc C}
IH1 : forall L K C, {prop K}@ -> ctx L -> {L |- conc K} ->
{L, hyp 