Welcome to Abella 2.0.5-dev.

Abella <Specification "equiv".Reading specification "equiv".

Abella <Define ctxs : olist -> olist -> olist -> prop by ctxs nil nil nil; ctxs (nd G :: L) (hyp G :: J) (hil G :: K) := ctxs L J K.

Abella <Theorem ctxs_member1 : forall L J K E, ctxs L J K -> member E L -> (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K).

============================ forall L J K E, ctxs L J K -> member E L -> (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K) ctxs_member1 <induction on 2.

IH : forall L J K E, ctxs L J K -> member E L * -> (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K) ============================ forall L J K E, ctxs L J K -> member E L @ -> (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K) ctxs_member1 <intros.

Variables: L J K E IH : forall L J K E, ctxs L J K -> member E L * -> (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K) H1 : ctxs L J K H2 : member E L @ ============================ exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K ctxs_member1 <case H2.

Subgoal 1: Variables: J K E L1 IH : forall L J K E, ctxs L J K -> member E L * -> (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K) H1 : ctxs (E :: L1) J K ============================ exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K Subgoal 2 is: exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K ctxs_member1 <case H1.

Subgoal 1: Variables: L1 K1 G J1 IH : forall L J K E, ctxs L J K -> member E L * -> (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K) H3 : ctxs L1 J1 K1 ============================ exists F, nd G = nd F /\ member (hyp F) (hyp G :: J1) /\ member (hil F) (hil G :: K1) Subgoal 2 is: exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K ctxs_member1 <search.

Subgoal 2: Variables: J K E L1 B IH : forall L J K E, ctxs L J K -> member E L * -> (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K) H1 : ctxs (B :: L1) J K H3 : member E L1 * ============================ exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K ctxs_member1 <case H1.

Subgoal 2: Variables: E L1 K1 G J1 IH : forall L J K E, ctxs L J K -> member E L * -> (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K) H3 : member E L1 * H4 : ctxs L1 J1 K1 ============================ exists F, E = nd F /\ member (hyp F) (hyp G :: J1) /\ member (hil F) (hil G :: K1) ctxs_member1 <apply IH to H4 H3.

Subgoal 2: Variables: L1 K1 G J1 F IH : forall L J K E, ctxs L J K -> member E L * -> (exists F, E = nd F /\ member (hyp F) J /\ member (hil F) K) H3 : member (nd F) L1 * H4 : ctxs L1 J1 K1 H5 : member (hyp F) J1 H6 : member (hil F) K1 ============================ exists F1, nd F = nd F1 /\ member (hyp F1) (hyp G :: J1) /\ member (hil F1) (hil G :: K1) ctxs_member1 <search.Proof completed.

Abella <Theorem ctxs_member2 : forall L J K E, ctxs L J K -> member E J -> (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K).

============================ forall L J K E, ctxs L J K -> member E J -> (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K) ctxs_member2 <induction on 2.

IH : forall L J K E, ctxs L J K -> member E J * -> (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K) ============================ forall L J K E, ctxs L J K -> member E J @ -> (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K) ctxs_member2 <intros.

Variables: L J K E IH : forall L J K E, ctxs L J K -> member E J * -> (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K) H1 : ctxs L J K H2 : member E J @ ============================ exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K ctxs_member2 <case H2.

Subgoal 1: Variables: L K E L1 IH : forall L J K E, ctxs L J K -> member E J * -> (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K) H1 : ctxs L (E :: L1) K ============================ exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K Subgoal 2 is: exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K ctxs_member2 <case H1.

Subgoal 1: Variables: L1 K1 G L2 IH : forall L J K E, ctxs L J K -> member E J * -> (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K) H3 : ctxs L2 L1 K1 ============================ exists F, hyp G = hyp F /\ member (nd F) (nd G :: L2) /\ member (hil F) (hil G :: K1) Subgoal 2 is: exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K ctxs_member2 <search.

Subgoal 2: Variables: L K E L1 B IH : forall L J K E, ctxs L J K -> member E J * -> (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K) H1 : ctxs L (B :: L1) K H3 : member E L1 * ============================ exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K ctxs_member2 <case H1.

