Welcome to Abella 2.0.4-dev

Abella <Specification "cr".Reading specification "cr"

Abella <Define ctxs : olist -> olist -> olist -> prop by ctxs nil nil nil; nabla x, ctxs (trm x :: L) (pr1 x x :: K) (cd1 x x :: notabs x :: J) := ctxs L K J.

Abella <Define name : tm -> prop by nabla x, name x.

Abella <Theorem trm_worlds : forall L K J E, ctxs L K J -> member E L -> (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J).

============================ forall L K J E, ctxs L K J -> member E L -> (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J) trm_worlds <induction on 2.

IH : forall L K J E, ctxs L K J -> member E L * -> (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J) ============================ forall L K J E, ctxs L K J -> member E L @ -> (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J) trm_worlds <intros.

Variables: L K J E IH : forall L K J E, ctxs L K J -> member E L * -> (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J) H1 : ctxs L K J H2 : member E L @ ============================ exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J trm_worlds <case H2.

Subgoal 1: Variables: K J E L1 IH : forall L K J E, ctxs L K J -> member E L * -> (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J) H1 : ctxs (E :: L1) K J ============================ exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J Subgoal 2 is: exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J trm_worlds <case H1.

Subgoal 1: Variables: J1 K1 L2 IH : forall L K J E, ctxs L K J -> member E L * -> (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J) H3 : ctxs L2 K1 J1 ============================ exists A, trm n1 = trm A /\ name A /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1) Subgoal 2 is: exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J trm_worlds <search.

Subgoal 2: Variables: K J E L1 B IH : forall L K J E, ctxs L K J -> member E L * -> (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J) H1 : ctxs (B :: L1) K J H3 : member E L1 * ============================ exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J trm_worlds <case H1.

Subgoal 2: Variables: E J1 K1 L2 IH : forall L K J E, ctxs L K J -> member E L * -> (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J) H3 : member (E n1) L2 * H4 : ctxs L2 K1 J1 ============================ exists A, E n1 = trm A /\ name A /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1) trm_worlds <apply IH to H4 H3.

Subgoal 2: Variables: J1 K1 L2 A IH : forall L K J E, ctxs L K J -> member E L * -> (exists A, E = trm A /\ name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J) H3 : member (trm (A n1)) L2 * H4 : ctxs L2 K1 J1 H5 : name (A n1) H6 : member (pr1 (A n1) (A n1)) K1 H7 : member (cd1 (A n1) (A n1)) J1 H8 : member (notabs (A n1)) J1 ============================ exists A1, trm (A n1) = trm A1 /\ name A1 /\ member (pr1 A1 A1) (pr1 n1 n1 :: K1) /\ member (cd1 A1 A1) (cd1 n1 n1 :: notabs n1 :: J1) /\ member (notabs A1) (cd1 n1 n1 :: notabs n1 :: J1) trm_worlds <search.Proof completed.

Abella <Theorem pr1_worlds : forall L K J E, ctxs L K J -> member E K -> (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J).

============================ forall L K J E, ctxs L K J -> member E K -> (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J) pr1_worlds <induction on 2.

IH : forall L K J E, ctxs L K J -> member E K * -> (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J) ============================ forall L K J E, ctxs L K J -> member E K @ -> (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J) pr1_worlds <intros.

Variables: L K J E IH : forall L K J E, ctxs L K J -> member E K * -> (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J) H1 : ctxs L K J H2 : member E K @ ============================ exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J pr1_worlds <case H2.

Subgoal 1: Variables: L J E L1 IH : forall L K J E, ctxs L K J -> member E K * -> (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J) H1 : ctxs L (E :: L1) J ============================ exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J Subgoal 2 is: exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J pr1_worlds <case H1.

Subgoal 1: Variables: J1 K1 L2 IH : forall L K J E, ctxs L K J -> member E K * -> (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J) H3 : ctxs L2 K1 J1 ============================ exists A B, pr1 n1 n1 = pr1 A B /\ name A /\ A = B /\ member (trm A) (trm n1 :: L2) /\ member (cd1 A B) (cd1 n1 n1 :: notabs n1 :: J1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1) Subgoal 2 is: exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J pr1_worlds <search.

Subgoal 2: Variables: L J E L1 B IH : forall L K J E, ctxs L K J -> member E K * -> (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J) H1 : ctxs L (B :: L1) J H3 : member E L1 * ============================ exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J pr1_worlds <case H1.

Subgoal 2: Variables: E J1 K1 L2 IH : forall L K J E, ctxs L K J -> member E K * -> (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J) H3 : member (E n1) K1 * H4 : ctxs L2 K1 J1 ============================ exists A B, E n1 = pr1 A B /\ name A /\ A = B /\ member (trm A) (trm n1 :: L2) /\ member (cd1 A B) (cd1 n1 n1 :: notabs n1 :: J1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1) pr1_worlds <apply IH to H4 H3.

Subgoal 2: Variables: J1 K1 L2 B1 IH : forall L K J E, ctxs L K J -> member E K * -> (exists A B, E = pr1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J) H3 : member (pr1 (B1 n1) (B1 n1)) K1 * H4 : ctxs L2 K1 J1 H5 : name (B1 n1) H6 : member (trm (B1 n1)) L2 H7 : member (cd1 (B1 n1) (B1 n1)) J1 H8 : member (notabs (B1 n1)) J1 ============================ exists A B, pr1 (B1 n1) (B1 n1) = pr1 A B /\ name A /\ A = B /\ member (trm A) (trm n1 :: L2) /\ member (cd1 A B) (cd1 n1 n1 :: notabs n1 :: J1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1) pr1_worlds <search.Proof completed.

Abella <Theorem cd_worlds : forall L K J E, ctxs L K J -> member E J -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J).

============================ forall L K J E, ctxs L K J -> member E J -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) cd_worlds <induction on 2.

IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) ============================ forall L K J E, ctxs L K J -> member E J @ -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) cd_worlds <intros.

Variables: L K J E IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) H1 : ctxs L K J H2 : member E J @ ============================ (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) cd_worlds <case H2.

Subgoal 1: Variables: L K E L1 IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) H1 : ctxs L K (E :: L1) ============================ (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) (E :: L1)) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) (E :: L1)) Subgoal 2 is: (exists A B1, E = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) (B :: L1)) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) (B :: L1)) cd_worlds <case H1.

Subgoal 1: Variables: J1 K1 L2 IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) H3 : ctxs L2 K1 J1 ============================ (exists A B, cd1 n1 n1 = cd1 A B /\ name A /\ A = B /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/ (exists A, cd1 n1 n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1)) Subgoal 2 is: (exists A B1, E = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) (B :: L1)) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) (B :: L1)) cd_worlds <search.

Subgoal 2: Variables: L K E L1 B IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) H1 : ctxs L K (B :: L1) H3 : member E L1 * ============================ (exists A B1, E = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) (B :: L1)) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) (B :: L1)) cd_worlds <case H1.

Subgoal 2: Variables: E J1 K1 L2 IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) H3 : member (E n1) (notabs n1 :: J1) * H4 : ctxs L2 K1 J1 ============================ (exists A B1, E n1 = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/ (exists A, E n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1)) cd_worlds <case H3.

Subgoal 2.1: Variables: J1 K1 L2 IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) H4 : ctxs L2 K1 J1 ============================ (exists A B1, notabs n1 = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/ (exists A, notabs n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1)) Subgoal 2.2 is: (exists A B1, E n1 = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/ (exists A, E n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1)) cd_worlds <right.

Subgoal 2.1: Variables: J1 K1 L2 IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) H4 : ctxs L2 K1 J1 ============================ exists A, notabs n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1) Subgoal 2.2 is: (exists A B1, E n1 = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/ (exists A, E n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1)) cd_worlds <search.

Subgoal 2.2: Variables: E J1 K1 L2 IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) H4 : ctxs L2 K1 J1 H5 : member (E n1) J1 * ============================ (exists A B1, E n1 = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/ (exists A, E n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1)) cd_worlds <apply IH to H4 H5.

Subgoal 2.2: Variables: E J1 K1 L2 IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) H4 : ctxs L2 K1 J1 H5 : member (E n1) J1 * H6 : (exists A B, E n1 = cd1 A B /\ name A /\ A = B /\ member (trm A) L2 /\ member (pr1 A A) K1 /\ member (notabs A) J1) \/ (exists A, E n1 = notabs A /\ name A /\ member (trm A) L2 /\ member (pr1 A A) K1 /\ member (cd1 A A) J1) ============================ (exists A B1, E n1 = cd1 A B1 /\ name A /\ A = B1 /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/ (exists A, E n1 = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1)) cd_worlds <case H6.

Subgoal 2.2.1: Variables: J1 K1 L2 B1 IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) H4 : ctxs L2 K1 J1 H5 : member (cd1 (B1 n1) (B1 n1)) J1 * H7 : name (B1 n1) H8 : member (trm (B1 n1)) L2 H9 : member (pr1 (B1 n1) (B1 n1)) K1 H10 : member (notabs (B1 n1)) J1 ============================ (exists A B2, cd1 (B1 n1) (B1 n1) = cd1 A B2 /\ name A /\ A = B2 /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (notabs A) (cd1 n1 n1 :: notabs n1 :: J1)) \/ (exists A, cd1 (B1 n1) (B1 n1) = notabs A /\ name A /\ member (trm A) (trm n1 :: L2) /\ member (pr1 A A) (pr1 n1 n1 :: K1) /\ member (cd1 A A) (cd1 n1 n1 :: notabs n1 :: J1)) Subgoal 2.2.2 is: (exists A1 B1, notabs (A n1) = cd1 A1 B1 /\ name A1 /\ A1 = B1 /\ member (trm A1) (trm n1 :: L2) /\ member (pr1 A1 A1) (pr1 n1 n1 :: K1) /\ member (notabs A1) (cd1 n1 n1 :: notabs n1 :: J1)) \/ (exists A1, notabs (A n1) = notabs A1 /\ name A1 /\ member (trm A1) (trm n1 :: L2) /\ member (pr1 A1 A1) (pr1 n1 n1 :: K1) /\ member (cd1 A1 A1) (cd1 n1 n1 :: notabs n1 :: J1)) cd_worlds <search.

Subgoal 2.2.2: Variables: J1 K1 L2 A IH : forall L K J E, ctxs L K J -> member E J * -> (exists A B, E = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, E = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) H4 : ctxs L2 K1 J1 H5 : member (notabs (A n1)) J1 * H7 : name (A n1) H8 : member (trm (A n1)) L2 H9 : member (pr1 (A n1) (A n1)) K1 H10 : member (cd1 (A n1) (A n1)) J1 ============================ (exists A1 B1, notabs (A n1) = cd1 A1 B1 /\ name A1 /\ A1 = B1 /\ member (trm A1) (trm n1 :: L2) /\ member (pr1 A1 A1) (pr1 n1 n1 :: K1) /\ member (notabs A1) (cd1 n1 n1 :: notabs n1 :: J1)) \/ (exists A1, notabs (A n1) = notabs A1 /\ name A1 /\ member (trm A1) (trm n1 :: L2) /\ member (pr1 A1 A1) (pr1 n1 n1 :: K1) /\ member (cd1 A1 A1) (cd1 n1 n1 :: notabs n1 :: J1)) cd_worlds <search.Proof completed.

Abella <Theorem notabs_abs_absurd : forall A L K J, ctxs L K J -> {J |- notabs (abs A)} -> false.

============================ forall A L K J, ctxs L K J -> {J |- notabs (abs A)} -> false notabs_abs_absurd <intros.

Variables: A L K J H1 : ctxs L K J H2 : {J |- notabs (abs A)} ============================ false notabs_abs_absurd <case H2.

