Welcome to Abella 1.1.3-dev2
Reading clauses from cr.mod
Abella < Define ctxs nil nil nil.
Abella < Define nabla x, ctxs (trm x :: L) (pr1 x x :: K) (cd1 x x :: notabs x :: J) := ctxs L K J.
Abella < Define nabla x, name x.
Abella < Theorem trm_worlds :
forall A L K J, ctxs L K J -> member (trm A) L -> name A /\
member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J.
1 subgoal(s).
============================
forall A L K J, ctxs L K J -> member (trm A) L -> name A /\
member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
trm_worlds < induction on 2.
1 subgoal(s).
IH : forall A L K J, ctxs L K J -> member (trm A) L * -> name A /\
member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
============================
forall A L K J, ctxs L K J -> member (trm A) L @ -> name A /\
member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
trm_worlds < intros.
1 subgoal(s).
Variables: A, L, K, J
IH : forall A L K J, ctxs L K J -> member (trm A) L * -> name A /\
member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
H1 : ctxs L K J
H2 : member (trm A) L @
============================
name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
trm_worlds < case H2.
2 subgoal(s).
Variables: A, L, K, J, L1
IH : forall A L K J, ctxs L K J -> member (trm A) L * -> name A /\
member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
H1 : ctxs (trm A :: L1) K J
============================
name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
subgoal 2 is:
name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
trm_worlds < case H1.
2 subgoal(s).
Variables: A, L, K, J, L1, J1, K1, L2
IH : forall A L K J, ctxs L K J -> member (trm A) L * -> name A /\
member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
H3 : ctxs L2 K1 J1
============================
name n1 /\ member (pr1 n1 n1) (pr1 n1 n1 :: K1) /\
member (cd1 n1 n1) (cd1 n1 n1 :: notabs n1 :: J1) /\
member (notabs n1) (cd1 n1 n1 :: notabs n1 :: J1)
subgoal 2 is:
name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
trm_worlds < search.
1 subgoal(s).
Variables: A, L, K, J, L1, B
IH : forall A L K J, ctxs L K J -> member (trm A) L * -> name A /\
member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
H1 : ctxs (B :: L1) K J
H3 : member (trm A) L1 *
============================
name A /\ member (pr1 A A) K /\ member (cd1 A A) J /\ member (notabs A) J
trm_worlds < case H1.
1 subgoal(s).
Variables: A, L, K, J, L1, B, J1, K1, L2
IH : forall A L K J, ctxs L K J -> member (trm A) L * -> 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
============================
name (A n1) /\ member (pr1 (A n1) (A n1)) (pr1 n1 n1 :: K1) /\
member (cd1 (A n1) (A n1)) (cd1 n1 n1 :: notabs n1 :: J1) /\
member (notabs (A n1)) (cd1 n1 n1 :: notabs n1 :: J1)
trm_worlds < apply IH to H4 H3.
1 subgoal(s).
Variables: A, L, K, J, L1, B, J1, K1, L2
IH : forall A L K J, ctxs L K J -> member (trm A) L * -> 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
============================
name (A n1) /\ member (pr1 (A n1) (A n1)) (pr1 n1 n1 :: K1) /\
member (cd1 (A n1) (A n1)) (cd1 n1 n1 :: notabs n1 :: J1) /\
member (notabs (A n1)) (cd1 n1 n1 :: notabs n1 :: J1)
trm_worlds < search.
Proof completed.
Abella < Theorem pr1_worlds :
forall A B L K J, ctxs L K J -> member (pr1 A B) K -> name A /\ A = B /\
member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J.
1 subgoal(s).
============================
forall A B L K J, ctxs L K J -> member (pr1 A B) K -> name A /\ A = B /\
member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J
pr1_worlds < induction on 2.
1 subgoal(s).
IH : forall A B L K J, ctxs L K J -> member (pr1 A B) K * -> name A /\
A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
============================
forall A B L K J, ctxs L K J -> member (pr1 A B) K @ -> name A /\ A = B /\
member (trm A) L /\ member (cd1 A B) J /\ member (notabs A) J
pr1_worlds < intros.
1 subgoal(s).
Variables: A, B, L, K, J
IH : forall A B L K J, ctxs L K J -> member (pr1 A B) K * -> name A /\
A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
H1 : ctxs L K J
H2 : member (pr1 A B) K @
============================
name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
pr1_worlds < case H2.
2 subgoal(s).
Variables: A, B, L, K, J, L1
IH : forall A B L K J, ctxs L K J -> member (pr1 A B) K * -> name A /\
A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
H1 : ctxs L (pr1 A B :: L1) J
============================
name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
subgoal 2 is:
name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
pr1_worlds < case H1.
2 subgoal(s).
Variables: A, B, L, K, J, L1, J1, K1, L2
IH : forall A B L K J, ctxs L K J -> member (pr1 A B) K * -> name A /\
A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
H3 : ctxs L2 K1 J1
============================
name n1 /\ n1 = n1 /\ member (trm n1) (trm n1 :: L2) /\
member (cd1 n1 n1) (cd1 n1 n1 :: notabs n1 :: J1) /\
member (notabs n1) (cd1 n1 n1 :: notabs n1 :: J1)
subgoal 2 is:
name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
pr1_worlds < search.
1 subgoal(s).
Variables: A, B, L, K, J, L1, B1
IH : forall A B L K J, ctxs L K J -> member (pr1 A B) K * -> name A /\
A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
H1 : ctxs L (B1 :: L1) J
H3 : member (pr1 A B) L1 *
============================
name A /\ A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
pr1_worlds < case H1.
1 subgoal(s).
Variables: A, B, L, K, J, L1, B1, J1, K1, L2
IH : forall A B L K J, ctxs L K J -> member (pr1 A B) K * -> name A /\
A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
H3 : member (pr1 (A n1) (B n1)) K1 *
H4 : ctxs L2 K1 J1
============================
name (A n1) /\ A n1 = B n1 /\ member (trm (A n1)) (trm n1 :: L2) /\
member (cd1 (A n1) (B n1)) (cd1 n1 n1 :: notabs n1 :: J1) /\
member (notabs (A n1)) (cd1 n1 n1 :: notabs n1 :: J1)
pr1_worlds < apply IH to H4 H3.
1 subgoal(s).
Variables: A, B, L, K, J, L1, B1, J1, K1, L2
IH : forall A B L K J, ctxs L K J -> member (pr1 A B) K * -> name A /\
A = B /\ member (trm A) L /\ member (cd1 A B) J /\
member (notabs A) J
H3 : member (pr1 (B n1) (B n1)) K1 *
H4 : ctxs L2 K1 J1
H5 : name (B n1)
H6 : member (trm (B n1)) L2
H7 : member (cd1 (B n1) (B n1)) J1
H8 : member (notabs (B n1)) J1
============================
name (B n1) /\ B n1 = B n1 /\ member (trm (B n1)) (trm n1 :: L2) /\
member (cd1 (B n1) (B n1)) (cd1 n1 n1 :: notabs n1 :: J1) /\
member (notabs (B n1)) (cd1 n1 n1 :: notabs n1 :: J1)
pr1_worlds < search.
Proof completed.
Abella < Theorem cd1_worlds :
forall A B L K J, ctxs L K J -> member (cd1 A B) J -> name A /\ A = B /\
member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J.
1 subgoal(s).
============================
forall A B L K J, ctxs L K J -> member (cd1 A B) J -> name A /\ A = B /\
member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J
cd1_worlds < induction on 2.
1 subgoal(s).
IH : forall A B L K J, ctxs L K J -> member (cd1 A B) J * -> name A /\
A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) J
============================
forall A B L K J, ctxs L K J -> member (cd1 A B) J @ -> name A /\ A = B /\
member (trm A) L /\ member (pr1 A A) K /\ member (notabs A) J
cd1_worlds < intros.
1 subgoal(s).
Variables: A, B, L, K, J
IH : forall A B L K J, ctxs L K J -> member (cd1 A B) J * -> name A /\
A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) J
H1 : ctxs L K J
H2 : member (cd1 A B) J @
============================
name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) J
cd1_worlds < case H2.
2 subgoal(s).
Variables: A, B, L, K, J, L1
IH : forall A B L K J, ctxs L K J -> member (cd1 A B) J * -> name A /\
A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) J
H1 : ctxs L K (cd1 A B :: L1)
============================
name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) (cd1 A B :: L1)
subgoal 2 is:
name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) (B1 :: L1)
cd1_worlds < case H1.
2 subgoal(s).
Variables: A, B, L, K, J, L1, J1, K1, L2
IH : forall A B L K J, ctxs L K J -> member (cd1 A B) J * -> name A /\
A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) J
H3 : ctxs L2 K1 J1
============================
name n1 /\ n1 = n1 /\ member (trm n1) (trm n1 :: L2) /\
member (pr1 n1 n1) (pr1 n1 n1 :: K1) /\
member (notabs n1) (cd1 n1 n1 :: notabs n1 :: J1)
subgoal 2 is:
name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) (B1 :: L1)
cd1_worlds < search.
1 subgoal(s).
Variables: A, B, L, K, J, L1, B1
IH : forall A B L K J, ctxs L K J -> member (cd1 A B) J * -> name A /\
A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) J
H1 : ctxs L K (B1 :: L1)
H3 : member (cd1 A B) L1 *
============================
name A /\ A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) (B1 :: L1)
cd1_worlds < case H1.
1 subgoal(s).
Variables: A, B, L, K, J, L1, B1, J1, K1, L2
IH : forall A B L K J, ctxs L K J -> member (cd1 A B) J * -> name A /\
A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) J
H3 : member (cd1 (A n1) (B n1)) (notabs n1 :: J1) *
H4 : ctxs L2 K1 J1
============================
name (A n1) /\ A n1 = B n1 /\ member (trm (A n1)) (trm n1 :: L2) /\
member (pr1 (A n1) (A n1)) (pr1 n1 n1 :: K1) /\
member (notabs (A n1)) (cd1 n1 n1 :: notabs n1 :: J1)
cd1_worlds < case H3.
1 subgoal(s).
Variables: A, B, L, K, J, L1, B1, J1, K1, L2
IH : forall A B L K J, ctxs L K J -> member (cd1 A B) J * -> name A /\
A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) J
H4 : ctxs L2 K1 J1
H5 : member (cd1 (A n1) (B n1)) J1 *
============================
name (A n1) /\ A n1 = B n1 /\ member (trm (A n1)) (trm n1 :: L2) /\
member (pr1 (A n1) (A n1)) (pr1 n1 n1 :: K1) /\
member (notabs (A n1)) (cd1 n1 n1 :: notabs n1 :: J1)
cd1_worlds < apply IH to H4 H5.
1 subgoal(s).
Variables: A, B, L, K, J, L1, B1, J1, K1, L2
IH : forall A B L K J, ctxs L K J -> member (cd1 A B) J * -> name A /\
A = B /\ member (trm A) L /\ member (pr1 A A) K /\
member (notabs A) J
H4 : ctxs L2 K1 J1
H5 : member (cd1 (B n1) (B n1)) J1 *
H6 : name (B n1)
H7 : member (trm (B n1)) L2
H8 : member (pr1 (B n1) (B n1)) K1
H9 : member (notabs (B n1)) J1
============================
name (B n1) /\ B n1 = B n1 /\ member (trm (B n1)) (trm n1 :: L2) /\
member (pr1 (B n1) (B n1)) (pr1 n1 n1 :: K1) /\
member (notabs (B n1)) (cd1 n1 n1 :: notabs n1 :: J1)
cd1_worlds < search.
Proof completed.
Abella < Theorem notabs_worlds :
forall A L K J, ctxs L K J -> member (notabs A) J -> name A /\
member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J.
1 subgoal(s).
============================
forall A L K J, ctxs L K J -> member (notabs A) J -> name A /\
member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J
notabs_worlds < induction on 2.
1 subgoal(s).
IH : forall A L K J, ctxs L K J -> member (notabs A) J * -> name A /\
member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J
============================
forall A L K J, ctxs L K J -> member (notabs A) J @ -> name A /\
member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J
notabs_worlds < intros.
1 subgoal(s).
Variables: A, L, K, J
IH : forall A L K J, ctxs L K J -> member (notabs A) J * -> name A /\
member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J
H1 : ctxs L K J
H2 : member (notabs A) J @
============================
name A /\ member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J
notabs_worlds < case H2.
2 subgoal(s).
Variables: A, L, K, J, L1
IH : forall A L K J, ctxs L K J -> member (notabs A) J * -> name A /\
member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J
H1 : ctxs L K (notabs A :: L1)
============================
name A /\ member (trm A) L /\ member (pr1 A A) K /\
member (cd1 A A) (notabs A :: L1)
subgoal 2 is:
name A /\ member (trm A) L /\ member (pr1 A A) K /\
member (cd1 A A) (B :: L1)
notabs_worlds < case H1.
1 subgoal(s).
Variables: A, L, K, J, L1, B
IH : forall A L K J, ctxs L K J -> member (notabs A) J * -> name A /\
member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J
H1 : ctxs L K (B :: L1)
H3 : member (notabs A) L1 *
============================
name A /\ member (trm A) L /\ member (pr1 A A) K /\
member (cd1 A A) (B :: L1)
notabs_worlds < case H1.
1 subgoal(s).
Variables: A, L, K, J, L1, B, J1, K1, L2
IH : forall A L K J, ctxs L K J -> member (notabs A) J * -> name A /\
member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J
H3 : member (notabs (A n1)) (notabs n1 :: J1) *
H4 : ctxs L2 K1 J1
============================
name (A n1) /\ member (trm (A n1)) (trm n1 :: L2) /\
member (pr1 (A n1) (A n1)) (pr1 n1 n1 :: K1) /\
member (cd1 (A n1) (A n1)) (cd1 n1 n1 :: notabs n1 :: J1)
notabs_worlds < case H3.
2 subgoal(s).
Variables: A, L, K, J, L1, B, J1, K1, L2
IH : forall A L K J, ctxs L K J -> member (notabs A) J * -> name A /\
member (trm A) L /\ member (pr1 A A) K /\ member (cd1 A A) J
H4 : ctxs L2 K1 J1
============================
name n1 /\ member (trm n1) (trm n1 :: L2) /\
member (pr1 n1 n1) (pr1 n1 n1 :: K1) /\
member (cd1 n1 n1) (cd1 n1 n1 :: notabs n1 :: J1)
subgoal 2 is:
name (A n1) /\ member (trm (A n1)) (trm n1 :: L2) /\
member (pr1 (A n1) (A n1)) (pr1 n1 n1 :: K1) /\
member (cd1 (A n1) (A n1)) (cd1 n1 n1 :: notabs n1 :: J1)
notabs_worlds < search.
1 subgoal(s).
Variables: A, L, K, J, L1, B, J1, K1, L2
IH : forall A L K J, ctxs L K J -> member (notabs A) J * -> 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 *
============================
name (A n1) /\ member (trm (A n1)) (trm n1 :: L2) /\
member (pr1 (A n1) (A n1)) (pr1 n1 n1 :: K1) /\
member (cd1 (A n1) (A n1)) (cd1 n1 n1 :: notabs n1 :: J1)
notabs_worlds < apply IH to H4 H5.
1 subgoal(s).
Variables: A, L, K, J, L1, B, J1, K1, L2
IH : forall A L K J, ctxs L K J -> member (notabs A) J * -> 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 *
H6 : name (A n1)
H7 : member (trm (A n1)) L2
H8 : member (pr1 (A n1) (A n1)) K1
H9 : member (cd1 (A n1) (A n1)) J1
============================
name (A n1) /\ member (trm (A n1)) (trm n1 :: L2) /\
member (pr1 (A n1) (A n1)) (pr1 n1 n1 :: K1) /\
member (cd1 (A n1) (A n1)) (cd1 n1 n1 :: notabs n1 :: J1)
notabs_worlds < search.
Proof completed.
Abella < Theorem notabs_abs_absurd :
forall A L K J, ctxs L K J -> {J |- notabs (abs A)} -> false.
1 subgoal(s).
============================
forall A L K J, ctxs L K J -> {J |- notabs (abs A)} -> false
notabs_abs_absurd < intros.
1 subgoal(s).
Variables: A, L, K, J
H1 : ctxs L K J
H2 : {J |- notabs (abs A)}
============================
false
notabs_abs_absurd < case H2.
1 subgoal(s).
Variables: A, L, K, J
H1 : ctxs L K J
H3 : member (notabs (abs A)) J
============================
false
notabs_abs_absurd < apply notabs_worlds to H1 H3.
1 subgoal(s).
Variables: A, L, K, J
H1 : ctxs L K J
H3 : member (notabs (abs A)) J
H4 : name (abs A)
H5 : member (trm (abs A)) L
H6 : member (pr1 (abs A) (abs A)) K
H7 : member (cd1 (abs A) (abs A)) J
============================
false
notabs_abs_absurd < case H4.
Proof completed.
Abella < Theorem cd1_trm :
forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {L |- trm A}.
1 subgoal(s).
============================
forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {L |- trm A}
cd1_trm < induction on 2.
1 subgoal(s).
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.
1 subgoal(s).
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.
4 subgoal(s).
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
H3 : member (cd1 A B) J
============================
{L |- trm A}
subgoal 2 is:
{L |- trm (app T1 S1)}
subgoal 3 is:
{L |- trm (abs S1)}
subgoal 4 is:
{L |- trm (app (abs T1) S1)}
cd1_trm < apply cd1_worlds to H1 H3.
4 subgoal(s).
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
H3 : member (cd1 B B) J
H4 : name B
H5 : member (trm B) L
H6 : member (pr1 B B) K
H7 : member (notabs B) J
============================
{L |- trm B}
subgoal 2 is:
{L |- trm (app T1 S1)}
subgoal 3 is:
{L |- trm (abs S1)}
subgoal 4 is:
{L |- trm (app (abs T1) S1)}
cd1_trm < search.
3 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
cd1_trm < apply IH to H1 H4.
3 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
cd1_trm < apply IH to H1 H5.
3 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
cd1_trm < search.
2 subgoal(s).
Variables: A, B, 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 2 is:
{L |- trm (app (abs T1) S1)}
cd1_trm < apply IH to _ H3.
2 subgoal(s).
Variables: A, B, 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 2 is:
{L |- trm (app (abs T1) S1)}
cd1_trm < search.
1 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
cd1_trm < apply IH to H1 H3.
1 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
cd1_trm < apply IH to H1 H4.
1 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
cd1_trm < search.
Proof completed.
Abella < Theorem pr1_trm :
forall A B L K J, ctxs L K J -> {K |- pr1 A B} -> {L |- trm A}.
1 subgoal(s).
============================
forall A B L K J, ctxs L K J -> {K |- pr1 A B} -> {L |- trm A}
pr1_trm < induction on 2.
1 subgoal(s).
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.
1 subgoal(s).
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.
4 subgoal(s).
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
H3 : member (pr1 A B) K
============================
{L |- trm A}
subgoal 2 is:
{L |- trm (app T1 S1)}
subgoal 3 is:
{L |- trm (abs S1)}
subgoal 4 is:
{L |- trm (app (abs T1) S1)}
pr1_trm < apply pr1_worlds to H1 H3.
4 subgoal(s).
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
H3 : member (pr1 B B) K
H4 : name B
H5 : member (trm B) L
H6 : member (cd1 B B) J
H7 : member (notabs B) J
============================
{L |- trm B}
subgoal 2 is:
{L |- trm (app T1 S1)}
subgoal 3 is:
{L |- trm (abs S1)}
subgoal 4 is:
{L |- trm (app (abs T1) S1)}
pr1_trm < search.
3 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
pr1_trm < apply IH to H1 H3.
3 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
pr1_trm < apply IH to H1 H4.
3 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
pr1_trm < search.
2 subgoal(s).
Variables: A, B, 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 2 is:
{L |- trm (app (abs T1) S1)}
pr1_trm < apply IH to _ H3.
2 subgoal(s).
Variables: A, B, 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 2 is:
{L |- trm (app (abs T1) S1)}
pr1_trm < search.
1 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
pr1_trm < apply IH to H1 H3.
1 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
pr1_trm < apply IH to H1 H4.
1 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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)}
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}.
1 subgoal(s).
============================
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.
1 subgoal(s).
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.
1 subgoal(s).
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.
3 subgoal(s).
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
H3 : {J |- cd1 A B}
H4 : member (trm A) L
============================
{K |- pr1 A B}
subgoal 2 is:
{K |- pr1 (app M N) B}
subgoal 3 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < apply trm_worlds to H1 H4.
3 subgoal(s).
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
H3 : {J |- cd1 A B}
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
============================
{K |- pr1 A B}
subgoal 2 is:
{K |- pr1 (app M N) B}
subgoal 3 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < case H3.
6 subgoal(s).
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
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
H9 : member (cd1 A B) J
============================
{K |- pr1 A B}
subgoal 2 is:
{K |- pr1 (app T1 S1) (app T2 S2)}
subgoal 3 is:
{K |- pr1 (abs S1) (abs S2)}
subgoal 4 is:
{K |- pr1 (app (abs T1) S1) (T2 S2)}
subgoal 5 is:
{K |- pr1 (app M N) B}
subgoal 6 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < apply cd1_worlds to H1 H9.
6 subgoal(s).
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
H4 : member (trm B) L
H5 : name B
H6 : member (pr1 B B) K
H7 : member (cd1 B B) J
H8 : member (notabs B) J
H9 : member (cd1 B B) J
H10 : name B
H11 : member (trm B) L
H12 : member (pr1 B B) K
H13 : member (notabs B) J
============================
{K |- pr1 B B}
subgoal 2 is:
{K |- pr1 (app T1 S1) (app T2 S2)}
subgoal 3 is:
{K |- pr1 (abs S1) (abs S2)}
subgoal 4 is:
{K |- pr1 (app (abs T1) S1) (T2 S2)}
subgoal 5 is:
{K |- pr1 (app M N) B}
subgoal 6 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < search.
5 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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
H4 : member (trm (app T1 S1)) L
H5 : name (app T1 S1)
H6 : member (pr1 (app T1 S1) (app T1 S1)) K
H7 : member (cd1 (app T1 S1) (app T1 S1)) J
H8 : member (notabs (app T1 S1)) J
H9 : {J |- notabs T1}
H10 : {J |- cd1 T1 T2}
H11 : {J |- cd1 S1 S2}
============================
{K |- pr1 (app T1 S1) (app T2 S2)}
subgoal 2 is:
{K |- pr1 (abs S1) (abs S2)}
subgoal 3 is:
{K |- pr1 (app (abs T1) S1) (T2 S2)}
subgoal 4 is:
{K |- pr1 (app M N) B}
subgoal 5 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < case H5.
4 subgoal(s).
Variables: A, B, L, K, J, S2, S1
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
H4 : member (trm (abs S1)) L
H5 : name (abs S1)
H6 : member (pr1 (abs S1) (abs S1)) K
H7 : member (cd1 (abs S1) (abs S1)) J
H8 : member (notabs (abs S1)) J
H9 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}
============================
{K |- pr1 (abs S1) (abs S2)}
subgoal 2 is:
{K |- pr1 (app (abs T1) S1) (T2 S2)}
subgoal 3 is:
{K |- pr1 (app M N) B}
subgoal 4 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < case H5.
3 subgoal(s).
Variables: A, B, L, K, J, S2, T2, S1, 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
H4 : member (trm (app (abs T1) S1)) L
H5 : name (app (abs T1) S1)
H6 : member (pr1 (app (abs T1) S1) (app (abs T1) S1)) K
H7 : member (cd1 (app (abs T1) S1) (app (abs T1) S1)) J
H8 : member (notabs (app (abs T1) S1)) J
H9 : {J |- cd1 (abs T1) (abs T2)}
H10 : {J |- cd1 S1 S2}
============================
{K |- pr1 (app (abs T1) S1) (T2 S2)}
subgoal 2 is:
{K |- pr1 (app M N) B}
subgoal 3 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < case H5.
2 subgoal(s).
Variables: A, 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
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}
pre_cd1_pr1 < case H3.
4 subgoal(s).
Variables: A, 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
H4 : {L |- trm M}*
H5 : {L |- trm N}*
H6 : member (cd1 (app M N) B) J
============================
{K |- pr1 (app M N) B}
subgoal 2 is:
{K |- pr1 (app M N) (app T2 S2)}
subgoal 3 is:
{K |- pr1 (app (abs T1) N) (T2 S2)}
subgoal 4 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < apply cd1_worlds to H1 H6.
4 subgoal(s).
Variables: A, 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
H4 : {L |- trm M}*
H5 : {L |- trm N}*
H6 : member (cd1 (app M N) (app M N)) J
H7 : name (app M N)
H8 : member (trm (app M N)) L
H9 : member (pr1 (app M N) (app M N)) K
H10 : member (notabs (app M N)) J
============================
{K |- pr1 (app M N) (app M N)}
subgoal 2 is:
{K |- pr1 (app M N) (app T2 S2)}
subgoal 3 is:
{K |- pr1 (app (abs T1) N) (T2 S2)}
subgoal 4 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < case H7.
3 subgoal(s).
Variables: A, B, 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
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 2 is:
{K |- pr1 (app (abs T1) N) (T2 S2)}
subgoal 3 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < apply IH to H1 H4 H7.
3 subgoal(s).
Variables: A, B, 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
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 2 is:
{K |- pr1 (app (abs T1) N) (T2 S2)}
subgoal 3 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < apply IH to H1 H5 H8.
3 subgoal(s).
Variables: A, B, 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
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 2 is:
{K |- pr1 (app (abs T1) N) (T2 S2)}
subgoal 3 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < search.
2 subgoal(s).
Variables: A, B, L, K, J, N, M, 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
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 2 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < apply IH to H1 H4 H6.
2 subgoal(s).
Variables: A, B, L, K, J, N, M, 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
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 2 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < apply IH to H1 H5 H7.
2 subgoal(s).
Variables: A, B, L, K, J, N, M, 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
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 2 is:
{K |- pr1 (abs R) B}
pre_cd1_pr1 < search.
1 subgoal(s).
Variables: A, 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
H3 : {J |- cd1 (abs R) B}
H4 : {L, trm n1 |- trm (R n1)}*
============================
{K |- pr1 (abs R) B}
pre_cd1_pr1 < case H3.
2 subgoal(s).
Variables: A, 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
H4 : {L, trm n1 |- trm (R n1)}*
H5 : member (cd1 (abs R) B) J
============================
{K |- pr1 (abs R) B}
subgoal 2 is:
{K |- pr1 (abs R) (abs S2)}
pre_cd1_pr1 < apply cd1_worlds to H1 H5.
2 subgoal(s).
Variables: A, 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
H4 : {L, trm n1 |- trm (R n1)}*
H5 : member (cd1 (abs R) (abs R)) J
H6 : name (abs R)
H7 : member (trm (abs R)) L
H8 : member (pr1 (abs R) (abs R)) K
H9 : member (notabs (abs R)) J
============================
{K |- pr1 (abs R) (abs R)}
subgoal 2 is:
{K |- pr1 (abs R) (abs S2)}
pre_cd1_pr1 < case H6.
1 subgoal(s).
Variables: A, B, 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
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)}
pre_cd1_pr1 < apply IH to _ H4 H5.
1 subgoal(s).
Variables: A, B, 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
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)}
pre_cd1_pr1 < search.
Proof completed.
Abella < Theorem cd1_pr1 :
forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {K |- pr1 A B}.
1 subgoal(s).
============================
forall A B L K J, ctxs L K J -> {J |- cd1 A B} -> {K |- pr1 A B}
cd1_pr1 < intros.
1 subgoal(s).
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.
1 subgoal(s).
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.
1 subgoal(s).
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}.
1 subgoal(s).
============================
forall A L K J, ctxs L K J -> {L |- trm A} -> {K |- pr1 A A}
pr1_rfl < induction on 2.
1 subgoal(s).
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.
1 subgoal(s).
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.
3 subgoal(s).
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
H3 : member (trm A) L
============================
{K |- pr1 A A}
subgoal 2 is:
{K |- pr1 (app M N) (app M N)}
subgoal 3 is:
{K |- pr1 (abs R) (abs R)}
pr1_rfl < apply trm_worlds to H1 H3.
3 subgoal(s).
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
H3 : member (trm A) L
H4 : name A
H5 : member (pr1 A A) K
H6 : member (cd1 A A) J
H7 : member (notabs A) J
============================
{K |- pr1 A A}
subgoal 2 is:
{K |- pr1 (app M N) (app M N)}
subgoal 3 is:
{K |- pr1 (abs R) (abs R)}
pr1_rfl < search.
2 subgoal(s).
Variables: A, 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)}
pr1_rfl < apply IH to H1 H3.
2 subgoal(s).
Variables: A, 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)}
pr1_rfl < apply IH to H1 H4.
2 subgoal(s).
Variables: A, 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)}
pr1_rfl < search.
1 subgoal(s).
Variables: A, 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)}
pr1_rfl < apply IH to _ H3.
1 subgoal(s).
Variables: A, 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)}
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.
1 subgoal(s).
============================
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.
1 subgoal(s).
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.
1 subgoal(s).
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.
4 subgoal(s).
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
H3 : {J |- cd1 A C}
H4 : member (cd1 A B) J
============================
B = C
subgoal 2 is:
app T2 S2 = C
subgoal 3 is:
abs S2 = C
subgoal 4 is:
T2 S2 = C
cd1_unique < apply cd1_worlds to H1 H4.
4 subgoal(s).
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
H3 : {J |- cd1 B C}
H4 : member (cd1 B B) J
H5 : name B
H6 : member (trm B) L
H7 : member (pr1 B B) K
H8 : member (notabs B) J
============================
B = C
subgoal 2 is:
app T2 S2 = C
subgoal 3 is:
abs S2 = C
subgoal 4 is:
T2 S2 = C
cd1_unique < case H3.
7 subgoal(s).
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
H4 : member (cd1 B B) J
H5 : name B
H6 : member (trm B) L
H7 : member (pr1 B B) K
H8 : member (notabs B) J
H9 : member (cd1 B C) J
============================
B = C
subgoal 2 is:
app T1 S1 = app T2 S2
subgoal 3 is:
abs S1 = abs S2
subgoal 4 is:
app (abs T1) S1 = T2 S2
subgoal 5 is:
app T2 S2 = C
subgoal 6 is:
abs S2 = C
subgoal 7 is:
T2 S2 = C
cd1_unique < apply cd1_worlds to H1 H9.
7 subgoal(s).
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
H4 : member (cd1 C C) J
H5 : name C
H6 : member (trm C) L
H7 : member (pr1 C C) K
H8 : member (notabs C) J
H9 : member (cd1 C C) J
H10 : name C
H11 : member (trm C) L
H12 : member (pr1 C C) K
H13 : member (notabs C) J
============================
C = C
subgoal 2 is:
app T1 S1 = app T2 S2
subgoal 3 is:
abs S1 = abs S2
subgoal 4 is:
app (abs T1) S1 = T2 S2
subgoal 5 is:
app T2 S2 = C
subgoal 6 is:
abs S2 = C
subgoal 7 is:
T2 S2 = C
cd1_unique < search.
6 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
H4 : member (cd1 (app T1 S1) (app T1 S1)) J
H5 : name (app T1 S1)
H6 : member (trm (app T1 S1)) L
H7 : member (pr1 (app T1 S1) (app T1 S1)) K
H8 : member (notabs (app T1 S1)) J
H9 : {J |- notabs T1}
H10 : {J |- cd1 T1 T2}
H11 : {J |- cd1 S1 S2}
============================
app T1 S1 = app T2 S2
subgoal 2 is:
abs S1 = abs S2
subgoal 3 is:
app (abs T1) S1 = T2 S2
subgoal 4 is:
app T2 S2 = C
subgoal 5 is:
abs S2 = C
subgoal 6 is:
T2 S2 = C
cd1_unique < case H5.
5 subgoal(s).
Variables: A, B, 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
H4 : member (cd1 (abs S1) (abs S1)) J
H5 : name (abs S1)
H6 : member (trm (abs S1)) L
H7 : member (pr1 (abs S1) (abs S1)) K
H8 : member (notabs (abs S1)) J
H9 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}
============================
abs S1 = abs S2
subgoal 2 is:
app (abs T1) S1 = T2 S2
subgoal 3 is:
app T2 S2 = C
subgoal 4 is:
abs S2 = C
subgoal 5 is:
T2 S2 = C
cd1_unique < case H5.
4 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
H4 : member (cd1 (app (abs T1) S1) (app (abs T1) S1)) J
H5 : name (app (abs T1) S1)
H6 : member (trm (app (abs T1) S1)) L
H7 : member (pr1 (app (abs T1) S1) (app (abs T1) S1)) K
H8 : member (notabs (app (abs T1) S1)) J
H9 : {J |- cd1 (abs T1) (abs T2)}
H10 : {J |- cd1 S1 S2}
============================
app (abs T1) S1 = T2 S2
subgoal 2 is:
app T2 S2 = C
subgoal 3 is:
abs S2 = C
subgoal 4 is:
T2 S2 = C
cd1_unique < case H5.
3 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
cd1_unique < case H3.
5 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : member (cd1 (app T1 S1) C) J
============================
app T2 S2 = C
subgoal 2 is:
app T2 S2 = app T4 S4
subgoal 3 is:
app T2 S2 = T4 S4
subgoal 4 is:
abs S2 = C
subgoal 5 is:
T2 S2 = C
cd1_unique < apply cd1_worlds to H1 H7.
5 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : member (cd1 (app T1 S1) (app T1 S1)) J
H8 : name (app T1 S1)
H9 : member (trm (app T1 S1)) L
H10 : member (pr1 (app T1 S1) (app T1 S1)) K
H11 : member (notabs (app T1 S1)) J
============================
app T2 S2 = app T1 S1
subgoal 2 is:
app T2 S2 = app T4 S4
subgoal 3 is:
app T2 S2 = T4 S4
subgoal 4 is:
abs S2 = C
subgoal 5 is:
T2 S2 = C
cd1_unique < case H8.
4 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {J |- notabs T1}
H8 : {J |- cd1 T1 T4}
H9 : {J |- cd1 S1 S4}
============================
app T2 S2 = app T4 S4
subgoal 2 is:
app T2 S2 = T4 S4
subgoal 3 is:
abs S2 = C
subgoal 4 is:
T2 S2 = C
cd1_unique < apply IH to H1 H5 H8.
4 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 T1}*
H5 : {J |- cd1 T1 T4}*
H6 : {J |- cd1 S1 S2}*
H7 : {J |- notabs T1}
H8 : {J |- cd1 T1 T4}
H9 : {J |- cd1 S1 S4}
============================
app T4 S2 = app T4 S4
subgoal 2 is:
app T2 S2 = T4 S4
subgoal 3 is:
abs S2 = C
subgoal 4 is:
T2 S2 = C
cd1_unique < apply IH to H1 H6 H9.
4 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 T1}*
H5 : {J |- cd1 T1 T4}*
H6 : {J |- cd1 S1 S4}*
H7 : {J |- notabs T1}
H8 : {J |- cd1 T1 T4}
H9 : {J |- cd1 S1 S4}
============================
app T4 S4 = app T4 S4
subgoal 2 is:
app T2 S2 = T4 S4
subgoal 3 is:
abs S2 = C
subgoal 4 is:
T2 S2 = C
cd1_unique < search.
3 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, T4, 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 (abs T3)}*
H5 : {J |- cd1 (abs T3) T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {J |- cd1 (abs T3) (abs T4)}
H8 : {J |- cd1 S1 S4}
============================
app T2 S2 = T4 S4
subgoal 2 is:
abs S2 = C
subgoal 3 is:
T2 S2 = C
cd1_unique < apply notabs_abs_absurd to H1 H4.
2 subgoal(s).
Variables: A, B, 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 2 is:
T2 S2 = C
cd1_unique < case H3.
3 subgoal(s).
Variables: A, B, 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
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : member (cd1 (abs S1) C) J
============================
abs S2 = C
subgoal 2 is:
abs S2 = abs S4
subgoal 3 is:
T2 S2 = C
cd1_unique < apply cd1_worlds to H1 H5.
3 subgoal(s).
Variables: A, B, 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
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : member (cd1 (abs S1) (abs S1)) J
H6 : name (abs S1)
H7 : member (trm (abs S1)) L
H8 : member (pr1 (abs S1) (abs S1)) K
H9 : member (notabs (abs S1)) J
============================
abs S2 = abs S1
subgoal 2 is:
abs S2 = abs S4
subgoal 3 is:
T2 S2 = C
cd1_unique < case H6.
2 subgoal(s).
Variables: A, B, C, L, K, J, S2, S1, S4
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) (S4 n1)}
============================
abs S2 = abs S4
subgoal 2 is:
T2 S2 = C
cd1_unique < apply IH to _ H4 H5.
2 subgoal(s).
Variables: A, B, C, L, K, J, S2, S1, S4
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) (S4 n1)}*
H5 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S4 n1)}
============================
abs (x1\S4 x1) = abs S4
subgoal 2 is:
T2 S2 = C
cd1_unique < search.
1 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
cd1_unique < case H3.
3 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : member (cd1 (app (abs T1) S1) C) J
============================
T2 S2 = C
subgoal 2 is:
T2 S2 = app T4 S4
subgoal 3 is:
T2 S2 = T4 S4
cd1_unique < apply cd1_worlds to H1 H6.
3 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : member (cd1 (app (abs T1) S1) (app (abs T1) S1)) J
H7 : name (app (abs T1) S1)
H8 : member (trm (app (abs T1) S1)) L
H9 : member (pr1 (app (abs T1) S1) (app (abs T1) S1)) K
H10 : member (notabs (app (abs T1) S1)) J
============================
T2 S2 = app (abs T1) S1
subgoal 2 is:
T2 S2 = app T4 S4
subgoal 3 is:
T2 S2 = T4 S4
cd1_unique < case H7.
2 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {J |- notabs (abs T1)}
H7 : {J |- cd1 (abs T1) T4}
H8 : {J |- cd1 S1 S4}
============================
T2 S2 = app T4 S4
subgoal 2 is:
T2 S2 = T4 S4
cd1_unique < apply notabs_abs_absurd to H1 H6.
1 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {J |- cd1 (abs T1) (abs T4)}
H7 : {J |- cd1 S1 S4}
============================
T2 S2 = T4 S4
cd1_unique < apply IH to H1 H4 H6.
1 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 |- cd1 (abs T1) (abs T4)}*
H5 : {J |- cd1 S1 S2}*
H6 : {J |- cd1 (abs T1) (abs T4)}
H7 : {J |- cd1 S1 S4}
============================
T4 S2 = T4 S4
cd1_unique < apply IH to H1 H5 H7.
1 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 |- cd1 (abs T1) (abs T4)}*
H5 : {J |- cd1 S1 S4}*
H6 : {J |- cd1 (abs T1) (abs T4)}
H7 : {J |- cd1 S1 S4}
============================
T4 S4 = T4 S4
cd1_unique < search.
Proof completed.
Abella < Theorem cd1_exists :
forall A L K J, ctxs L K J -> {L |- trm A} -> (exists B, {J |- cd1 A B}).
1 subgoal(s).
============================
forall A L K J, ctxs L K J -> {L |- trm A} -> (exists B, {J |- cd1 A B})
cd1_exists < induction on 2.
1 subgoal(s).
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.
1 subgoal(s).
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.
3 subgoal(s).
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
H3 : member (trm A) L
============================
exists B, {J |- cd1 A B}
subgoal 2 is:
exists B, {J |- cd1 (app M N) B}
subgoal 3 is:
exists B, {J |- cd1 (abs R) B}
cd1_exists < apply trm_worlds to H1 H3.
3 subgoal(s).
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
H3 : member (trm A) L
H4 : name A
H5 : member (pr1 A A) K
H6 : member (cd1 A A) J
H7 : member (notabs A) J
============================
exists B, {J |- cd1 A B}
subgoal 2 is:
exists B, {J |- cd1 (app M N) B}
subgoal 3 is:
exists B, {J |- cd1 (abs R) B}
cd1_exists < search.
2 subgoal(s).
Variables: A, 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}
cd1_exists < apply IH to H1 H3.
2 subgoal(s).
Variables: A, 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}
cd1_exists < apply IH to H1 H4.
2 subgoal(s).
Variables: A, 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}
cd1_exists < case H3.
4 subgoal(s).
Variables: A, 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}
H7 : member (trm M) L
============================
exists B, {J |- cd1 (app M N) B}
subgoal 2 is:
exists B, {J |- cd1 (app (app M1 N1) N) B}
subgoal 3 is:
exists B, {J |- cd1 (app (abs R) N) B}
subgoal 4 is:
exists B, {J |- cd1 (abs R) B}
cd1_exists < apply trm_worlds to H1 H7.
4 subgoal(s).
Variables: A, 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}
H7 : member (trm M) L
H8 : name M
H9 : member (pr1 M M) K
H10 : member (cd1 M M) J
H11 : member (notabs M) J
============================
exists B, {J |- cd1 (app M N) B}
subgoal 2 is:
exists B, {J |- cd1 (app (app M1 N1) N) B}
subgoal 3 is:
exists B, {J |- cd1 (app (abs R) N) B}
subgoal 4 is:
exists B, {J |- cd1 (abs R) B}
cd1_exists < search.
3 subgoal(s).
Variables: A, L, K, J, N, M, 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 2 is:
exists B, {J |- cd1 (app (abs R) N) B}
subgoal 3 is:
exists B, {J |- cd1 (abs R) B}
cd1_exists < search.
2 subgoal(s).
Variables: A, L, K, J, N, M, 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 2 is:
exists B, {J |- cd1 (abs R) B}
cd1_exists < apply IH to _ H7.
2 subgoal(s).
Variables: A, L, K, J, N, M, 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 2 is:
exists B, {J |- cd1 (abs R) B}
cd1_exists < search.
1 subgoal(s).
Variables: A, 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}
cd1_exists < apply IH to _ H3.
1 subgoal(s).
Variables: A, 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}
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.
1 subgoal(s).
============================
forall A B L K J, ctxs L K J -> {K |- pr1 A B} -> name A -> B = A
pr1_name < intros.
1 subgoal(s).
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.
1 subgoal(s).
Variables: A, 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.
1 subgoal(s).
Variables: A, B, L, K, J
H1 : ctxs (L n1) (K n1) (J n1)
H4 : member (pr1 n1 (B n1)) (K n1)
============================
B n1 = n1
pr1_name < apply pr1_worlds to H1 H4.
1 subgoal(s).
Variables: A, B, L, K, J
H1 : ctxs (L n1) (K n1) (J n1)
H4 : member (pr1 n1 n1) (K n1)
H5 : name n1
H6 : member (trm n1) (L n1)
H7 : member (cd1 n1 n1) (J n1)
H8 : member (notabs n1) (J n1)
============================
n1 = n1
pr1_name < search.
Proof completed.
Abella < Theorem pr1_abs :
forall A R B L K J, ctxs L K J -> {K |- pr1 (abs R) B} -> (exists S,
B = abs S).
1 subgoal(s).
============================
forall A R B L K J, ctxs L K J -> {K |- pr1 (abs R) B} -> (exists S,
B = abs S)
pr1_abs < intros.
1 subgoal(s).
Variables: A, 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.
2 subgoal(s).
Variables: A, R, B, L, K, J
H1 : ctxs L K J
H3 : member (pr1 (abs R) B) K
============================
exists S, B = abs S
subgoal 2 is:
exists S, abs S2 = abs S
pr1_abs < apply pr1_worlds to H1 H3.
2 subgoal(s).
Variables: A, R, B, L, K, J
H1 : ctxs L K J
H3 : member (pr1 (abs R) (abs R)) K
H4 : name (abs R)
H5 : member (trm (abs R)) L
H6 : member (cd1 (abs R) (abs R)) J
H7 : member (notabs (abs R)) J
============================
exists S, abs R = abs S
subgoal 2 is:
exists S, abs S2 = abs S
pr1_abs < case H4.
1 subgoal(s).
Variables: A, R, B, 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
pr1_abs < search.
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)}.
1 subgoal(s).
============================
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.
1 subgoal(s).
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.
1 subgoal(s).
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.
4 subgoal(s).
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 : member (pr1 (A1 n1) (A2 n1)) (pr1 n1 n1 :: K)
============================
{K |- pr1 (A1 B1) (A2 B2)}
subgoal 2 is:
{K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))}
subgoal 3 is:
{K |- pr1 (abs (S1 B1)) (abs (S2 B2))}
subgoal 4 is:
{K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}
pre_pr1_subst_lem < case H4.
5 subgoal(s).
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}
============================
{K |- pr1 B1 B2}
subgoal 2 is:
{K |- pr1 (A1 B1) (A2 B2)}
subgoal 3 is:
{K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))}
subgoal 4 is:
{K |- pr1 (abs (S1 B1)) (abs (S2 B2))}
subgoal 5 is:
{K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}
pre_pr1_subst_lem < search.
4 subgoal(s).
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}
H5 : member (pr1 (A1 n1) (A2 n1)) K
============================
{K |- pr1 (A1 B1) (A2 B2)}
subgoal 2 is:
{K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))}
subgoal 3 is:
{K |- pr1 (abs (S1 B1)) (abs (S2 B2))}
subgoal 4 is:
{K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}
pre_pr1_subst_lem < apply pr1_worlds to H1 H5.
4 subgoal(s).
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}
H5 : member (pr1 (A2 n1) (A2 n1)) K
H6 : name (A2 n1)
H7 : member (trm (A2 n1)) L
H8 : member (cd1 (A2 n1) (A2 n1)) J
H9 : member (notabs (A2 n1)) J
============================
{K |- pr1 (A2 B1) (A2 B2)}
subgoal 2 is:
{K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))}
subgoal 3 is:
{K |- pr1 (abs (S1 B1)) (abs (S2 B2))}
subgoal 4 is:
{K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}
pre_pr1_subst_lem < case H6.
5 subgoal(s).
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 n2) (K n2) (J n2)
H3 : {K n2 |- pr1 (B1 n2) (B2 n2)}
H5 : member (pr1 n2 n2) (K n2)
H7 : member (trm n2) (L n2)
H8 : member (cd1 n2 n2) (J n2)
H9 : member (notabs n2) (J n2)
============================
{K n2 |- pr1 n2 n2}
subgoal 2 is:
{K |- pr1 B1 B2}
subgoal 3 is:
{K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))}
subgoal 4 is:
{K |- pr1 (abs (S1 B1)) (abs (S2 B2))}
subgoal 5 is:
{K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}
pre_pr1_subst_lem < search.
4 subgoal(s).
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}
H5 : member (pr1 n1 n1) K
H7 : member (trm n1) L
H8 : member (cd1 n1 n1) J
H9 : member (notabs n1) J
============================
{K |- pr1 B1 B2}
subgoal 2 is:
{K |- pr1 (app (T1 B1) (S1 B1)) (app (T2 B2) (S2 B2))}
subgoal 3 is:
{K |- pr1 (abs (S1 B1)) (abs (S2 B2))}
subgoal 4 is:
{K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}
pre_pr1_subst_lem < search.
3 subgoal(s).
Variables: A1, A2, B1, B2, L, K, J, S2, T2, S1, 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))}
pre_pr1_subst_lem < apply IH to H1 H4 H3.
3 subgoal(s).
Variables: A1, A2, B1, B2, L, K, J, S2, T2, S1, 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))}
pre_pr1_subst_lem < apply IH to H1 H5 H3.
3 subgoal(s).
Variables: A1, A2, B1, B2, L, K, J, S2, T2, S1, 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))}
pre_pr1_subst_lem < search.
2 subgoal(s).
Variables: A1, A2, 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 2 is:
{K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}
pre_pr1_subst_lem < apply IH to _ H4 H3.
2 subgoal(s).
Variables: A1, A2, 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 2 is:
{K |- pr1 (app (abs (T1 B1)) (S1 B1)) (T2 B2 (S2 B2))}
pre_pr1_subst_lem < search.
1 subgoal(s).
Variables: A1, A2, B1, B2, L, K, J, S2, T2, S1, 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))}
pre_pr1_subst_lem < apply IH to H1 H4 H3.
1 subgoal(s).
Variables: A1, A2, B1, B2, L, K, J, S2, T2, S1, 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))}
pre_pr1_subst_lem < apply IH to H1 H5 H3.
1 subgoal(s).
Variables: A1, A2, B1, B2, L, K, J, S2, T2, S1, 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))}
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)}.
1 subgoal(s).
============================
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.
1 subgoal(s).
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.
2 subgoal(s).
Variables: A1, A2, B1, B2, L, K, J
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : member (pr1 (abs A1) (abs A2)) K
============================
{K |- pr1 (A1 B1) (A2 B2)}
subgoal 2 is:
{K |- pr1 (A1 B1) (A2 B2)}
pr1_subst_lem < apply pr1_worlds to H1 H4.
2 subgoal(s).
Variables: A1, A2, B1, B2, L, K, J
H1 : ctxs L K J
H3 : {K |- pr1 B1 B2}
H4 : member (pr1 (abs A2) (abs A2)) K
H5 : name (abs A2)
H6 : member (trm (abs A2)) L
H7 : member (cd1 (abs A2) (abs A2)) J
H8 : member (notabs (abs A2)) J
============================
{K |- pr1 (A2 B1) (A2 B2)}
subgoal 2 is:
{K |- pr1 (A1 B1) (A2 B2)}
pr1_subst_lem < case H5.
1 subgoal(s).
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)}
pr1_subst_lem < apply pre_pr1_subst_lem to H1 H4 H3.
1 subgoal(s).
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)}
pr1_subst_lem < search.
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}.
1 subgoal(s).
============================
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.
1 subgoal(s).
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.
1 subgoal(s).
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.
4 subgoal(s).
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}
H4 : member (cd1 A C) J
============================
{K |- pr1 B C}
subgoal 2 is:
{K |- pr1 B (app T2 S2)}
subgoal 3 is:
{K |- pr1 B (abs S2)}
subgoal 4 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < apply cd1_worlds to H1 H4.
4 subgoal(s).
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 C B}
H4 : member (cd1 C C) J
H5 : name C
H6 : member (trm C) L
H7 : member (pr1 C C) K
H8 : member (notabs C) J
============================
{K |- pr1 B C}
subgoal 2 is:
{K |- pr1 B (app T2 S2)}
subgoal 3 is:
{K |- pr1 B (abs S2)}
subgoal 4 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < apply pr1_name to H1 H2 H5.
4 subgoal(s).
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 C C}
H4 : member (cd1 C C) J
H5 : name C
H6 : member (trm C) L
H7 : member (pr1 C C) K
H8 : member (notabs C) J
============================
{K |- pr1 C C}
subgoal 2 is:
{K |- pr1 B (app T2 S2)}
subgoal 3 is:
{K |- pr1 B (abs S2)}
subgoal 4 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < search.
3 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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)}
cd1_pr1_triangle < case H2.
5 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : member (pr1 (app T1 S1) B) K
============================
{K |- pr1 B (app T2 S2)}
subgoal 2 is:
{K |- pr1 (app T4 S4) (app T2 S2)}
subgoal 3 is:
{K |- pr1 (T4 S4) (app T2 S2)}
subgoal 4 is:
{K |- pr1 B (abs S2)}
subgoal 5 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < apply pr1_worlds to H1 H7.
5 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
H4 : {J |- notabs T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : member (pr1 (app T1 S1) (app T1 S1)) K
H8 : name (app T1 S1)
H9 : member (trm (app T1 S1)) L
H10 : member (cd1 (app T1 S1) (app T1 S1)) J
H11 : member (notabs (app T1 S1)) J
============================
{K |- pr1 (app T1 S1) (app T2 S2)}
subgoal 2 is:
{K |- pr1 (app T4 S4) (app T2 S2)}
subgoal 3 is:
{K |- pr1 (T4 S4) (app T2 S2)}
subgoal 4 is:
{K |- pr1 B (abs S2)}
subgoal 5 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < case H8.
4 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 T1 T4}
H8 : {K |- pr1 S1 S4}
============================
{K |- pr1 (app T4 S4) (app T2 S2)}
subgoal 2 is:
{K |- pr1 (T4 S4) (app T2 S2)}
subgoal 3 is:
{K |- pr1 B (abs S2)}
subgoal 4 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < apply IH to H1 H7 H5.
4 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 T1 T4}
H8 : {K |- pr1 S1 S4}
H9 : {K |- pr1 T4 T2}
============================
{K |- pr1 (app T4 S4) (app T2 S2)}
subgoal 2 is:
{K |- pr1 (T4 S4) (app T2 S2)}
subgoal 3 is:
{K |- pr1 B (abs S2)}
subgoal 4 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < apply IH to H1 H8 H6.
4 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 T1}*
H5 : {J |- cd1 T1 T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 T1 T4}
H8 : {K |- pr1 S1 S4}
H9 : {K |- pr1 T4 T2}
H10 : {K |- pr1 S4 S2}
============================
{K |- pr1 (app T4 S4) (app T2 S2)}
subgoal 2 is:
{K |- pr1 (T4 S4) (app T2 S2)}
subgoal 3 is:
{K |- pr1 B (abs S2)}
subgoal 4 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < search.
3 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, T4, 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 (abs T3)}*
H5 : {J |- cd1 (abs T3) T2}*
H6 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 (abs T3) (abs T4)}
H8 : {K |- pr1 S1 S4}
============================
{K |- pr1 (T4 S4) (app T2 S2)}
subgoal 2 is:
{K |- pr1 B (abs S2)}
subgoal 3 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < apply notabs_abs_absurd to H1 H4.
2 subgoal(s).
Variables: A, B, C, 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 2 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < case H2.
3 subgoal(s).
Variables: A, B, C, 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
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : member (pr1 (abs S1) B) K
============================
{K |- pr1 B (abs S2)}
subgoal 2 is:
{K |- pr1 (abs S4) (abs S2)}
subgoal 3 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < apply pr1_worlds to H1 H5.
3 subgoal(s).
Variables: A, B, C, 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
H4 : {J, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : member (pr1 (abs S1) (abs S1)) K
H6 : name (abs S1)
H7 : member (trm (abs S1)) L
H8 : member (cd1 (abs S1) (abs S1)) J
H9 : member (notabs (abs S1)) J
============================
{K |- pr1 (abs S1) (abs S2)}
subgoal 2 is:
{K |- pr1 (abs S4) (abs S2)}
subgoal 3 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < case H6.
2 subgoal(s).
Variables: A, B, C, L, K, J, S2, S1, 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, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S4 n1)}
============================
{K |- pr1 (abs S4) (abs S2)}
subgoal 2 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < apply IH to _ H5 H4.
2 subgoal(s).
Variables: A, B, C, L, K, J, S2, S1, 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, notabs n1, cd1 n1 n1 |- cd1 (S1 n1) (S2 n1)}*
H5 : {K, pr1 n1 n1 |- pr1 (S1 n1) (S4 n1)}
H6 : {K, pr1 n1 n1 |- pr1 (S4 n1) (S2 n1)}
============================
{K |- pr1 (abs S4) (abs S2)}
subgoal 2 is:
{K |- pr1 B (T2 S2)}
cd1_pr1_triangle < search.
1 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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)}
cd1_pr1_triangle < case H2.
3 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : member (pr1 (app (abs T1) S1) B) K
============================
{K |- pr1 B (T2 S2)}
subgoal 2 is:
{K |- pr1 (app T4 S4) (T2 S2)}
subgoal 3 is:
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < apply pr1_worlds to H1 H6.
3 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, 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
H4 : {J |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : member (pr1 (app (abs T1) S1) (app (abs T1) S1)) K
H7 : name (app (abs T1) S1)
H8 : member (trm (app (abs T1) S1)) L
H9 : member (cd1 (app (abs T1) S1) (app (abs T1) S1)) J
H10 : member (notabs (app (abs T1) S1)) J
============================
{K |- pr1 (app (abs T1) S1) (T2 S2)}
subgoal 2 is:
{K |- pr1 (app T4 S4) (T2 S2)}
subgoal 3 is:
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < case H7.
2 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K |- pr1 (abs T1) T4}
H7 : {K |- pr1 S1 S4}
============================
{K |- pr1 (app T4 S4) (T2 S2)}
subgoal 2 is:
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < case H6.
3 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 S1 S4}
H8 : member (pr1 (abs T1) T4) K
============================
{K |- pr1 (app T4 S4) (T2 S2)}
subgoal 2 is:
{K |- pr1 (app (abs S5) S4) (T2 S2)}
subgoal 3 is:
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < apply pr1_worlds to H1 H8.
3 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H7 : {K |- pr1 S1 S4}
H8 : member (pr1 (abs T1) (abs T1)) K
H9 : name (abs T1)
H10 : member (trm (abs T1)) L
H11 : member (cd1 (abs T1) (abs T1)) J
H12 : member (notabs (abs T1)) J
============================
{K |- pr1 (app (abs T1) S4) (T2 S2)}
subgoal 2 is:
{K |- pr1 (app (abs S5) S4) (T2 S2)}
subgoal 3 is:
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < case H9.
2 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, T4, S5
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 S4}
H8 : {K, pr1 n1 n1 |- pr1 (T1 n1) (S5 n1)}
============================
{K |- pr1 (app (abs S5) S4) (T2 S2)}
subgoal 2 is:
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < apply IH to H1 H7 H5.
2 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, T4, S5
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 S4}
H8 : {K, pr1 n1 n1 |- pr1 (T1 n1) (S5 n1)}
H9 : {K |- pr1 S4 S2}
============================
{K |- pr1 (app (abs S5) S4) (T2 S2)}
subgoal 2 is:
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < apply IH to H1 _ H4.
2 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, T4, S5
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 S4}
H8 : {K, pr1 n1 n1 |- pr1 (T1 n1) (S5 n1)}
H9 : {K |- pr1 S4 S2}
H10 : {K |- pr1 (abs (x1\S5 x1)) (abs T2)}
============================
{K |- pr1 (app (abs S5) S4) (T2 S2)}
subgoal 2 is:
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < search.
1 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K |- pr1 (abs T1) (abs T4)}
H7 : {K |- pr1 S1 S4}
============================
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < apply IH to H1 H7 H5.
1 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K |- pr1 (abs T1) (abs T4)}
H7 : {K |- pr1 S1 S4}
H8 : {K |- pr1 S4 S2}
============================
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < apply IH to H1 _ H4.
1 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K |- pr1 (abs T1) (abs T4)}
H7 : {K |- pr1 S1 S4}
H8 : {K |- pr1 S4 S2}
H9 : {K |- pr1 (abs T4) (abs T2)}
============================
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < apply pr1_subst_lem to H1 H9 H8.
1 subgoal(s).
Variables: A, B, C, L, K, J, S2, T2, S1, T1, S4, 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 |- cd1 (abs T1) (abs T2)}*
H5 : {J |- cd1 S1 S2}*
H6 : {K |- pr1 (abs T1) (abs T4)}
H7 : {K |- pr1 S1 S4}
H8 : {K |- pr1 S4 S2}
H9 : {K |- pr1 (abs T4) (abs T2)}
H10 : {K |- pr1 (T4 S4) (T2 S2)}
============================
{K |- pr1 (T4 S4) (T2 S2)}
cd1_pr1_triangle < search.
Proof completed.
Abella < Theorem pr1_diamond :
forall A B1 B2 C 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}).
1 subgoal(s).
============================
forall A B1 B2 C 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.
1 subgoal(s).
Variables: A, B1, B2, C, 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.
1 subgoal(s).
Variables: A, B1, B2, C, 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.
1 subgoal(s).
Variables: A, B1, B2, C, 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.
1 subgoal(s).
Variables: A, B1, B2, C, 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.
1 subgoal(s).
Variables: A, B1, B2, C, 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 < Goodbye.