Subgoal 2: Variables: E L1 K1 G L2 IH : forall L J K E, ctxs L J K -> member E J * -> (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K) H3 : member E L1 * H4 : ctxs L2 L1 K1 ============================ exists F, E = hyp F /\ member (nd F) (nd G :: L2) /\ member (hil F) (hil G :: K1) ctxs_member2 <apply IH to H4 H3.

Subgoal 2: Variables: L1 K1 G L2 F IH : forall L J K E, ctxs L J K -> member E J * -> (exists F, E = hyp F /\ member (nd F) L /\ member (hil F) K) H3 : member (hyp F) L1 * H4 : ctxs L2 L1 K1 H5 : member (nd F) L2 H6 : member (hil F) K1 ============================ exists F1, hyp F = hyp F1 /\ member (nd F1) (nd G :: L2) /\ member (hil F1) (hil G :: K1) ctxs_member2 <search.Proof completed.

Abella <Theorem ctxs_member3 : forall L J K E, ctxs L J K -> member E K -> (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J).

============================ forall L J K E, ctxs L J K -> member E K -> (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J) ctxs_member3 <induction on 2.

IH : forall L J K E, ctxs L J K -> member E K * -> (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J) ============================ forall L J K E, ctxs L J K -> member E K @ -> (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J) ctxs_member3 <intros.

Variables: L J K E IH : forall L J K E, ctxs L J K -> member E K * -> (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J) H1 : ctxs L J K H2 : member E K @ ============================ exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J ctxs_member3 <case H2.

Subgoal 1: Variables: L J E L1 IH : forall L J K E, ctxs L J K -> member E K * -> (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J) H1 : ctxs L J (E :: L1) ============================ exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J Subgoal 2 is: exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J ctxs_member3 <case H1.

Subgoal 1: Variables: L1 G J1 L2 IH : forall L J K E, ctxs L J K -> member E K * -> (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J) H3 : ctxs L2 J1 L1 ============================ exists F, hil G = hil F /\ member (nd F) (nd G :: L2) /\ member (hyp F) (hyp G :: J1) Subgoal 2 is: exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J ctxs_member3 <search.

Subgoal 2: Variables: L J E L1 B IH : forall L J K E, ctxs L J K -> member E K * -> (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J) H1 : ctxs L J (B :: L1) H3 : member E L1 * ============================ exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J ctxs_member3 <case H1.

Subgoal 2: Variables: E L1 G J1 L2 IH : forall L J K E, ctxs L J K -> member E K * -> (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J) H3 : member E L1 * H4 : ctxs L2 J1 L1 ============================ exists F, E = hil F /\ member (nd F) (nd G :: L2) /\ member (hyp F) (hyp G :: J1) ctxs_member3 <apply IH to H4 H3.

Subgoal 2: Variables: L1 G J1 L2 F IH : forall L J K E, ctxs L J K -> member E K * -> (exists F, E = hil F /\ member (nd F) L /\ member (hyp F) J) H3 : member (hil F) L1 * H4 : ctxs L2 J1 L1 H5 : member (nd F) L2 H6 : member (hyp F) J1 ============================ exists F1, hil F = hil F1 /\ member (nd F1) (nd G :: L2) /\ member (hyp F1) (hyp G :: J1) ctxs_member3 <search.Proof completed.

Abella <Theorem nd_to_seq_ext : forall L J K G, ctxs L J K -> {L |- nd G} -> {J |- conc G}.

============================ forall L J K G, ctxs L J K -> {L |- nd G} -> {J |- conc G} nd_to_seq_ext <induction on 2.

IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G} ============================ forall L J K G, ctxs L J K -> {L |- nd G}@ -> {J |- conc G} nd_to_seq_ext <intros.

Variables: L J K G IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G} H1 : ctxs L J K H2 : {L |- nd G}@ ============================ {J |- conc G} nd_to_seq_ext <case H2.

Subgoal 1: Variables: L J K B A IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G} H1 : ctxs L J K H3 : {L, nd A |- nd B}* ============================ {J |- conc (imp A B)} Subgoal 2 is: {J |- conc G} Subgoal 3 is: {J |- conc G} nd_to_seq_ext <apply IH to _ H3.