Variables: A L K J F H1 : ctxs L K J H3 : {J, [F] |- notabs (abs A)} H4 : member F J ============================ false notabs_abs_absurd <apply cd_worlds to H1 H4.

Variables: A L K J F H1 : ctxs L K J H3 : {J, [F] |- notabs (abs A)} H4 : member F J H5 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, F = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) ============================ false notabs_abs_absurd <case H5.

Subgoal 1: Variables: A L K J B H1 : ctxs L K J H3 : {J, [cd1 B B] |- notabs (abs A)} H4 : member (cd1 B B) J H6 : name B H7 : member (trm B) L H8 : member (pr1 B B) K H9 : member (notabs B) J ============================ false Subgoal 2 is: false notabs_abs_absurd <case H3.

Subgoal 2: Variables: A L K J A1 H1 : ctxs L K J H3 : {J, [notabs A1] |- notabs (abs A)} H4 : member (notabs A1) J H6 : name A1 H7 : member (trm A1) L H8 : member (pr1 A1 A1) K H9 : member (cd1 A1 A1) J ============================ false notabs_abs_absurd <case H3.

Subgoal 2: Variables: A L K J H1 : ctxs L K J H4 : member (notabs (abs A)) J H6 : name (abs A) H7 : member (trm (abs A)) L H8 : member (pr1 (abs A) (abs A)) K H9 : member (cd1 (abs A) (abs A)) J ============================ false notabs_abs_absurd <case H6.Proof completed.

Abella <Theorem cd1_trm : forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {L |- trm A}.

============================ forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {L |- trm A} cd1_trm <induction on 2.

IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} ============================ forall A B L K J, ctxs L K J -> {J |- cd1 A B}@ -> {L |- trm A} cd1_trm <intros.

Variables: A B L K J IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H2 : {J |- cd1 A B}@ ============================ {L |- trm A} cd1_trm <case H2.

Subgoal 1: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J |- notabs T1}* H4 : {J |- cd1 T1 T2}* H5 : {J |- cd1 S1 S2}* ============================ {L |- trm (app T1 S1)} Subgoal 2 is: {L |- trm (abs S1)} Subgoal 3 is: {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} cd1_trm <apply IH to H1 H4.

Subgoal 1: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J |- notabs T1}* H4 : {J |- cd1 T1 T2}* H5 : {J |- cd1 S1 S2}* H6 : {L |- trm T1} ============================ {L |- trm (app T1 S1)} Subgoal 2 is: {L |- trm (abs S1)} Subgoal 3 is: {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} cd1_trm <apply IH to H1 H5.

Subgoal 1: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J |- notabs T1}* H4 : {J |- cd1 T1 T2}* H5 : {J |- cd1 S1 S2}* H6 : {L |- trm T1} H7 : {L |- trm S1} ============================ {L |- trm (app T1 S1)} Subgoal 2 is: {L |- trm (abs S1)} Subgoal 3 is: {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} cd1_trm <search.

Subgoal 2: Variables: L K J S2 S1 IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* ============================ {L |- trm (abs S1)} Subgoal 3 is: {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} cd1_trm <apply IH to _ H3.

Subgoal 2: Variables: L K J S2 S1 IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* H4 : {L, trm n1 |- trm (S1 n1)} ============================ {L |- trm (abs S1)} Subgoal 3 is: {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} cd1_trm <search.

Subgoal 3: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J |- cd1 (abs T1) (abs T2)}* H4 : {J |- cd1 S1 S2}* ============================ {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} cd1_trm <apply IH to H1 H3.

Subgoal 3: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J |- cd1 (abs T1) (abs T2)}* H4 : {J |- cd1 S1 S2}* H5 : {L |- trm (abs T1)} ============================ {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} cd1_trm <apply IH to H1 H4.

Subgoal 3: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J |- cd1 (abs T1) (abs T2)}* H4 : {J |- cd1 S1 S2}* H5 : {L |- trm (abs T1)} H6 : {L |- trm S1} ============================ {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} cd1_trm <search.

Subgoal 4: Variables: A B L K J F IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J, [F] |- cd1 A B}* H4 : member F J ============================ {L |- trm A} cd1_trm <apply cd_worlds to H1 H4.

Subgoal 4: Variables: A B L K J F IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J, [F] |- cd1 A B}* H4 : member F J H5 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, F = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) ============================ {L |- trm A} cd1_trm <case H5.

Subgoal 4.1: Variables: A B L K J B1 IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J, [cd1 B1 B1] |- cd1 A B}* H4 : member (cd1 B1 B1) J H6 : name B1 H7 : member (trm B1) L H8 : member (pr1 B1 B1) K H9 : member (notabs B1) J ============================ {L |- trm A} Subgoal 4.2 is: {L |- trm A} cd1_trm <case H3.

Subgoal 4.1: Variables: B L K J IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H4 : member (cd1 B B) J H6 : name B H7 : member (trm B) L H8 : member (pr1 B B) K H9 : member (notabs B) J ============================ {L |- trm B} Subgoal 4.2 is: {L |- trm A} cd1_trm <search.

Subgoal 4.2: Variables: A B L K J A1 IH : forall A B L K J, ctxs L K J -> {J |- cd1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {J, [notabs A1] |- cd1 A B}* H4 : member (notabs A1) J H6 : name A1 H7 : member (trm A1) L H8 : member (pr1 A1 A1) K H9 : member (cd1 A1 A1) J ============================ {L |- trm A} cd1_trm <case H3.Proof completed.

Abella <Theorem pr1_trm : forall A B L K J, ctxs L K J -> {K |- pr1 A B} -> {L |- trm A}.

============================ forall A B L K J, ctxs L K J -> {K |- pr1 A B} -> {L |- trm A} pr1_trm <induction on 2.

IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} ============================ forall A B L K J, ctxs L K J -> {K |- pr1 A B}@ -> {L |- trm A} pr1_trm <intros.

Variables: A B L K J IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H2 : {K |- pr1 A B}@ ============================ {L |- trm A} pr1_trm <case H2.

Subgoal 1: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {K |- pr1 T1 T2}* H4 : {K |- pr1 S1 S2}* ============================ {L |- trm (app T1 S1)} Subgoal 2 is: {L |- trm (abs S1)} Subgoal 3 is: {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} pr1_trm <apply IH to H1 H3.

Subgoal 1: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {K |- pr1 T1 T2}* H4 : {K |- pr1 S1 S2}* H5 : {L |- trm T1} ============================ {L |- trm (app T1 S1)} Subgoal 2 is: {L |- trm (abs S1)} Subgoal 3 is: {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} pr1_trm <apply IH to H1 H4.

Subgoal 1: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {K |- pr1 T1 T2}* H4 : {K |- pr1 S1 S2}* H5 : {L |- trm T1} H6 : {L |- trm S1} ============================ {L |- trm (app T1 S1)} Subgoal 2 is: {L |- trm (abs S1)} Subgoal 3 is: {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} pr1_trm <search.

Subgoal 2: Variables: L K J S2 S1 IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}* ============================ {L |- trm (abs S1)} Subgoal 3 is: {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} pr1_trm <apply IH to _ H3.

Subgoal 2: Variables: L K J S2 S1 IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}* H4 : {L, trm n1 |- trm (S1 n1)} ============================ {L |- trm (abs S1)} Subgoal 3 is: {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} pr1_trm <search.

Subgoal 3: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {K |- pr1 (abs T1) (abs T2)}* H4 : {K |- pr1 S1 S2}* ============================ {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} pr1_trm <apply IH to H1 H3.

Subgoal 3: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {K |- pr1 (abs T1) (abs T2)}* H4 : {K |- pr1 S1 S2}* H5 : {L |- trm (abs T1)} ============================ {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} pr1_trm <apply IH to H1 H4.

Subgoal 3: Variables: L K J S2 S1 T2 T1 IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {K |- pr1 (abs T1) (abs T2)}* H4 : {K |- pr1 S1 S2}* H5 : {L |- trm (abs T1)} H6 : {L |- trm S1} ============================ {L |- trm (app (abs T1) S1)} Subgoal 4 is: {L |- trm A} pr1_trm <search.

Subgoal 4: Variables: A B L K J F IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {K, [F] |- pr1 A B}* H4 : member F K ============================ {L |- trm A} pr1_trm <apply pr1_worlds to H1 H4.

Subgoal 4: Variables: A B L K J B1 IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H3 : {K, [pr1 B1 B1] |- pr1 A B}* H4 : member (pr1 B1 B1) K H5 : name B1 H6 : member (trm B1) L H7 : member (cd1 B1 B1) J H8 : member (notabs B1) J ============================ {L |- trm A} pr1_trm <case H3.

Subgoal 4: Variables: B L K J IH : forall A B L K J, ctxs L K J -> {K |- pr1 A B}* -> {L |- trm A} H1 : ctxs L K J H4 : member (pr1 B B) K H5 : name B H6 : member (trm B) L H7 : member (cd1 B B) J H8 : member (notabs B) J ============================ {L |- trm B} pr1_trm <search.Proof completed.

Abella <Theorem pre_cd1_pr1 : forall A B L K J, ctxs L K J -> {L |- trm A} -> {J |- cd1 A B} -> {K |- pr1 A B}.

============================ forall A B L K J, ctxs L K J -> {L |- trm A} -> {J |- cd1 A B} -> {K |- pr1 A B} pre_cd1_pr1 <induction on 2.

IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} ============================ forall A B L K J, ctxs L K J -> {L |- trm A}@ -> {J |- cd1 A B} -> {K |- pr1 A B} pre_cd1_pr1 <intros.

Variables: A B L K J IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm A}@ H3 : {J |- cd1 A B} ============================ {K |- pr1 A B} pre_cd1_pr1 <case H2 (keep).