Subgoal 1: Variables: L J K B A IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G} H1 : ctxs L J K H3 : {L, nd A |- nd B}* H4 : {J, hyp A |- conc B} ============================ {J |- conc (imp A B)} Subgoal 2 is: {J |- conc G} Subgoal 3 is: {J |- conc G} nd_to_seq_ext <search.

Subgoal 2: Variables: L J K G A IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G} H1 : ctxs L J K H3 : {L |- nd (imp A G)}* H4 : {L |- nd A}* ============================ {J |- conc G} Subgoal 3 is: {J |- conc G} nd_to_seq_ext <apply IH to H1 H3.

Subgoal 2: Variables: L J K G A IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G} H1 : ctxs L J K H3 : {L |- nd (imp A G)}* H4 : {L |- nd A}* H5 : {J |- conc (imp A G)} ============================ {J |- conc G} Subgoal 3 is: {J |- conc G} nd_to_seq_ext <apply IH to H1 H4.

Subgoal 2: Variables: L J K G A IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G} H1 : ctxs L J K H3 : {L |- nd (imp A G)}* H4 : {L |- nd A}* H5 : {J |- conc (imp A G)} H6 : {J |- conc A} ============================ {J |- conc G} Subgoal 3 is: {J |- conc G} nd_to_seq_ext <search.

Subgoal 3: Variables: L J K G F IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G} H1 : ctxs L J K H3 : {L, [F] |- nd G}* H4 : member F L ============================ {J |- conc G} nd_to_seq_ext <apply ctxs_member1 to H1 H4.

Subgoal 3: Variables: L J K G F1 IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G} H1 : ctxs L J K H3 : {L, [nd F1] |- nd G}* H4 : member (nd F1) L H5 : member (hyp F1) J H6 : member (hil F1) K ============================ {J |- conc G} nd_to_seq_ext <case H3.

Subgoal 3: Variables: L J K G IH : forall L J K G, ctxs L J K -> {L |- nd G}* -> {J |- conc G} H1 : ctxs L J K H4 : member (nd G) L H5 : member (hyp G) J H6 : member (hil G) K ============================ {J |- conc G} nd_to_seq_ext <search.Proof completed.

Abella <Theorem nd_to_seq : forall G, {nd G} -> {conc G}.

============================ forall G, {nd G} -> {conc G} nd_to_seq <intros.

Variables: G H1 : {nd G} ============================ {conc G} nd_to_seq <apply nd_to_seq_ext to _ H1.

Variables: G H1 : {nd G} H2 : {conc G} ============================ {conc G} nd_to_seq <search.Proof completed.

Abella <Set witnesses on.

Abella <Theorem hil_deduction : forall L J K A B, ctxs L J K -> {K, hil A |- hil B} -> {K |- hil (imp A B)}.

============================ forall L J K A B, ctxs L J K -> {K, hil A |- hil B} -> {K |- hil (imp A B)} hil_deduction <induction on 2.

IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} ============================ forall L J K A B, ctxs L J K -> {K, hil A |- hil B}@ -> {K |- hil (imp A B)} hil_deduction <intros.

Variables: L J K A B IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K H2 : {K, hil A |- hil B}@ ============================ {K |- hil (imp A B)} hil_deduction <case H2.

Subgoal 1: Variables: L J K A A1 B1 IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K ============================ {K |- hil (imp A (imp A1 (imp B1 A1)))} Subgoal 2 is: {K |- hil (imp A (imp (imp A1 (imp B1 C)) (imp (imp A1 B1) (imp A1 C))))} Subgoal 3 is: {K |- hil (imp A B)} Subgoal 4 is: {K |- hil (imp A B)} hil_deduction <search.Witness: unfold(hil, 3, unfold(hil, 1), unfold(hil, 1)).

Subgoal 2: Variables: L J K A C A1 B1 IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K ============================ {K |- hil (imp A (imp (imp A1 (imp B1 C)) (imp (imp A1 B1) (imp A1 C))))} Subgoal 3 is: {K |- hil (imp A B)} Subgoal 4 is: {K |- hil (imp A B)} hil_deduction <search.Witness: unfold(hil, 3, unfold(hil, 1), unfold(hil, 2)).

Subgoal 3: Variables: L J K A B A1 IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K H3 : {K, hil A |- hil (imp A1 B)}* H4 : {K, hil A |- hil A1}* ============================ {K |- hil (imp A B)} Subgoal 4 is: {K |- hil (imp A B)} hil_deduction <apply IH to _ H3.Witness: apply H1.

Subgoal 3: Variables: L J K A B A1 IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K H3 : {K, hil A |- hil (imp A1 B)}* H4 : {K, hil A |- hil A1}* H5 : {K |- hil (imp A (imp A1 B))} ============================ {K |- hil (imp A B)} Subgoal 4 is: {K |- hil (imp A B)} hil_deduction <apply IH to _ H4.Witness: apply H1.

Subgoal 3: Variables: L J K A B A1 IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K H3 : {K, hil A |- hil (imp A1 B)}* H4 : {K, hil A |- hil A1}* H5 : {K |- hil (imp A (imp A1 B))} H6 : {K |- hil (imp A A1)} ============================ {K |- hil (imp A B)} Subgoal 4 is: {K |- hil (imp A B)} hil_deduction <search.Witness: unfold(hil, 3, unfold(hil, 3, unfold(hil, 1), unfold(hil, 3, unfold(hil, 3, unfold(hil, 2), apply H5), apply H6)), apply H5).

Subgoal 4: Variables: L J K A B F IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K H3 : {K, hil A, [F] |- hil B}* H4 : member F (hil A :: K) ============================ {K |- hil (imp A B)} hil_deduction <case H4.

Subgoal 4.1: Variables: L J K A B IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K H3 : {K, hil A, [hil A] |- hil B}* ============================ {K |- hil (imp A B)} Subgoal 4.2 is: {K |- hil (imp A B)} hil_deduction <case H3.

Subgoal 4.1: Variables: L J K B IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K ============================ {K |- hil (imp B B)} Subgoal 4.2 is: {K |- hil (imp A B)} hil_deduction <search.Witness: unfold(hil, 3, unfold(hil, 3, unfold(hil, 1), unfold(hil, 3, unfold(hil, 3, unfold(hil, 2), unfold(hil, 1)), unfold(hil, 1))), unfold(hil, 1)).

Subgoal 4.2: Variables: L J K A B F IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K H3 : {K, hil A, [F] |- hil B}* H5 : member F K ============================ {K |- hil (imp A B)} hil_deduction <apply ctxs_member3 to H1 H5.

Subgoal 4.2: Variables: L J K A B F1 IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K H3 : {K, hil A, [hil F1] |- hil B}* H5 : member (hil F1) K H6 : member (nd F1) L H7 : member (hyp F1) J ============================ {K |- hil (imp A B)} hil_deduction <case H3.

Subgoal 4.2: Variables: L J K A B IH : forall L J K A B, ctxs L J K -> {K, hil A |- hil B}* -> {K |- hil (imp A B)} H1 : ctxs L J K H5 : member (hil B) K H6 : member (nd B) L H7 : member (hyp B) J ============================ {K |- hil (imp A B)} hil_deduction <search.Witness: unfold(hil, 3, unfold(hil, 1), unfold(hil, 3, unfold(hil, 3, unfold(hil, 1), unfold(hil, 1)), unfold(hil, 1))). Proof completed.

Abella <Set witnesses off.

Abella <Theorem seq_to_hil_ext : forall L J K G, ctxs L J K -> {J |- conc G} -> {K |- hil G}.

============================ forall L J K G, ctxs L J K -> {J |- conc G} -> {K |- hil G} seq_to_hil_ext <induction on 2.

IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} ============================ forall L J K G, ctxs L J K -> {J |- conc G}@ -> {K |- hil G} seq_to_hil_ext <intros.

Variables: L J K G IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H2 : {J |- conc G}@ ============================ {K |- hil G} seq_to_hil_ext <case H2.