Subgoal 1: Variables: B L K J N M IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (app M N)}@ H3 : {J |- cd1 (app M N) B} H4 : {L |- trm M}* H5 : {L |- trm N}* ============================ {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <case H3.

Subgoal 1.1: Variables: L K J N M S2 T2 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (app M N)}@ H4 : {L |- trm M}* H5 : {L |- trm N}* H6 : {J |- notabs M} H7 : {J |- cd1 M T2} H8 : {J |- cd1 N S2} ============================ {K |- pr1 (app M N) (app T2 S2)} Subgoal 1.2 is: {K |- pr1 (app (abs T1) N) (T2 S2)} Subgoal 1.3 is: {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <apply IH to H1 H4 H7.

Subgoal 1.1: Variables: L K J N M S2 T2 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (app M N)}@ H4 : {L |- trm M}* H5 : {L |- trm N}* H6 : {J |- notabs M} H7 : {J |- cd1 M T2} H8 : {J |- cd1 N S2} H9 : {K |- pr1 M T2} ============================ {K |- pr1 (app M N) (app T2 S2)} Subgoal 1.2 is: {K |- pr1 (app (abs T1) N) (T2 S2)} Subgoal 1.3 is: {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <apply IH to H1 H5 H8.

Subgoal 1.1: Variables: L K J N M S2 T2 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (app M N)}@ H4 : {L |- trm M}* H5 : {L |- trm N}* H6 : {J |- notabs M} H7 : {J |- cd1 M T2} H8 : {J |- cd1 N S2} H9 : {K |- pr1 M T2} H10 : {K |- pr1 N S2} ============================ {K |- pr1 (app M N) (app T2 S2)} Subgoal 1.2 is: {K |- pr1 (app (abs T1) N) (T2 S2)} Subgoal 1.3 is: {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <search.

Subgoal 1.2: Variables: L K J N S2 T2 T1 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (app (abs T1) N)}@ H4 : {L |- trm (abs T1)}* H5 : {L |- trm N}* H6 : {J |- cd1 (abs T1) (abs T2)} H7 : {J |- cd1 N S2} ============================ {K |- pr1 (app (abs T1) N) (T2 S2)} Subgoal 1.3 is: {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <apply IH to H1 H4 H6.

Subgoal 1.2: Variables: L K J N S2 T2 T1 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (app (abs T1) N)}@ H4 : {L |- trm (abs T1)}* H5 : {L |- trm N}* H6 : {J |- cd1 (abs T1) (abs T2)} H7 : {J |- cd1 N S2} H8 : {K |- pr1 (abs T1) (abs T2)} ============================ {K |- pr1 (app (abs T1) N) (T2 S2)} Subgoal 1.3 is: {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <apply IH to H1 H5 H7.

Subgoal 1.2: Variables: L K J N S2 T2 T1 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (app (abs T1) N)}@ H4 : {L |- trm (abs T1)}* H5 : {L |- trm N}* H6 : {J |- cd1 (abs T1) (abs T2)} H7 : {J |- cd1 N S2} H8 : {K |- pr1 (abs T1) (abs T2)} H9 : {K |- pr1 N S2} ============================ {K |- pr1 (app (abs T1) N) (T2 S2)} Subgoal 1.3 is: {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <search.

Subgoal 1.3: Variables: B L K J N M F IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (app M N)}@ H4 : {L |- trm M}* H5 : {L |- trm N}* H6 : {J, [F] |- cd1 (app M N) B} H7 : member F J ============================ {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <apply cd_worlds to H1 H7.

Subgoal 1.3: Variables: B L K J N M F IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (app M N)}@ H4 : {L |- trm M}* H5 : {L |- trm N}* H6 : {J, [F] |- cd1 (app M N) B} H7 : member F J H8 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, F = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) ============================ {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <case H8.

Subgoal 1.3.1: Variables: B L K J N M B1 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (app M N)}@ H4 : {L |- trm M}* H5 : {L |- trm N}* H6 : {J, [cd1 B1 B1] |- cd1 (app M N) B} H7 : member (cd1 B1 B1) J H9 : name B1 H10 : member (trm B1) L H11 : member (pr1 B1 B1) K H12 : member (notabs B1) J ============================ {K |- pr1 (app M N) B} Subgoal 1.3.2 is: {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <case H9.

Subgoal 1.3.1: Variables: B L K J N M IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs (L n1) (K n1) (J n1) H2 : {L n1 |- trm (app (M n1) (N n1))}@ H4 : {L n1 |- trm (M n1)}* H5 : {L n1 |- trm (N n1)}* H6 : {J n1, [cd1 n1 n1] |- cd1 (app (M n1) (N n1)) (B n1)} H7 : member (cd1 n1 n1) (J n1) H10 : member (trm n1) (L n1) H11 : member (pr1 n1 n1) (K n1) H12 : member (notabs n1) (J n1) ============================ {K n1 |- pr1 (app (M n1) (N n1)) (B n1)} Subgoal 1.3.2 is: {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <case H6.

Subgoal 1.3.2: Variables: B L K J N M A1 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (app M N)}@ H4 : {L |- trm M}* H5 : {L |- trm N}* H6 : {J, [notabs A1] |- cd1 (app M N) B} H7 : member (notabs A1) J H9 : name A1 H10 : member (trm A1) L H11 : member (pr1 A1 A1) K H12 : member (cd1 A1 A1) J ============================ {K |- pr1 (app M N) B} Subgoal 2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <case H6.

Subgoal 2: Variables: B L K J R IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (abs R)}@ H3 : {J |- cd1 (abs R) B} H4 : {L, trm n1 |- trm (R n1)}* ============================ {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <case H3.

Subgoal 2.1: Variables: L K J R S2 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (abs R)}@ H4 : {L, trm n1 |- trm (R n1)}* H5 : {J, notabs n1, cd1 n1 n1 |- cd1 (R n1) (S2 n1)} ============================ {K |- pr1 (abs R) (abs S2)} Subgoal 2.2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <apply IH to _ H4 H5.

Subgoal 2.1: Variables: L K J R S2 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (abs R)}@ H4 : {L, trm n1 |- trm (R n1)}* H5 : {J, notabs n1, cd1 n1 n1 |- cd1 (R n1) (S2 n1)} H6 : {K, pr1 n1 n1 |- pr1 (R n1) (S2 n1)} ============================ {K |- pr1 (abs R) (abs S2)} Subgoal 2.2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <search.

Subgoal 2.2: Variables: B L K J R F IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (abs R)}@ H4 : {L, trm n1 |- trm (R n1)}* H5 : {J, [F] |- cd1 (abs R) B} H6 : member F J ============================ {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <apply cd_worlds to H1 H6.

Subgoal 2.2: Variables: B L K J R F IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (abs R)}@ H4 : {L, trm n1 |- trm (R n1)}* H5 : {J, [F] |- cd1 (abs R) B} H6 : member F J H7 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, F = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) ============================ {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <case H7.

Subgoal 2.2.1: Variables: B L K J R B1 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (abs R)}@ H4 : {L, trm n1 |- trm (R n1)}* H5 : {J, [cd1 B1 B1] |- cd1 (abs R) B} H6 : member (cd1 B1 B1) J H8 : name B1 H9 : member (trm B1) L H10 : member (pr1 B1 B1) K H11 : member (notabs B1) J ============================ {K |- pr1 (abs R) B} Subgoal 2.2.2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <case H8.

Subgoal 2.2.1: Variables: B L K J R IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs (L n2) (K n2) (J n2) H2 : {L n2 |- trm (abs (R n2))}@ H4 : {L n2, trm n1 |- trm (R n2 n1)}* H5 : {J n2, [cd1 n2 n2] |- cd1 (abs (R n2)) (B n2)} H6 : member (cd1 n2 n2) (J n2) H9 : member (trm n2) (L n2) H10 : member (pr1 n2 n2) (K n2) H11 : member (notabs n2) (J n2) ============================ {K n2 |- pr1 (abs (R n2)) (B n2)} Subgoal 2.2.2 is: {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <case H5.

Subgoal 2.2.2: Variables: B L K J R A1 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm (abs R)}@ H4 : {L, trm n1 |- trm (R n1)}* H5 : {J, [notabs A1] |- cd1 (abs R) B} H6 : member (notabs A1) J H8 : name A1 H9 : member (trm A1) L H10 : member (pr1 A1 A1) K H11 : member (cd1 A1 A1) J ============================ {K |- pr1 (abs R) B} Subgoal 3 is: {K |- pr1 A B} pre_cd1_pr1 <case H5.

Subgoal 3: Variables: A B L K J F IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm A}@ H3 : {J |- cd1 A B} H4 : {L, [F] |- trm A}* H5 : member F L ============================ {K |- pr1 A B} pre_cd1_pr1 <apply trm_worlds to H1 H5.

Subgoal 3: Variables: A B L K J A1 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm A}@ H3 : {J |- cd1 A B} H4 : {L, [trm A1] |- trm A}* H5 : member (trm A1) L H6 : name A1 H7 : member (pr1 A1 A1) K H8 : member (cd1 A1 A1) J H9 : member (notabs A1) J ============================ {K |- pr1 A B} pre_cd1_pr1 <case H4.

Subgoal 3: Variables: A B L K J IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs L K J H2 : {L |- trm A}@ H3 : {J |- cd1 A B} H5 : member (trm A) L H6 : name A H7 : member (pr1 A A) K H8 : member (cd1 A A) J H9 : member (notabs A) J ============================ {K |- pr1 A B} pre_cd1_pr1 <case H6.

Subgoal 3: Variables: B L K J IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs (L n1) (K n1) (J n1) H2 : {L n1 |- trm n1}@ H3 : {J n1 |- cd1 n1 (B n1)} H5 : member (trm n1) (L n1) H7 : member (pr1 n1 n1) (K n1) H8 : member (cd1 n1 n1) (J n1) H9 : member (notabs n1) (J n1) ============================ {K n1 |- pr1 n1 (B n1)} pre_cd1_pr1 <case H3.

Subgoal 3: Variables: B L K J F1 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs (L n1) (K n1) (J n1) H2 : {L n1 |- trm n1}@ H5 : member (trm n1) (L n1) H7 : member (pr1 n1 n1) (K n1) H8 : member (cd1 n1 n1) (J n1) H9 : member (notabs n1) (J n1) H10 : {J n1, [F1 n1] |- cd1 n1 (B n1)} H11 : member (F1 n1) (J n1) ============================ {K n1 |- pr1 n1 (B n1)} pre_cd1_pr1 <apply cd_worlds to H1 H11.

Subgoal 3: Variables: B L K J F1 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs (L n1) (K n1) (J n1) H2 : {L n1 |- trm n1}@ H5 : member (trm n1) (L n1) H7 : member (pr1 n1 n1) (K n1) H8 : member (cd1 n1 n1) (J n1) H9 : member (notabs n1) (J n1) H10 : {J n1, [F1 n1] |- cd1 n1 (B n1)} H11 : member (F1 n1) (J n1) H12 : (exists A B, F1 n1 = cd1 A B /\ name A /\ A = B /\ member (trm A) (L n1) /\ member (pr1 A A) (K n1) /\ member (notabs A) (J n1)) \/ (exists A, F1 n1 = notabs A /\ name A /\ member (trm A) (L n1) /\ member (pr1 A A) (K n1) /\ member (cd1 A A) (J n1)) ============================ {K n1 |- pr1 n1 (B n1)} pre_cd1_pr1 <case H12.

Subgoal 3.1: Variables: B L K J B1 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs (L n1) (K n1) (J n1) H2 : {L n1 |- trm n1}@ H5 : member (trm n1) (L n1) H7 : member (pr1 n1 n1) (K n1) H8 : member (cd1 n1 n1) (J n1) H9 : member (notabs n1) (J n1) H10 : {J n1, [cd1 (B1 n1) (B1 n1)] |- cd1 n1 (B n1)} H11 : member (cd1 (B1 n1) (B1 n1)) (J n1) H13 : name (B1 n1) H14 : member (trm (B1 n1)) (L n1) H15 : member (pr1 (B1 n1) (B1 n1)) (K n1) H16 : member (notabs (B1 n1)) (J n1) ============================ {K n1 |- pr1 n1 (B n1)} Subgoal 3.2 is: {K n1 |- pr1 n1 (B n1)} pre_cd1_pr1 <case H10.

Subgoal 3.1: Variables: L K J IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs (L n1) (K n1) (J n1) H2 : {L n1 |- trm n1}@ H5 : member (trm n1) (L n1) H7 : member (pr1 n1 n1) (K n1) H8 : member (cd1 n1 n1) (J n1) H9 : member (notabs n1) (J n1) H11 : member (cd1 n1 n1) (J n1) H13 : name n1 H14 : member (trm n1) (L n1) H15 : member (pr1 n1 n1) (K n1) H16 : member (notabs n1) (J n1) ============================ {K n1 |- pr1 n1 n1} Subgoal 3.2 is: {K n1 |- pr1 n1 (B n1)} pre_cd1_pr1 <search.

Subgoal 3.2: Variables: B L K J A2 IH : forall A B L K J, ctxs L K J -> {L |- trm A}* -> {J |- cd1 A B} -> {K |- pr1 A B} H1 : ctxs (L n1) (K n1) (J n1) H2 : {L n1 |- trm n1}@ H5 : member (trm n1) (L n1) H7 : member (pr1 n1 n1) (K n1) H8 : member (cd1 n1 n1) (J n1) H9 : member (notabs n1) (J n1) H10 : {J n1, [notabs (A2 n1)] |- cd1 n1 (B n1)} H11 : member (notabs (A2 n1)) (J n1) H13 : name (A2 n1) H14 : member (trm (A2 n1)) (L n1) H15 : member (pr1 (A2 n1) (A2 n1)) (K n1) H16 : member (cd1 (A2 n1) (A2 n1)) (J n1) ============================ {K n1 |- pr1 n1 (B n1)} pre_cd1_pr1 <case H10.Proof completed.

Abella <Theorem cd1_pr1 : forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {K |- pr1 A B}.

============================ forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {K |- pr1 A B} cd1_pr1 <intros.

Variables: A B L K J H1 : ctxs L K J H2 : {J |- cd1 A B} ============================ {K |- pr1 A B} cd1_pr1 <apply cd1_trm to H1 H2.

Variables: A B L K J H1 : ctxs L K J H2 : {J |- cd1 A B} H3 : {L |- trm A} ============================ {K |- pr1 A B} cd1_pr1 <apply pre_cd1_pr1 to H1 H3 H2.

Variables: A B L K J H1 : ctxs L K J H2 : {J |- cd1 A B} H3 : {L |- trm A} H4 : {K |- pr1 A B} ============================ {K |- pr1 A B} cd1_pr1 <search.Proof completed.

Abella <Theorem pr1_rfl : forall A L K J, ctxs L K J -> {L |- trm A} -> {K |- pr1 A A}.

============================ forall A L K J, ctxs L K J -> {L |- trm A} -> {K |- pr1 A A} pr1_rfl <induction on 2.

IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A} ============================ forall A L K J, ctxs L K J -> {L |- trm A}@ -> {K |- pr1 A A} pr1_rfl <intros.

Variables: A L K J IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A} H1 : ctxs L K J H2 : {L |- trm A}@ ============================ {K |- pr1 A A} pr1_rfl <case H2.

Subgoal 1: Variables: L K J N M IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A} H1 : ctxs L K J H3 : {L |- trm M}* H4 : {L |- trm N}* ============================ {K |- pr1 (app M N) (app M N)} Subgoal 2 is: {K |- pr1 (abs R) (abs R)} Subgoal 3 is: {K |- pr1 A A} pr1_rfl <apply IH to H1 H3.

Subgoal 1: Variables: L K J N M IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A} H1 : ctxs L K J H3 : {L |- trm M}* H4 : {L |- trm N}* H5 : {K |- pr1 M M} ============================ {K |- pr1 (app M N) (app M N)} Subgoal 2 is: {K |- pr1 (abs R) (abs R)} Subgoal 3 is: {K |- pr1 A A} pr1_rfl <apply IH to H1 H4.

Subgoal 1: Variables: L K J N M IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A} H1 : ctxs L K J H3 : {L |- trm M}* H4 : {L |- trm N}* H5 : {K |- pr1 M M} H6 : {K |- pr1 N N} ============================ {K |- pr1 (app M N) (app M N)} Subgoal 2 is: {K |- pr1 (abs R) (abs R)} Subgoal 3 is: {K |- pr1 A A} pr1_rfl <search.

Subgoal 2: Variables: L K J R IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A} H1 : ctxs L K J H3 : {L, trm n1 |- trm (R n1)}* ============================ {K |- pr1 (abs R) (abs R)} Subgoal 3 is: {K |- pr1 A A} pr1_rfl <apply IH to _ H3.

Subgoal 2: Variables: L K J R IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A} H1 : ctxs L K J H3 : {L, trm n1 |- trm (R n1)}* H4 : {K, pr1 n1 n1 |- pr1 (R n1) (R n1)} ============================ {K |- pr1 (abs R) (abs R)} Subgoal 3 is: {K |- pr1 A A} pr1_rfl <search.

Subgoal 3: Variables: A L K J F IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A} H1 : ctxs L K J H3 : {L, [F] |- trm A}* H4 : member F L ============================ {K |- pr1 A A} pr1_rfl <apply trm_worlds to H1 H4.

Subgoal 3: Variables: A L K J A1 IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A} H1 : ctxs L K J H3 : {L, [trm A1] |- trm A}* H4 : member (trm A1) L H5 : name A1 H6 : member (pr1 A1 A1) K H7 : member (cd1 A1 A1) J H8 : member (notabs A1) J ============================ {K |- pr1 A A} pr1_rfl <case H5.

Subgoal 3: Variables: A L K J IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A} H1 : ctxs (L n1) (K n1) (J n1) H3 : {L n1, [trm n1] |- trm (A n1)}* H4 : member (trm n1) (L n1) H6 : member (pr1 n1 n1) (K n1) H7 : member (cd1 n1 n1) (J n1) H8 : member (notabs n1) (J n1) ============================ {K n1 |- pr1 (A n1) (A n1)} pr1_rfl <case H3.

Subgoal 3: Variables: L K J IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> {K |- pr1 A A} H1 : ctxs (L n1) (K n1) (J n1) H4 : member (trm n1) (L n1) H6 : member (pr1 n1 n1) (K n1) H7 : member (cd1 n1 n1) (J n1) H8 : member (notabs n1) (J n1) ============================ {K n1 |- pr1 n1 n1} pr1_rfl <search.Proof completed.

Abella <Theorem cd1_unique : forall A B C L K J, ctxs L K J -> {J |- cd1 A B} -> {J |- cd1 A C} -> B = C.

============================ forall A B C L K J, ctxs L K J -> {J |- cd1 A B} -> {J |- cd1 A C} -> B = C cd1_unique <induction on 2.

IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C ============================ forall A B C L K J, ctxs L K J -> {J |- cd1 A B}@ -> {J |- cd1 A C} -> B = C cd1_unique <intros.

Variables: A B C L K J IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H2 : {J |- cd1 A B}@ H3 : {J |- cd1 A C} ============================ B = C cd1_unique <case H2.

Subgoal 1: Variables: C L K J S2 S1 T2 T1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H3 : {J |- cd1 (app T1 S1) C} H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* ============================ app T2 S2 = C Subgoal 2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H3.

Subgoal 1.1: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* H7 : {J |- notabs T1} H8 : {J |- cd1 T1 T3} H9 : {J |- cd1 S1 S3} ============================ app T2 S2 = app T3 S3 Subgoal 1.2 is: app T2 S2 = T3 S3 Subgoal 1.3 is: app T2 S2 = C Subgoal 2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <apply IH to H1 H5 H8.

Subgoal 1.1: Variables: L K J S2 S1 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T3}* H6 : {J |- cd1 S1 S2}* H7 : {J |- notabs T1} H8 : {J |- cd1 T1 T3} H9 : {J |- cd1 S1 S3} ============================ app T3 S2 = app T3 S3 Subgoal 1.2 is: app T2 S2 = T3 S3 Subgoal 1.3 is: app T2 S2 = C Subgoal 2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <apply IH to H1 H6 H9.

Subgoal 1.1: Variables: L K J S1 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T3}* H6 : {J |- cd1 S1 S3}* H7 : {J |- notabs T1} H8 : {J |- cd1 T1 T3} H9 : {J |- cd1 S1 S3} ============================ app T3 S3 = app T3 S3 Subgoal 1.2 is: app T2 S2 = T3 S3 Subgoal 1.3 is: app T2 S2 = C Subgoal 2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <search.

Subgoal 1.2: Variables: L K J S2 S1 T2 S3 T3 T4 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- notabs (abs T4)}* H5 : {J |- cd1 (abs T4) T2}* H6 : {J |- cd1 S1 S2}* H7 : {J |- cd1 (abs T4) (abs T3)} H8 : {J |- cd1 S1 S3} ============================ app T2 S2 = T3 S3 Subgoal 1.3 is: app T2 S2 = C Subgoal 2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <apply notabs_abs_absurd to H1 H4.

Subgoal 1.3: Variables: C L K J S2 S1 T2 T1 F IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* H7 : {J, [F] |- cd1 (app T1 S1) C} H8 : member F J ============================ app T2 S2 = C Subgoal 2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <apply cd_worlds to H1 H8.

Subgoal 1.3: Variables: C L K J S2 S1 T2 T1 F IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* H7 : {J, [F] |- cd1 (app T1 S1) C} H8 : member F J H9 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, F = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) ============================ app T2 S2 = C Subgoal 2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H9.

Subgoal 1.3.1: Variables: C L K J S2 S1 T2 T1 B1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* H7 : {J, [cd1 B1 B1] |- cd1 (app T1 S1) C} H8 : member (cd1 B1 B1) J H10 : name B1 H11 : member (trm B1) L H12 : member (pr1 B1 B1) K H13 : member (notabs B1) J ============================ app T2 S2 = C Subgoal 1.3.2 is: app T2 S2 = C Subgoal 2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H10.

Subgoal 1.3.1: Variables: C L K J S2 S1 T2 T1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs (L n1) (K n1) (J n1) H4 : {J n1 |- notabs (T1 n1)}* H5 : {J n1 |- cd1 (T1 n1) (T2 n1)}* H6 : {J n1 |- cd1 (S1 n1) (S2 n1)}* H7 : {J n1, [cd1 n1 n1] |- cd1 (app (T1 n1) (S1 n1)) (C n1)} H8 : member (cd1 n1 n1) (J n1) H11 : member (trm n1) (L n1) H12 : member (pr1 n1 n1) (K n1) H13 : member (notabs n1) (J n1) ============================ app (T2 n1) (S2 n1) = C n1 Subgoal 1.3.2 is: app T2 S2 = C Subgoal 2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H7.

Subgoal 1.3.2: Variables: C L K J S2 S1 T2 T1 A1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* H7 : {J, [notabs A1] |- cd1 (app T1 S1) C} H8 : member (notabs A1) J H10 : name A1 H11 : member (trm A1) L H12 : member (pr1 A1 A1) K H13 : member (cd1 A1 A1) J ============================ app T2 S2 = C Subgoal 2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H10.

Subgoal 1.3.2: Variables: C L K J S2 S1 T2 T1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs (L n1) (K n1) (J n1) H4 : {J n1 |- notabs (T1 n1)}* H5 : {J n1 |- cd1 (T1 n1) (T2 n1)}* H6 : {J n1 |- cd1 (S1 n1) (S2 n1)}* H7 : {J n1, [notabs n1] |- cd1 (app (T1 n1) (S1 n1)) (C n1)} H8 : member (notabs n1) (J n1) H11 : member (trm n1) (L n1) H12 : member (pr1 n1 n1) (K n1) H13 : member (cd1 n1 n1) (J n1) ============================ app (T2 n1) (S2 n1) = C n1 Subgoal 2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H7.

Subgoal 2: Variables: C L K J S2 S1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H3 : {J |- cd1 (abs S1) C} H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* ============================ abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H3.

Subgoal 2.1: Variables: L K J S2 S1 S3 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* H5 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S3 n1)} ============================ abs S2 = abs S3 Subgoal 2.2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <apply IH to _ H4 H5.

Subgoal 2.1: Variables: L K J S1 S3 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S3 n1)}* H5 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S3 n1)} ============================ abs (z1\S3 z1) = abs S3 Subgoal 2.2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <search.

Subgoal 2.2: Variables: C L K J S2 S1 F IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* H5 : {J, [F] |- cd1 (abs S1) C} H6 : member F J ============================ abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <apply cd_worlds to H1 H6.

Subgoal 2.2: Variables: C L K J S2 S1 F IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* H5 : {J, [F] |- cd1 (abs S1) C} H6 : member F J H7 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, F = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) ============================ abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H7.

Subgoal 2.2.1: Variables: C L K J S2 S1 B1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* H5 : {J, [cd1 B1 B1] |- cd1 (abs S1) C} H6 : member (cd1 B1 B1) J H8 : name B1 H9 : member (trm B1) L H10 : member (pr1 B1 B1) K H11 : member (notabs B1) J ============================ abs S2 = C Subgoal 2.2.2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H8.