Subgoal 1: Variables: L J K G IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H3 : {J |- hyp G}* ============================ {K |- hil G} Subgoal 2 is: {K |- hil G} Subgoal 3 is: {K |- hil (imp A B)} Subgoal 4 is: {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <case H3.

Subgoal 1: Variables: L J K G F IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H4 : {J, [F] |- hyp G}* H5 : member F J ============================ {K |- hil G} Subgoal 2 is: {K |- hil G} Subgoal 3 is: {K |- hil (imp A B)} Subgoal 4 is: {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <apply ctxs_member2 to H1 H5.

Subgoal 1: Variables: L J K G F1 IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H4 : {J, [hyp F1] |- hyp G}* H5 : member (hyp F1) J H6 : member (nd F1) L H7 : member (hil F1) K ============================ {K |- hil G} Subgoal 2 is: {K |- hil G} Subgoal 3 is: {K |- hil (imp A B)} Subgoal 4 is: {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <case H4.

Subgoal 1: Variables: L J K G IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H5 : member (hyp G) J H6 : member (nd G) L H7 : member (hil G) K ============================ {K |- hil G} Subgoal 2 is: {K |- hil G} Subgoal 3 is: {K |- hil (imp A B)} Subgoal 4 is: {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <search.

Subgoal 2: Variables: L J K G A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H3 : {J, hyp A |- conc G}* H4 : {J |- conc A}* ============================ {K |- hil G} Subgoal 3 is: {K |- hil (imp A B)} Subgoal 4 is: {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <apply IH to _ H3.

Subgoal 2: Variables: L J K G A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H3 : {J, hyp A |- conc G}* H4 : {J |- conc A}* H5 : {K, hil A |- hil G} ============================ {K |- hil G} Subgoal 3 is: {K |- hil (imp A B)} Subgoal 4 is: {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <apply IH to H1 H4.

Subgoal 2: Variables: L J K G A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H3 : {J, hyp A |- conc G}* H4 : {J |- conc A}* H5 : {K, hil A |- hil G} H6 : {K |- hil A} ============================ {K |- hil G} Subgoal 3 is: {K |- hil (imp A B)} Subgoal 4 is: {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <apply hil_deduction to _ H5.

Subgoal 2: Variables: L J K G A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H3 : {J, hyp A |- conc G}* H4 : {J |- conc A}* H5 : {K, hil A |- hil G} H6 : {K |- hil A} H7 : {K |- hil (imp A G)} ============================ {K |- hil G} Subgoal 3 is: {K |- hil (imp A B)} Subgoal 4 is: {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <search.

Subgoal 3: Variables: L J K B A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H3 : {J, hyp A |- conc B}* ============================ {K |- hil (imp A B)} Subgoal 4 is: {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <apply IH to _ H3.

Subgoal 3: Variables: L J K B A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H3 : {J, hyp A |- conc B}* H4 : {K, hil A |- hil B} ============================ {K |- hil (imp A B)} Subgoal 4 is: {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <apply hil_deduction to _ H4.

Subgoal 3: Variables: L J K B A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H3 : {J, hyp A |- conc B}* H4 : {K, hil A |- hil B} H5 : {K |- hil (imp A B)} ============================ {K |- hil (imp A B)} Subgoal 4 is: {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <search.

Subgoal 4: Variables: L J K G B A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H3 : {J |- hyp (imp A B)}* H4 : {J |- conc A}* H5 : {J, hyp B |- conc G}* ============================ {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <case H3.

Subgoal 4: Variables: L J K G B A F IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H4 : {J |- conc A}* H5 : {J, hyp B |- conc G}* H6 : {J, [F] |- hyp (imp A B)}* H7 : member F J ============================ {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <apply ctxs_member2 to H1 H7.

Subgoal 4: Variables: L J K G B A F1 IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H4 : {J |- conc A}* H5 : {J, hyp B |- conc G}* H6 : {J, [hyp F1] |- hyp (imp A B)}* H7 : member (hyp F1) J H8 : member (nd F1) L H9 : member (hil F1) K ============================ {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <case H6.

Subgoal 4: Variables: L J K G B A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H4 : {J |- conc A}* H5 : {J, hyp B |- conc G}* H7 : member (hyp (imp A B)) J H8 : member (nd (imp A B)) L H9 : member (hil (imp A B)) K ============================ {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <apply IH to H1 H4.

Subgoal 4: Variables: L J K G B A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H4 : {J |- conc A}* H5 : {J, hyp B |- conc G}* H7 : member (hyp (imp A B)) J H8 : member (nd (imp A B)) L H9 : member (hil (imp A B)) K H10 : {K |- hil A} ============================ {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <apply IH to _ H5.

Subgoal 4: Variables: L J K G B A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H4 : {J |- conc A}* H5 : {J, hyp B |- conc G}* H7 : member (hyp (imp A B)) J H8 : member (nd (imp A B)) L H9 : member (hil (imp A B)) K H10 : {K |- hil A} H11 : {K, hil B |- hil G} ============================ {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <apply hil_deduction to _ H11.

Subgoal 4: Variables: L J K G B A IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H4 : {J |- conc A}* H5 : {J, hyp B |- conc G}* H7 : member (hyp (imp A B)) J H8 : member (nd (imp A B)) L H9 : member (hil (imp A B)) K H10 : {K |- hil A} H11 : {K, hil B |- hil G} H12 : {K |- hil (imp B G)} ============================ {K |- hil G} Subgoal 5 is: {K |- hil G} seq_to_hil_ext <search.

Subgoal 5: Variables: L J K G F IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H3 : {J, [F] |- conc G}* H4 : member F J ============================ {K |- hil G} seq_to_hil_ext <apply ctxs_member2 to H1 H4.

Subgoal 5: Variables: L J K G F1 IH : forall L J K G, ctxs L J K -> {J |- conc G}* -> {K |- hil G} H1 : ctxs L J K H3 : {J, [hyp F1] |- conc G}* H4 : member (hyp F1) J H5 : member (nd F1) L H6 : member (hil F1) K ============================ {K |- hil G} seq_to_hil_ext <case H3.Proof completed.

Abella <Theorem seq_to_hil : forall G, {conc G} -> {hil G}.

============================ forall G, {conc G} -> {hil G} seq_to_hil <intros.

Variables: G H1 : {conc G} ============================ {hil G} seq_to_hil <apply seq_to_hil_ext to _ H1.

Variables: G H1 : {conc G} H2 : {hil G} ============================ {hil G} seq_to_hil <search.Proof completed.

Abella <Theorem hil_to_nd_ext : forall L J K G, ctxs L J K -> {K |- hil G} -> {L |- nd G}.

============================ forall L J K G, ctxs L J K -> {K |- hil G} -> {L |- nd G} hil_to_nd_ext <induction on 2.

IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G} ============================ forall L J K G, ctxs L J K -> {K |- hil G}@ -> {L |- nd G} hil_to_nd_ext <intros.

Variables: L J K G IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G} H1 : ctxs L J K H2 : {K |- hil G}@ ============================ {L |- nd G} hil_to_nd_ext <case H2.

Subgoal 1: Variables: L J K A B IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G} H1 : ctxs L J K ============================ {L |- nd (imp A (imp B A))} Subgoal 2 is: {L |- nd (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))} Subgoal 3 is: {L |- nd G} Subgoal 4 is: {L |- nd G} hil_to_nd_ext <search.

Subgoal 2: Variables: L J K C A B IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G} H1 : ctxs L J K ============================ {L |- nd (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))} Subgoal 3 is: {L |- nd G} Subgoal 4 is: {L |- nd G} hil_to_nd_ext <assert {nd (imp A (imp B C)), nd (imp A B), nd A |- nd C}.

Subgoal 2: Variables: L J K C A B IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G} H1 : ctxs L J K H3 : {nd (imp A (imp B C)), nd (imp A B), nd A |- nd C} ============================ {L |- nd (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))} Subgoal 3 is: {L |- nd G} Subgoal 4 is: {L |- nd G} hil_to_nd_ext <search.

Subgoal 3: Variables: L J K G A IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G} H1 : ctxs L J K H3 : {K |- hil (imp A G)}* H4 : {K |- hil A}* ============================ {L |- nd G} Subgoal 4 is: {L |- nd G} hil_to_nd_ext <apply IH to H1 H3.

Subgoal 3: Variables: L J K G A IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G} H1 : ctxs L J K H3 : {K |- hil (imp A G)}* H4 : {K |- hil A}* H5 : {L |- nd (imp A G)} ============================ {L |- nd G} Subgoal 4 is: {L |- nd G} hil_to_nd_ext <apply IH to H1 H4.

Subgoal 3: Variables: L J K G A IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G} H1 : ctxs L J K H3 : {K |- hil (imp A G)}* H4 : {K |- hil A}* H5 : {L |- nd (imp A G)} H6 : {L |- nd A} ============================ {L |- nd G} Subgoal 4 is: {L |- nd G} hil_to_nd_ext <search.

Subgoal 4: Variables: L J K G F IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G} H1 : ctxs L J K H3 : {K, [F] |- hil G}* H4 : member F K ============================ {L |- nd G} hil_to_nd_ext <apply ctxs_member3 to H1 H4.

Subgoal 4: Variables: L J K G F1 IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G} H1 : ctxs L J K H3 : {K, [hil F1] |- hil G}* H4 : member (hil F1) K H5 : member (nd F1) L H6 : member (hyp F1) J ============================ {L |- nd G} hil_to_nd_ext <case H3.

Subgoal 4: Variables: L J K G IH : forall L J K G, ctxs L J K -> {K |- hil G}* -> {L |- nd G} H1 : ctxs L J K H4 : member (hil G) K H5 : member (nd G) L H6 : member (hyp G) J ============================ {L |- nd G} hil_to_nd_ext <search.Proof completed.

Abella <Theorem hil_to_nd : forall G, {hil G} -> {nd G}.

============================ forall G, {hil G} -> {nd G} hil_to_nd <intros.

Variables: G H1 : {hil G} ============================ {nd G} hil_to_nd <apply hil_to_nd_ext to _ H1.

Variables: G H1 : {hil G} H2 : {nd G} ============================ {nd G} hil_to_nd <search.Proof completed.

Abella <Define fold : olist -> form -> form -> prop by fold nil B B; fold (hil A :: L) B B' := fold L (imp A B) B'.

Abella <Theorem hil_deduction_generalized : forall L J K B B', ctxs L J K -> fold K B B' -> {K |- hil B} -> {hil B'}.

============================ forall L J K B B', ctxs L J K -> fold K B B' -> {K |- hil B} -> {hil B'} hil_deduction_generalized <induction on 2.

IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} -> {hil B'} ============================ forall L J K B B', ctxs L J K -> fold K B B' @ -> {K |- hil B} -> {hil B'} hil_deduction_generalized <intros.

Variables: L J K B B' IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} -> {hil B'} H1 : ctxs L J K H2 : fold K B B' @ H3 : {K |- hil B} ============================ {hil B'} hil_deduction_generalized <case H2.

Subgoal 1: Variables: L J B' IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} -> {hil B'} H1 : ctxs L J nil H3 : {hil B'} ============================ {hil B'} Subgoal 2 is: {hil B'} hil_deduction_generalized <search.

Subgoal 2: Variables: L J B B' L1 A IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} -> {hil B'} H1 : ctxs L J (hil A :: L1) H3 : {L1, hil A |- hil B} H4 : fold L1 (imp A B) B' * ============================ {hil B'} hil_deduction_generalized <case H1.

Subgoal 2: Variables: B B' L1 A J1 L2 IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} -> {hil B'} H3 : {L1, hil A |- hil B} H4 : fold L1 (imp A B) B' * H5 : ctxs L2 J1 L1 ============================ {hil B'} hil_deduction_generalized <apply hil_deduction to _ H3.

Subgoal 2: Variables: B B' L1 A J1 L2 IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} -> {hil B'} H3 : {L1, hil A |- hil B} H4 : fold L1 (imp A B) B' * H5 : ctxs L2 J1 L1 H6 : {L1 |- hil (imp A B)} ============================ {hil B'} hil_deduction_generalized <apply IH to _ H4 H6.

Subgoal 2: Variables: B B' L1 A J1 L2 IH : forall L J K B B', ctxs L J K -> fold K B B' * -> {K |- hil B} -> {hil B'} H3 : {L1, hil A |- hil B} H4 : fold L1 (imp A B) B' * H5 : ctxs L2 J1 L1 H6 : {L1 |- hil (imp A B)} H7 : {hil B'} ============================ {hil B'} hil_deduction_generalized <search.Proof completed.

Abella <