Subgoal 2.2.1: Variables: C L K J S2 S1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs (L n2) (K n2) (J n2) H4 : {J n2, notabs n1, cd1 n1 n1 |- cd1 (S1 n2 n1) (S2 n2 n1)}* H5 : {J n2, [cd1 n2 n2] |- cd1 (abs (S1 n2)) (C n2)} H6 : member (cd1 n2 n2) (J n2) H9 : member (trm n2) (L n2) H10 : member (pr1 n2 n2) (K n2) H11 : member (notabs n2) (J n2) ============================ abs (S2 n2) = C n2 Subgoal 2.2.2 is: abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H5.

Subgoal 2.2.2: Variables: C L K J S2 S1 A1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* H5 : {J, [notabs A1] |- cd1 (abs S1) C} H6 : member (notabs A1) J H8 : name A1 H9 : member (trm A1) L H10 : member (pr1 A1 A1) K H11 : member (cd1 A1 A1) J ============================ abs S2 = C Subgoal 3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H5.

Subgoal 3: Variables: C L K J S2 S1 T2 T1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H3 : {J |- cd1 (app (abs T1) S1) C} H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* ============================ T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H3.

Subgoal 3.1: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {J |- notabs (abs T1)} H7 : {J |- cd1 (abs T1) T3} H8 : {J |- cd1 S1 S3} ============================ T2 S2 = app T3 S3 Subgoal 3.2 is: T2 S2 = T3 S3 Subgoal 3.3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <apply notabs_abs_absurd to H1 H6.

Subgoal 3.2: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {J |- cd1 (abs T1) (abs T3)} H7 : {J |- cd1 S1 S3} ============================ T2 S2 = T3 S3 Subgoal 3.3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <apply IH to H1 H4 H6.

Subgoal 3.2: Variables: L K J S2 S1 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T3)}* H5 : {J |- cd1 S1 S2}* H6 : {J |- cd1 (abs T1) (abs T3)} H7 : {J |- cd1 S1 S3} ============================ T3 S2 = T3 S3 Subgoal 3.3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <apply IH to H1 H5 H7.

Subgoal 3.2: Variables: L K J S1 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T3)}* H5 : {J |- cd1 S1 S3}* H6 : {J |- cd1 (abs T1) (abs T3)} H7 : {J |- cd1 S1 S3} ============================ T3 S3 = T3 S3 Subgoal 3.3 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <search.

Subgoal 3.3: Variables: C L K J S2 S1 T2 T1 F IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {J, [F] |- cd1 (app (abs T1) S1) C} H7 : member F J ============================ T2 S2 = C Subgoal 4 is: B = C cd1_unique <apply cd_worlds to H1 H7.

Subgoal 3.3: Variables: C L K J S2 S1 T2 T1 F IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {J, [F] |- cd1 (app (abs T1) S1) C} H7 : member F J H8 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, F = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) ============================ T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H8.

Subgoal 3.3.1: Variables: C L K J S2 S1 T2 T1 B1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {J, [cd1 B1 B1] |- cd1 (app (abs T1) S1) C} H7 : member (cd1 B1 B1) J H9 : name B1 H10 : member (trm B1) L H11 : member (pr1 B1 B1) K H12 : member (notabs B1) J ============================ T2 S2 = C Subgoal 3.3.2 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H9.

Subgoal 3.3.1: Variables: C L K J S2 S1 T2 T1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs (L n1) (K n1) (J n1) H4 : {J n1 |- cd1 (abs (T1 n1)) (abs (T2 n1))}* H5 : {J n1 |- cd1 (S1 n1) (S2 n1)}* H6 : {J n1, [cd1 n1 n1] |- cd1 (app (abs (T1 n1)) (S1 n1)) (C n1)} H7 : member (cd1 n1 n1) (J n1) H10 : member (trm n1) (L n1) H11 : member (pr1 n1 n1) (K n1) H12 : member (notabs n1) (J n1) ============================ T2 n1 (S2 n1) = C n1 Subgoal 3.3.2 is: T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H6.

Subgoal 3.3.2: Variables: C L K J S2 S1 T2 T1 A1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {J, [notabs A1] |- cd1 (app (abs T1) S1) C} H7 : member (notabs A1) J H9 : name A1 H10 : member (trm A1) L H11 : member (pr1 A1 A1) K H12 : member (cd1 A1 A1) J ============================ T2 S2 = C Subgoal 4 is: B = C cd1_unique <case H6.

Subgoal 4: Variables: A B C L K J F IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H3 : {J |- cd1 A C} H4 : {J, [F] |- cd1 A B}* H5 : member F J ============================ B = C cd1_unique <apply cd_worlds to H1 H5.

Subgoal 4: Variables: A B C L K J F IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H3 : {J |- cd1 A C} H4 : {J, [F] |- cd1 A B}* H5 : member F J H6 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, F = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) ============================ B = C cd1_unique <case H6.

Subgoal 4.1: Variables: A B C L K J B1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H3 : {J |- cd1 A C} H4 : {J, [cd1 B1 B1] |- cd1 A B}* H5 : member (cd1 B1 B1) J H7 : name B1 H8 : member (trm B1) L H9 : member (pr1 B1 B1) K H10 : member (notabs B1) J ============================ B = C Subgoal 4.2 is: B = C cd1_unique <case H7.

Subgoal 4.1: Variables: A B C L K J IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs (L n1) (K n1) (J n1) H3 : {J n1 |- cd1 (A n1) (C n1)} H4 : {J n1, [cd1 n1 n1] |- cd1 (A n1) (B n1)}* H5 : member (cd1 n1 n1) (J n1) H8 : member (trm n1) (L n1) H9 : member (pr1 n1 n1) (K n1) H10 : member (notabs n1) (J n1) ============================ B n1 = C n1 Subgoal 4.2 is: B = C cd1_unique <case H4.

Subgoal 4.1: Variables: C L K J IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs (L n1) (K n1) (J n1) H3 : {J n1 |- cd1 n1 (C n1)} H5 : member (cd1 n1 n1) (J n1) H8 : member (trm n1) (L n1) H9 : member (pr1 n1 n1) (K n1) H10 : member (notabs n1) (J n1) ============================ n1 = C n1 Subgoal 4.2 is: B = C cd1_unique <case H3.

Subgoal 4.1: Variables: C L K J F1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs (L n1) (K n1) (J n1) H5 : member (cd1 n1 n1) (J n1) H8 : member (trm n1) (L n1) H9 : member (pr1 n1 n1) (K n1) H10 : member (notabs n1) (J n1) H11 : {J n1, [F1 n1] |- cd1 n1 (C n1)} H12 : member (F1 n1) (J n1) ============================ n1 = C n1 Subgoal 4.2 is: B = C cd1_unique <apply cd_worlds to H1 H12.

Subgoal 4.1: Variables: C L K J F1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs (L n1) (K n1) (J n1) H5 : member (cd1 n1 n1) (J n1) H8 : member (trm n1) (L n1) H9 : member (pr1 n1 n1) (K n1) H10 : member (notabs n1) (J n1) H11 : {J n1, [F1 n1] |- cd1 n1 (C n1)} H12 : member (F1 n1) (J n1) H13 : (exists A B, F1 n1 = cd1 A B /\ name A /\ A = B /\ member (trm A) (L n1) /\ member (pr1 A A) (K n1) /\ member (notabs A) (J n1)) \/ (exists A, F1 n1 = notabs A /\ name A /\ member (trm A) (L n1) /\ member (pr1 A A) (K n1) /\ member (cd1 A A) (J n1)) ============================ n1 = C n1 Subgoal 4.2 is: B = C cd1_unique <case H13.

Subgoal 4.1.1: Variables: C L K J B2 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs (L n1) (K n1) (J n1) H5 : member (cd1 n1 n1) (J n1) H8 : member (trm n1) (L n1) H9 : member (pr1 n1 n1) (K n1) H10 : member (notabs n1) (J n1) H11 : {J n1, [cd1 (B2 n1) (B2 n1)] |- cd1 n1 (C n1)} H12 : member (cd1 (B2 n1) (B2 n1)) (J n1) H14 : name (B2 n1) H15 : member (trm (B2 n1)) (L n1) H16 : member (pr1 (B2 n1) (B2 n1)) (K n1) H17 : member (notabs (B2 n1)) (J n1) ============================ n1 = C n1 Subgoal 4.1.2 is: n1 = C n1 Subgoal 4.2 is: B = C cd1_unique <case H11.

Subgoal 4.1.1: Variables: L K J IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs (L n1) (K n1) (J n1) H5 : member (cd1 n1 n1) (J n1) H8 : member (trm n1) (L n1) H9 : member (pr1 n1 n1) (K n1) H10 : member (notabs n1) (J n1) H12 : member (cd1 n1 n1) (J n1) H14 : name n1 H15 : member (trm n1) (L n1) H16 : member (pr1 n1 n1) (K n1) H17 : member (notabs n1) (J n1) ============================ n1 = n1 Subgoal 4.1.2 is: n1 = C n1 Subgoal 4.2 is: B = C cd1_unique <search.

Subgoal 4.1.2: Variables: C L K J A2 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs (L n1) (K n1) (J n1) H5 : member (cd1 n1 n1) (J n1) H8 : member (trm n1) (L n1) H9 : member (pr1 n1 n1) (K n1) H10 : member (notabs n1) (J n1) H11 : {J n1, [notabs (A2 n1)] |- cd1 n1 (C n1)} H12 : member (notabs (A2 n1)) (J n1) H14 : name (A2 n1) H15 : member (trm (A2 n1)) (L n1) H16 : member (pr1 (A2 n1) (A2 n1)) (K n1) H17 : member (cd1 (A2 n1) (A2 n1)) (J n1) ============================ n1 = C n1 Subgoal 4.2 is: B = C cd1_unique <case H11.

Subgoal 4.2: Variables: A B C L K J A1 IH : forall A B C L K J, ctxs L K J -> {J |- cd1 A B}* -> {J |- cd1 A C} -> B = C H1 : ctxs L K J H3 : {J |- cd1 A C} H4 : {J, [notabs A1] |- cd1 A B}* H5 : member (notabs A1) J H7 : name A1 H8 : member (trm A1) L H9 : member (pr1 A1 A1) K H10 : member (cd1 A1 A1) J ============================ B = C cd1_unique <case H4.Proof completed.

Abella <Theorem cd1_exists : forall A L K J, ctxs L K J -> {L |- trm A} -> (exists B, {J |- cd1 A B}).

============================ forall A L K J, ctxs L K J -> {L |- trm A} -> (exists B, {J |- cd1 A B}) cd1_exists <induction on 2.

IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) ============================ forall A L K J, ctxs L K J -> {L |- trm A}@ -> (exists B, {J |- cd1 A B}) cd1_exists <intros.

Variables: A L K J IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H2 : {L |- trm A}@ ============================ exists B, {J |- cd1 A B} cd1_exists <case H2.

Subgoal 1: Variables: L K J N M IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H3 : {L |- trm M}* H4 : {L |- trm N}* ============================ exists B, {J |- cd1 (app M N) B} Subgoal 2 is: exists B, {J |- cd1 (abs R) B} Subgoal 3 is: exists B, {J |- cd1 A B} cd1_exists <apply IH to H1 H3.

Subgoal 1: Variables: L K J N M B IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H3 : {L |- trm M}* H4 : {L |- trm N}* H5 : {J |- cd1 M B} ============================ exists B, {J |- cd1 (app M N) B} Subgoal 2 is: exists B, {J |- cd1 (abs R) B} Subgoal 3 is: exists B, {J |- cd1 A B} cd1_exists <apply IH to H1 H4.

Subgoal 1: Variables: L K J N M B B1 IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H3 : {L |- trm M}* H4 : {L |- trm N}* H5 : {J |- cd1 M B} H6 : {J |- cd1 N B1} ============================ exists B, {J |- cd1 (app M N) B} Subgoal 2 is: exists B, {J |- cd1 (abs R) B} Subgoal 3 is: exists B, {J |- cd1 A B} cd1_exists <case H3.

Subgoal 1.1: Variables: L K J N B B1 N1 M1 IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H4 : {L |- trm N}* H5 : {J |- cd1 (app M1 N1) B} H6 : {J |- cd1 N B1} H7 : {L |- trm M1}* H8 : {L |- trm N1}* ============================ exists B, {J |- cd1 (app (app M1 N1) N) B} Subgoal 1.2 is: exists B, {J |- cd1 (app (abs R) N) B} Subgoal 1.3 is: exists B, {J |- cd1 (app M N) B} Subgoal 2 is: exists B, {J |- cd1 (abs R) B} Subgoal 3 is: exists B, {J |- cd1 A B} cd1_exists <search.

Subgoal 1.2: Variables: L K J N B B1 R IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H4 : {L |- trm N}* H5 : {J |- cd1 (abs R) B} H6 : {J |- cd1 N B1} H7 : {L, trm n1 |- trm (R n1)}* ============================ exists B, {J |- cd1 (app (abs R) N) B} Subgoal 1.3 is: exists B, {J |- cd1 (app M N) B} Subgoal 2 is: exists B, {J |- cd1 (abs R) B} Subgoal 3 is: exists B, {J |- cd1 A B} cd1_exists <apply IH to _ H7.

Subgoal 1.2: Variables: L K J N B B1 R B2 IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H4 : {L |- trm N}* H5 : {J |- cd1 (abs R) B} H6 : {J |- cd1 N B1} H7 : {L, trm n1 |- trm (R n1)}* H8 : {J, notabs n1, cd1 n1 n1 |- cd1 (R n1) (B2 n1)} ============================ exists B, {J |- cd1 (app (abs R) N) B} Subgoal 1.3 is: exists B, {J |- cd1 (app M N) B} Subgoal 2 is: exists B, {J |- cd1 (abs R) B} Subgoal 3 is: exists B, {J |- cd1 A B} cd1_exists <search.

Subgoal 1.3: Variables: L K J N M B B1 F IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H4 : {L |- trm N}* H5 : {J |- cd1 M B} H6 : {J |- cd1 N B1} H7 : {L, [F] |- trm M}* H8 : member F L ============================ exists B, {J |- cd1 (app M N) B} Subgoal 2 is: exists B, {J |- cd1 (abs R) B} Subgoal 3 is: exists B, {J |- cd1 A B} cd1_exists <apply trm_worlds to H1 H8.

Subgoal 1.3: Variables: L K J N M B B1 A1 IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H4 : {L |- trm N}* H5 : {J |- cd1 M B} H6 : {J |- cd1 N B1} H7 : {L, [trm A1] |- trm M}* H8 : member (trm A1) L H9 : name A1 H10 : member (pr1 A1 A1) K H11 : member (cd1 A1 A1) J H12 : member (notabs A1) J ============================ exists B, {J |- cd1 (app M N) B} Subgoal 2 is: exists B, {J |- cd1 (abs R) B} Subgoal 3 is: exists B, {J |- cd1 A B} cd1_exists <case H7.

Subgoal 1.3: Variables: L K J N M B B1 IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H4 : {L |- trm N}* H5 : {J |- cd1 M B} H6 : {J |- cd1 N B1} H8 : member (trm M) L H9 : name M H10 : member (pr1 M M) K H11 : member (cd1 M M) J H12 : member (notabs M) J ============================ exists B, {J |- cd1 (app M N) B} Subgoal 2 is: exists B, {J |- cd1 (abs R) B} Subgoal 3 is: exists B, {J |- cd1 A B} cd1_exists <search.

Subgoal 2: Variables: L K J R IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H3 : {L, trm n1 |- trm (R n1)}* ============================ exists B, {J |- cd1 (abs R) B} Subgoal 3 is: exists B, {J |- cd1 A B} cd1_exists <apply IH to _ H3.

Subgoal 2: Variables: L K J R B IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H3 : {L, trm n1 |- trm (R n1)}* H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (R n1) (B n1)} ============================ exists B, {J |- cd1 (abs R) B} Subgoal 3 is: exists B, {J |- cd1 A B} cd1_exists <search.

Subgoal 3: Variables: A L K J F IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H3 : {L, [F] |- trm A}* H4 : member F L ============================ exists B, {J |- cd1 A B} cd1_exists <apply trm_worlds to H1 H4.

Subgoal 3: Variables: A L K J A1 IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H3 : {L, [trm A1] |- trm A}* H4 : member (trm A1) L H5 : name A1 H6 : member (pr1 A1 A1) K H7 : member (cd1 A1 A1) J H8 : member (notabs A1) J ============================ exists B, {J |- cd1 A B} cd1_exists <case H3.

Subgoal 3: Variables: A L K J IH : forall A L K J, ctxs L K J -> {L |- trm A}* -> (exists B, {J |- cd1 A B}) H1 : ctxs L K J H4 : member (trm A) L H5 : name A H6 : member (pr1 A A) K H7 : member (cd1 A A) J H8 : member (notabs A) J ============================ exists B, {J |- cd1 A B} cd1_exists <search.Proof completed.

Abella <Theorem pr1_name : forall A B L K J, ctxs L K J -> {K |- pr1 A B} -> name A -> B = A.

============================ forall A B L K J, ctxs L K J -> {K |- pr1 A B} -> name A -> B = A pr1_name <intros.

Variables: A B L K J H1 : ctxs L K J H2 : {K |- pr1 A B} H3 : name A ============================ B = A pr1_name <case H3.

Variables: B L K J H1 : ctxs (L n1) (K n1) (J n1) H2 : {K n1 |- pr1 n1 (B n1)} ============================ B n1 = n1 pr1_name <case H2.

Variables: B L K J F H1 : ctxs (L n1) (K n1) (J n1) H4 : {K n1, [F n1] |- pr1 n1 (B n1)} H5 : member (F n1) (K n1) ============================ B n1 = n1 pr1_name <apply pr1_worlds to H1 H5.

Variables: B L K J B1 H1 : ctxs (L n1) (K n1) (J n1) H4 : {K n1, [pr1 (B1 n1) (B1 n1)] |- pr1 n1 (B n1)} H5 : member (pr1 (B1 n1) (B1 n1)) (K n1) H6 : name (B1 n1) H7 : member (trm (B1 n1)) (L n1) H8 : member (cd1 (B1 n1) (B1 n1)) (J n1) H9 : member (notabs (B1 n1)) (J n1) ============================ B n1 = n1 pr1_name <case H4.

Variables: L K J H1 : ctxs (L n1) (K n1) (J n1) H5 : member (pr1 n1 n1) (K n1) H6 : name n1 H7 : member (trm n1) (L n1) H8 : member (cd1 n1 n1) (J n1) H9 : member (notabs n1) (J n1) ============================ n1 = n1 pr1_name <search.Proof completed.

Abella <Theorem pr1_abs : forall R B L K J, ctxs L K J -> {K |- pr1 (abs R) B} -> (exists S, B = abs S).

============================ forall R B L K J, ctxs L K J -> {K |- pr1 (abs R) B} -> (exists S, B = abs S) pr1_abs <intros.

Variables: R B L K J H1 : ctxs L K J H2 : {K |- pr1 (abs R) B} ============================ exists S, B = abs S pr1_abs <case H2.

Subgoal 1: Variables: R L K J S2 H1 : ctxs L K J H3 : {K, pr1 n1 n1 |- pr1 (R n1) (S2 n1)} ============================ exists S, abs S2 = abs S Subgoal 2 is: exists S, B = abs S pr1_abs <search.

Subgoal 2: Variables: R B L K J F H1 : ctxs L K J H3 : {K, [F] |- pr1 (abs R) B} H4 : member F K ============================ exists S, B = abs S pr1_abs <apply pr1_worlds to H1 H4.

Subgoal 2: Variables: R B L K J B1 H1 : ctxs L K J H3 : {K, [pr1 B1 B1] |- pr1 (abs R) B} H4 : member (pr1 B1 B1) K H5 : name B1 H6 : member (trm B1) L H7 : member (cd1 B1 B1) J H8 : member (notabs B1) J ============================ exists S, B = abs S pr1_abs <case H5.

Subgoal 2: Variables: R B L K J H1 : ctxs (L n1) (K n1) (J n1) H3 : {K n1, [pr1 n1 n1] |- pr1 (abs (R n1)) (B n1)} H4 : member (pr1 n1 n1) (K n1) H6 : member (trm n1) (L n1) H7 : member (cd1 n1 n1) (J n1) H8 : member (notabs n1) (J n1) ============================ exists S, B n1 = abs S pr1_abs <case H3.Proof completed.

Abella <Theorem pre_pr1_subst_lem : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)} -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)}.

============================ forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)} -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <induction on 2.

IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} ============================ forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}@ -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <intros.

Variables: A1 A2 B1 B2 L K J IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H2 : {K, pr1 n1 n1 |- pr1 (A1 n1) (A2 n1)}@ H3 : {K |- pr1 B1 B2} ============================ {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <case H2.

Subgoal 1: Variables: B1 B2 L K J S2 S1 T2 T1 IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1 |- pr1 (T1 n1) (T2 n1)}* H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}* ============================ {K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))} Subgoal 2 is: {K |- pr1 (abs (S1 B1)) (abs (S2 B2))} Subgoal 3 is: {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))} Subgoal 4 is: {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <apply IH to H1 H4 H3.

Subgoal 1: Variables: B1 B2 L K J S2 S1 T2 T1 IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1 |- pr1 (T1 n1) (T2 n1)}* H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}* H6 : {K |- pr1 (T1 B1) (T2 B2)} ============================ {K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))} Subgoal 2 is: {K |- pr1 (abs (S1 B1)) (abs (S2 B2))} Subgoal 3 is: {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))} Subgoal 4 is: {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <apply IH to H1 H5 H3.

Subgoal 1: Variables: B1 B2 L K J S2 S1 T2 T1 IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1 |- pr1 (T1 n1) (T2 n1)}* H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}* H6 : {K |- pr1 (T1 B1) (T2 B2)} H7 : {K |- pr1 (S1 B1) (S2 B2)} ============================ {K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))} Subgoal 2 is: {K |- pr1 (abs (S1 B1)) (abs (S2 B2))} Subgoal 3 is: {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))} Subgoal 4 is: {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <search.

Subgoal 2: Variables: B1 B2 L K J S2 S1 IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1, pr1 n2 n2 |- pr1 (S1 n1 n2) (S2 n1 n2)}* ============================ {K |- pr1 (abs (S1 B1)) (abs (S2 B2))} Subgoal 3 is: {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))} Subgoal 4 is: {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <apply IH to _ H4 H3.

Subgoal 2: Variables: B1 B2 L K J S2 S1 IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1, pr1 n2 n2 |- pr1 (S1 n1 n2) (S2 n1 n2)}* H5 : {K, pr1 n2 n2 |- pr1 (S1 B1 n2) (S2 B2 n2)} ============================ {K |- pr1 (abs (S1 B1)) (abs (S2 B2))} Subgoal 3 is: {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))} Subgoal 4 is: {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <search.

Subgoal 3: Variables: B1 B2 L K J S2 S1 T2 T1 IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1 |- pr1 (abs (T1 n1)) (abs (T2 n1))}* H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}* ============================ {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))} Subgoal 4 is: {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <apply IH to H1 H4 H3.

Subgoal 3: Variables: B1 B2 L K J S2 S1 T2 T1 IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1 |- pr1 (abs (T1 n1)) (abs (T2 n1))}* H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}* H6 : {K |- pr1 (abs (T1 B1)) (abs (T2 B2))} ============================ {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))} Subgoal 4 is: {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <apply IH to H1 H5 H3.

Subgoal 3: Variables: B1 B2 L K J S2 S1 T2 T1 IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1 |- pr1 (abs (T1 n1)) (abs (T2 n1))}* H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S2 n1)}* H6 : {K |- pr1 (abs (T1 B1)) (abs (T2 B2))} H7 : {K |- pr1 (S1 B1) (S2 B2)} ============================ {K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))} Subgoal 4 is: {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <search.

Subgoal 4: Variables: A1 A2 B1 B2 L K J F IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1, [F n1] |- pr1 (A1 n1) (A2 n1)}* H5 : member (F n1) (pr1 n1 n1 :: K) ============================ {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <case H5.

Subgoal 4.1: Variables: A1 A2 B1 B2 L K J IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1, [pr1 n1 n1] |- pr1 (A1 n1) (A2 n1)}* ============================ {K |- pr1 (A1 B1) (A2 B2)} Subgoal 4.2 is: {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <case H4.

Subgoal 4.1: Variables: B1 B2 L K J IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} ============================ {K |- pr1 B1 B2} Subgoal 4.2 is: {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <search.

Subgoal 4.2: Variables: A1 A2 B1 B2 L K J F IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1, [F n1] |- pr1 (A1 n1) (A2 n1)}* H6 : member (F n1) K ============================ {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <apply pr1_worlds to H1 H6.

Subgoal 4.2: Variables: A1 A2 B1 B2 L K J B IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1, [pr1 (B n1) (B n1)] |- pr1 (A1 n1) (A2 n1)}* H6 : member (pr1 (B n1) (B n1)) K H7 : name (B n1) H8 : member (trm (B n1)) L H9 : member (cd1 (B n1) (B n1)) J H10 : member (notabs (B n1)) J ============================ {K |- pr1 (A1 B1) (A2 B2)} pre_pr1_subst_lem <case H4.

Subgoal 4.2: Variables: A2 B1 B2 L K J IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H6 : member (pr1 (A2 n1) (A2 n1)) K H7 : name (A2 n1) H8 : member (trm (A2 n1)) L H9 : member (cd1 (A2 n1) (A2 n1)) J H10 : member (notabs (A2 n1)) J ============================ {K |- pr1 (A2 B1) (A2 B2)} pre_pr1_subst_lem <case H7.

Subgoal 4.2.1: Variables: B1 B2 L K J IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs (L n2) (K n2) (J n2) H3 : {K n2 |- pr1 (B1 n2) (B2 n2)} H6 : member (pr1 n2 n2) (K n2) H8 : member (trm n2) (L n2) H9 : member (cd1 n2 n2) (J n2) H10 : member (notabs n2) (J n2) ============================ {K n2 |- pr1 n2 n2} Subgoal 4.2.2 is: {K |- pr1 B1 B2} pre_pr1_subst_lem <search.

Subgoal 4.2.2: Variables: B1 B2 L K J IH : forall A1 A2 B1 B2 L K J, nabla x, ctxs L K J -> {K, pr1 x x |- pr1 (A1 x) (A2 x)}* -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H6 : member (pr1 n1 n1) K H8 : member (trm n1) L H9 : member (cd1 n1 n1) J H10 : member (notabs n1) J ============================ {K |- pr1 B1 B2} pre_pr1_subst_lem <search.Proof completed.

Abella <Theorem pr1_subst_lem : forall A1 A2 B1 B2 L K J, ctxs L K J -> {K |- pr1 (abs A1) (abs A2)} -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)}.

============================ forall A1 A2 B1 B2 L K J, ctxs L K J -> {K |- pr1 (abs A1) (abs A2)} -> {K |- pr1 B1 B2} -> {K |- pr1 (A1 B1) (A2 B2)} pr1_subst_lem <intros.

Variables: A1 A2 B1 B2 L K J H1 : ctxs L K J H2 : {K |- pr1 (abs A1) (abs A2)} H3 : {K |- pr1 B1 B2} ============================ {K |- pr1 (A1 B1) (A2 B2)} pr1_subst_lem <case H2.

Subgoal 1: Variables: A1 A2 B1 B2 L K J H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1 |- pr1 (A1 n1) (A2 n1)} ============================ {K |- pr1 (A1 B1) (A2 B2)} Subgoal 2 is: {K |- pr1 (A1 B1) (A2 B2)} pr1_subst_lem <apply pre_pr1_subst_lem to H1 H4 H3.

Subgoal 1: Variables: A1 A2 B1 B2 L K J H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, pr1 n1 n1 |- pr1 (A1 n1) (A2 n1)} H5 : {K |- pr1 (A1 B1) (A2 B2)} ============================ {K |- pr1 (A1 B1) (A2 B2)} Subgoal 2 is: {K |- pr1 (A1 B1) (A2 B2)} pr1_subst_lem <search.

Subgoal 2: Variables: A1 A2 B1 B2 L K J F H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, [F] |- pr1 (abs A1) (abs A2)} H5 : member F K ============================ {K |- pr1 (A1 B1) (A2 B2)} pr1_subst_lem <apply pr1_worlds to H1 H5.

Subgoal 2: Variables: A1 A2 B1 B2 L K J B H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H4 : {K, [pr1 B B] |- pr1 (abs A1) (abs A2)} H5 : member (pr1 B B) K H6 : name B H7 : member (trm B) L H8 : member (cd1 B B) J H9 : member (notabs B) J ============================ {K |- pr1 (A1 B1) (A2 B2)} pr1_subst_lem <case H4.

Subgoal 2: Variables: A2 B1 B2 L K J H1 : ctxs L K J H3 : {K |- pr1 B1 B2} H5 : member (pr1 (abs A2) (abs A2)) K H6 : name (abs A2) H7 : member (trm (abs A2)) L H8 : member (cd1 (abs A2) (abs A2)) J H9 : member (notabs (abs A2)) J ============================ {K |- pr1 (A2 B1) (A2 B2)} pr1_subst_lem <case H6.Proof completed.

Abella <Theorem cd1_pr1_triangle : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C} -> {K |- pr1 B C}.

============================ forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C} -> {K |- pr1 B C} cd1_pr1_triangle <induction on 3.

IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} ============================ forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}@ -> {K |- pr1 B C} cd1_pr1_triangle <intros.

Variables: A B C L K J IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H2 : {K |- pr1 A B} H3 : {J |- cd1 A C}@ ============================ {K |- pr1 B C} cd1_pr1_triangle <case H3.

Subgoal 1: Variables: B L K J S2 S1 T2 T1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H2 : {K |- pr1 (app T1 S1) B} H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* ============================ {K |- pr1 B (app T2 S2)} Subgoal 2 is: {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H2.

Subgoal 1.1: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* H7 : {K |- pr1 T1 T3} H8 : {K |- pr1 S1 S3} ============================ {K |- pr1 (app T3 S3) (app T2 S2)} Subgoal 1.2 is: {K |- pr1 (T3 S3) (app T2 S2)} Subgoal 1.3 is: {K |- pr1 B (app T2 S2)} Subgoal 2 is: {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply IH to H1 H7 H5.

Subgoal 1.1: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* H7 : {K |- pr1 T1 T3} H8 : {K |- pr1 S1 S3} H9 : {K |- pr1 T3 T2} ============================ {K |- pr1 (app T3 S3) (app T2 S2)} Subgoal 1.2 is: {K |- pr1 (T3 S3) (app T2 S2)} Subgoal 1.3 is: {K |- pr1 B (app T2 S2)} Subgoal 2 is: {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply IH to H1 H8 H6.

Subgoal 1.1: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* H7 : {K |- pr1 T1 T3} H8 : {K |- pr1 S1 S3} H9 : {K |- pr1 T3 T2} H10 : {K |- pr1 S3 S2} ============================ {K |- pr1 (app T3 S3) (app T2 S2)} Subgoal 1.2 is: {K |- pr1 (T3 S3) (app T2 S2)} Subgoal 1.3 is: {K |- pr1 B (app T2 S2)} Subgoal 2 is: {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <search.

Subgoal 1.2: Variables: L K J S2 S1 T2 S3 T3 T4 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- notabs (abs T4)}* H5 : {J |- cd1 (abs T4) T2}* H6 : {J |- cd1 S1 S2}* H7 : {K |- pr1 (abs T4) (abs T3)} H8 : {K |- pr1 S1 S3} ============================ {K |- pr1 (T3 S3) (app T2 S2)} Subgoal 1.3 is: {K |- pr1 B (app T2 S2)} Subgoal 2 is: {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply notabs_abs_absurd to H1 H4.

Subgoal 1.3: Variables: B L K J S2 S1 T2 T1 F IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* H7 : {K, [F] |- pr1 (app T1 S1) B} H8 : member F K ============================ {K |- pr1 B (app T2 S2)} Subgoal 2 is: {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply pr1_worlds to H1 H8.

Subgoal 1.3: Variables: B L K J S2 S1 T2 T1 B1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- notabs T1}* H5 : {J |- cd1 T1 T2}* H6 : {J |- cd1 S1 S2}* H7 : {K, [pr1 B1 B1] |- pr1 (app T1 S1) B} H8 : member (pr1 B1 B1) K H9 : name B1 H10 : member (trm B1) L H11 : member (cd1 B1 B1) J H12 : member (notabs B1) J ============================ {K |- pr1 B (app T2 S2)} Subgoal 2 is: {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H9.

Subgoal 1.3: Variables: B L K J S2 S1 T2 T1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs (L n1) (K n1) (J n1) H4 : {J n1 |- notabs (T1 n1)}* H5 : {J n1 |- cd1 (T1 n1) (T2 n1)}* H6 : {J n1 |- cd1 (S1 n1) (S2 n1)}* H7 : {K n1, [pr1 n1 n1] |- pr1 (app (T1 n1) (S1 n1)) (B n1)} H8 : member (pr1 n1 n1) (K n1) H10 : member (trm n1) (L n1) H11 : member (cd1 n1 n1) (J n1) H12 : member (notabs n1) (J n1) ============================ {K n1 |- pr1 (B n1) (app (T2 n1) (S2 n1))} Subgoal 2 is: {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H7.

Subgoal 2: Variables: B L K J S2 S1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H2 : {K |- pr1 (abs S1) B} H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* ============================ {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H2.

Subgoal 2.1: Variables: L K J S2 S1 S3 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S3 n1)} ============================ {K |- pr1 (abs S3) (abs S2)} Subgoal 2.2 is: {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply IH to _ H5 H4.

Subgoal 2.1: Variables: L K J S2 S1 S3 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S3 n1)} H6 : {K, pr1 n1 n1 |- pr1 (S3 n1) (S2 n1)} ============================ {K |- pr1 (abs S3) (abs S2)} Subgoal 2.2 is: {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <search.

Subgoal 2.2: Variables: B L K J S2 S1 F IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* H5 : {K, [F] |- pr1 (abs S1) B} H6 : member F K ============================ {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply pr1_worlds to H1 H6.

Subgoal 2.2: Variables: B L K J S2 S1 B1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}* H5 : {K, [pr1 B1 B1] |- pr1 (abs S1) B} H6 : member (pr1 B1 B1) K H7 : name B1 H8 : member (trm B1) L H9 : member (cd1 B1 B1) J H10 : member (notabs B1) J ============================ {K |- pr1 B (abs S2)} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H7.

Subgoal 2.2: Variables: B L K J S2 S1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs (L n2) (K n2) (J n2) H4 : {J n2, notabs n1, cd1 n1 n1 |- cd1 (S1 n2 n1) (S2 n2 n1)}* H5 : {K n2, [pr1 n2 n2] |- pr1 (abs (S1 n2)) (B n2)} H6 : member (pr1 n2 n2) (K n2) H8 : member (trm n2) (L n2) H9 : member (cd1 n2 n2) (J n2) H10 : member (notabs n2) (J n2) ============================ {K n2 |- pr1 (B n2) (abs (S2 n2))} Subgoal 3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H5.

Subgoal 3: Variables: B L K J S2 S1 T2 T1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H2 : {K |- pr1 (app (abs T1) S1) B} H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* ============================ {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H2.

Subgoal 3.1: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {K |- pr1 (abs T1) T3} H7 : {K |- pr1 S1 S3} ============================ {K |- pr1 (app T3 S3) (T2 S2)} Subgoal 3.2 is: {K |- pr1 (T3 S3) (T2 S2)} Subgoal 3.3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H6.

Subgoal 3.1.1: Variables: L K J S2 S1 T2 T1 S3 S4 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H7 : {K |- pr1 S1 S3} H8 : {K, pr1 n1 n1 |- pr1 (T1 n1) (S4 n1)} ============================ {K |- pr1 (app (abs S4) S3) (T2 S2)} Subgoal 3.1.2 is: {K |- pr1 (app T3 S3) (T2 S2)} Subgoal 3.2 is: {K |- pr1 (T3 S3) (T2 S2)} Subgoal 3.3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply IH to H1 H7 H5.

Subgoal 3.1.1: Variables: L K J S2 S1 T2 T1 S3 S4 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H7 : {K |- pr1 S1 S3} H8 : {K, pr1 n1 n1 |- pr1 (T1 n1) (S4 n1)} H9 : {K |- pr1 S3 S2} ============================ {K |- pr1 (app (abs S4) S3) (T2 S2)} Subgoal 3.1.2 is: {K |- pr1 (app T3 S3) (T2 S2)} Subgoal 3.2 is: {K |- pr1 (T3 S3) (T2 S2)} Subgoal 3.3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply IH to H1 _ H4.

Subgoal 3.1.1: Variables: L K J S2 S1 T2 T1 S3 S4 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H7 : {K |- pr1 S1 S3} H8 : {K, pr1 n1 n1 |- pr1 (T1 n1) (S4 n1)} H9 : {K |- pr1 S3 S2} H10 : {K |- pr1 (abs (z1\S4 z1)) (abs T2)} ============================ {K |- pr1 (app (abs S4) S3) (T2 S2)} Subgoal 3.1.2 is: {K |- pr1 (app T3 S3) (T2 S2)} Subgoal 3.2 is: {K |- pr1 (T3 S3) (T2 S2)} Subgoal 3.3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <search.

Subgoal 3.1.2: Variables: L K J S2 S1 T2 T1 S3 T3 F IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H7 : {K |- pr1 S1 S3} H8 : {K, [F] |- pr1 (abs T1) T3} H9 : member F K ============================ {K |- pr1 (app T3 S3) (T2 S2)} Subgoal 3.2 is: {K |- pr1 (T3 S3) (T2 S2)} Subgoal 3.3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply pr1_worlds to H1 H9.

Subgoal 3.1.2: Variables: L K J S2 S1 T2 T1 S3 T3 B1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H7 : {K |- pr1 S1 S3} H8 : {K, [pr1 B1 B1] |- pr1 (abs T1) T3} H9 : member (pr1 B1 B1) K H10 : name B1 H11 : member (trm B1) L H12 : member (cd1 B1 B1) J H13 : member (notabs B1) J ============================ {K |- pr1 (app T3 S3) (T2 S2)} Subgoal 3.2 is: {K |- pr1 (T3 S3) (T2 S2)} Subgoal 3.3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H10.

Subgoal 3.1.2: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs (L n1) (K n1) (J n1) H4 : {J n1 |- cd1 (abs (T1 n1)) (abs (T2 n1))}* H5 : {J n1 |- cd1 (S1 n1) (S2 n1)}* H7 : {K n1 |- pr1 (S1 n1) (S3 n1)} H8 : {K n1, [pr1 n1 n1] |- pr1 (abs (T1 n1)) (T3 n1)} H9 : member (pr1 n1 n1) (K n1) H11 : member (trm n1) (L n1) H12 : member (cd1 n1 n1) (J n1) H13 : member (notabs n1) (J n1) ============================ {K n1 |- pr1 (app (T3 n1) (S3 n1)) (T2 n1 (S2 n1))} Subgoal 3.2 is: {K |- pr1 (T3 S3) (T2 S2)} Subgoal 3.3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H8.

Subgoal 3.2: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {K |- pr1 (abs T1) (abs T3)} H7 : {K |- pr1 S1 S3} ============================ {K |- pr1 (T3 S3) (T2 S2)} Subgoal 3.3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply IH to H1 H7 H5.

Subgoal 3.2: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {K |- pr1 (abs T1) (abs T3)} H7 : {K |- pr1 S1 S3} H8 : {K |- pr1 S3 S2} ============================ {K |- pr1 (T3 S3) (T2 S2)} Subgoal 3.3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply IH to H1 _ H4.

Subgoal 3.2: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {K |- pr1 (abs T1) (abs T3)} H7 : {K |- pr1 S1 S3} H8 : {K |- pr1 S3 S2} H9 : {K |- pr1 (abs T3) (abs T2)} ============================ {K |- pr1 (T3 S3) (T2 S2)} Subgoal 3.3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply pr1_subst_lem to H1 H9 H8.

Subgoal 3.2: Variables: L K J S2 S1 T2 T1 S3 T3 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {K |- pr1 (abs T1) (abs T3)} H7 : {K |- pr1 S1 S3} H8 : {K |- pr1 S3 S2} H9 : {K |- pr1 (abs T3) (abs T2)} H10 : {K |- pr1 (T3 S3) (T2 S2)} ============================ {K |- pr1 (T3 S3) (T2 S2)} Subgoal 3.3 is: {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <search.

Subgoal 3.3: Variables: B L K J S2 S1 T2 T1 F IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {K, [F] |- pr1 (app (abs T1) S1) B} H7 : member F K ============================ {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <apply pr1_worlds to H1 H7.

Subgoal 3.3: Variables: B L K J S2 S1 T2 T1 B1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H4 : {J |- cd1 (abs T1) (abs T2)}* H5 : {J |- cd1 S1 S2}* H6 : {K, [pr1 B1 B1] |- pr1 (app (abs T1) S1) B} H7 : member (pr1 B1 B1) K H8 : name B1 H9 : member (trm B1) L H10 : member (cd1 B1 B1) J H11 : member (notabs B1) J ============================ {K |- pr1 B (T2 S2)} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H8.

Subgoal 3.3: Variables: B L K J S2 S1 T2 T1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs (L n1) (K n1) (J n1) H4 : {J n1 |- cd1 (abs (T1 n1)) (abs (T2 n1))}* H5 : {J n1 |- cd1 (S1 n1) (S2 n1)}* H6 : {K n1, [pr1 n1 n1] |- pr1 (app (abs (T1 n1)) (S1 n1)) (B n1)} H7 : member (pr1 n1 n1) (K n1) H9 : member (trm n1) (L n1) H10 : member (cd1 n1 n1) (J n1) H11 : member (notabs n1) (J n1) ============================ {K n1 |- pr1 (B n1) (T2 n1 (S2 n1))} Subgoal 4 is: {K |- pr1 B C} cd1_pr1_triangle <case H6.

Subgoal 4: Variables: A B C L K J F IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H2 : {K |- pr1 A B} H4 : {J, [F] |- cd1 A C}* H5 : member F J ============================ {K |- pr1 B C} cd1_pr1_triangle <apply cd_worlds to H1 H5.

Subgoal 4: Variables: A B C L K J F IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H2 : {K |- pr1 A B} H4 : {J, [F] |- cd1 A C}* H5 : member F J H6 : (exists A B, F = cd1 A B /\ name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J) \/ (exists A, F = notabs A /\ name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J) ============================ {K |- pr1 B C} cd1_pr1_triangle <case H6.

Subgoal 4.1: Variables: A B C L K J B1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H2 : {K |- pr1 A B} H4 : {J, [cd1 B1 B1] |- cd1 A C}* H5 : member (cd1 B1 B1) J H7 : name B1 H8 : member (trm B1) L H9 : member (pr1 B1 B1) K H10 : member (notabs B1) J ============================ {K |- pr1 B C} Subgoal 4.2 is: {K |- pr1 B C} cd1_pr1_triangle <case H4.

Subgoal 4.1: Variables: B C L K J IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H2 : {K |- pr1 C B} H5 : member (cd1 C C) J H7 : name C H8 : member (trm C) L H9 : member (pr1 C C) K H10 : member (notabs C) J ============================ {K |- pr1 B C} Subgoal 4.2 is: {K |- pr1 B C} cd1_pr1_triangle <apply pr1_name to H1 H2 H7.

Subgoal 4.1: Variables: C L K J IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H2 : {K |- pr1 C C} H5 : member (cd1 C C) J H7 : name C H8 : member (trm C) L H9 : member (pr1 C C) K H10 : member (notabs C) J ============================ {K |- pr1 C C} Subgoal 4.2 is: {K |- pr1 B C} cd1_pr1_triangle <search.

Subgoal 4.2: Variables: A B C L K J A1 IH : forall A B C L K J, ctxs L K J -> {K |- pr1 A B} -> {J |- cd1 A C}* -> {K |- pr1 B C} H1 : ctxs L K J H2 : {K |- pr1 A B} H4 : {J, [notabs A1] |- cd1 A C}* H5 : member (notabs A1) J H7 : name A1 H8 : member (trm A1) L H9 : member (pr1 A1 A1) K H10 : member (cd1 A1 A1) J ============================ {K |- pr1 B C} cd1_pr1_triangle <case H4.Proof completed.

Abella <Theorem pr1_diamond : forall A B1 B2 L K J, ctxs L K J -> {K |- pr1 A B1} -> {K |- pr1 A B2} -> (exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C}).

============================ forall A B1 B2 L K J, ctxs L K J -> {K |- pr1 A B1} -> {K |- pr1 A B2} -> (exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C}) pr1_diamond <intros.

Variables: A B1 B2 L K J H1 : ctxs L K J H2 : {K |- pr1 A B1} H3 : {K |- pr1 A B2} ============================ exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C} pr1_diamond <apply pr1_trm to H1 H2.

Variables: A B1 B2 L K J H1 : ctxs L K J H2 : {K |- pr1 A B1} H3 : {K |- pr1 A B2} H4 : {L |- trm A} ============================ exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C} pr1_diamond <apply cd1_exists to H1 H4.

Variables: A B1 B2 L K J B H1 : ctxs L K J H2 : {K |- pr1 A B1} H3 : {K |- pr1 A B2} H4 : {L |- trm A} H5 : {J |- cd1 A B} ============================ exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C} pr1_diamond <apply cd1_pr1_triangle to H1 H2 H5.

Variables: A B1 B2 L K J B H1 : ctxs L K J H2 : {K |- pr1 A B1} H3 : {K |- pr1 A B2} H4 : {L |- trm A} H5 : {J |- cd1 A B} H6 : {K |- pr1 B1 B} ============================ exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C} pr1_diamond <apply cd1_pr1_triangle to H1 H3 H5.

Variables: A B1 B2 L K J B H1 : ctxs L K J H2 : {K |- pr1 A B1} H3 : {K |- pr1 A B2} H4 : {L |- trm A} H5 : {J |- cd1 A B} H6 : {K |- pr1 B1 B} H7 : {K |- pr1 B2 B} ============================ exists C, {K |- pr1 B1 C} /\ {K |- pr1 B2 C} pr1_diamond <search.Proof completed.

Abella <