Welcome to Abella 2.0.5-dev.
Abella < Specification "path".

Abella < Close tm, path.

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

Abella < Define path_var : path -> prop by
nabla x, path_var x.

Abella < Theorem member_prune_tm :
forall E L, nabla x, member (E x) L -> (exists F, E = y\F).

============================
forall E L, nabla x, member (E x) L -> (exists F, E = y\F)

member_prune_tm < induction on 1.

IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
forall E L, nabla x, member (E x) L @ -> (exists F, E = y\F)

member_prune_tm < intros.

Variables: E L
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H1 : member (E n1) L @
============================
exists F, E = y\F

member_prune_tm < case H1.
Subgoal 1:

Variables: L3 L2
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
exists F, z1\L2 = y\F

Subgoal 2 is:
exists F, E = y\F

member_prune_tm < search.
Subgoal 2:

Variables: E L3 L2
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member (E n1) L3 *
============================
exists F, E = y\F

member_prune_tm < apply IH to H2.
Subgoal 2:

Variables: L3 L2 F
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member F L3 *
============================
exists F1, z1\F = y\F1

member_prune_tm < search.
Proof completed.
Abella < Theorem member_prune_path :
forall E L, nabla x, member (E x) L -> (exists F, E = y\F).

============================
forall E L, nabla x, member (E x) L -> (exists F, E = y\F)

member_prune_path < induction on 1.

IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
forall E L, nabla x, member (E x) L @ -> (exists F, E = y\F)

member_prune_path < intros.

Variables: E L
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H1 : member (E n1) L @
============================
exists F, E = y\F

member_prune_path < case H1.
Subgoal 1:

Variables: L3 L2
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
exists F, z1\L2 = y\F

Subgoal 2 is:
exists F, E = y\F

member_prune_path < search.
Subgoal 2:

Variables: E L3 L2
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member (E n1) L3 *
============================
exists F, E = y\F

member_prune_path < apply IH to H2.
Subgoal 2:

Variables: L3 L2 F
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member F L3 *
============================
exists F1, z1\F = y\F1

member_prune_path < search.
Proof completed.
Abella < Define ctxs : olist -> olist -> prop by
ctxs nil nil;
nabla x p, ctxs (tm x :: L) (path x p :: K) := ctxs L K.

Abella < Theorem ctxs_member1 :
forall X L K, ctxs L K -> member X L ->
(exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\ path_var F).

============================
forall X L K, ctxs L K -> member X L ->
(exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\ path_var F)

ctxs_member1 < induction on 1.

IH : forall X L K, ctxs L K * -> member X L ->
(exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\
path_var F)
============================
forall X L K, ctxs L K @ -> member X L ->
(exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\ path_var F)

ctxs_member1 < intros.

Variables: X L K
IH : forall X L K, ctxs L K * -> member X L ->
(exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\
path_var F)
H1 : ctxs L K @
H2 : member X L
============================
exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\ path_var F

ctxs_member1 < case H1.
Subgoal 1:

Variables: X
IH : forall X L K, ctxs L K * -> member X L ->
(exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\
path_var F)
H2 : member X nil
============================
exists E F, X = tm E /\ tm_var E /\ member (path E F) nil /\ path_var F

Subgoal 2 is:
exists E F, X n1 n2 = tm E /\ tm_var E /\
member (path E F) (path n1 n2 :: K1) /\ path_var F

ctxs_member1 < case H2.
Subgoal 2:

Variables: X K1 L1
IH : forall X L K, ctxs L K * -> member X L ->
(exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\
path_var F)
H2 : member (X n1 n2) (tm n1 :: L1)
H3 : ctxs L1 K1 *
============================
exists E F, X n1 n2 = tm E /\ tm_var E /\
member (path E F) (path n1 n2 :: K1) /\ path_var F

ctxs_member1 < case H2.
Subgoal 2.1:

Variables: K1 L1
IH : forall X L K, ctxs L K * -> member X L ->
(exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\
path_var F)
H3 : ctxs L1 K1 *
============================
exists E F, tm n1 = tm E /\ tm_var E /\
member (path E F) (path n1 n2 :: K1) /\ path_var F

Subgoal 2.2 is:
exists E F, X n1 n2 = tm E /\ tm_var E /\
member (path E F) (path n1 n2 :: K1) /\ path_var F

ctxs_member1 < search.
Subgoal 2.2:

Variables: X K1 L1
IH : forall X L K, ctxs L K * -> member X L ->
(exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\
path_var F)
H3 : ctxs L1 K1 *
H4 : member (X n1 n2) L1
============================
exists E F, X n1 n2 = tm E /\ tm_var E /\
member (path E F) (path n1 n2 :: K1) /\ path_var F

ctxs_member1 < apply IH to H3 H4.
Subgoal 2.2:

Variables: K1 L1 E F
IH : forall X L K, ctxs L K * -> member X L ->
(exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\
path_var F)
H3 : ctxs L1 K1 *
H4 : member (tm (E n1)) L1
H5 : tm_var (E n1)
H6 : member (path (E n1) (F n2)) K1
H7 : path_var (F n2)
============================
exists E1 F, tm (E n1) = tm E1 /\ tm_var E1 /\
member (path E1 F) (path n1 n2 :: K1) /\ path_var F

ctxs_member1 < search.
Proof completed.
Abella < Theorem ctxs_member2 :
forall X L K, ctxs L K -> member X K ->
(exists E F, X = path E F /\ tm_var E /\ path_var F).

============================
forall X L K, ctxs L K -> member X K ->
(exists E F, X = path E F /\ tm_var E /\ path_var F)

ctxs_member2 < induction on 1.

IH : forall X L K, ctxs L K * -> member X K ->
(exists E F, X = path E F /\ tm_var E /\ path_var F)
============================
forall X L K, ctxs L K @ -> member X K ->
(exists E F, X = path E F /\ tm_var E /\ path_var F)

ctxs_member2 < intros.

Variables: X L K
IH : forall X L K, ctxs L K * -> member X K ->
(exists E F, X = path E F /\ tm_var E /\ path_var F)
H1 : ctxs L K @
H2 : member X K
============================
exists E F, X = path E F /\ tm_var E /\ path_var F

ctxs_member2 < case H1.
Subgoal 1:

Variables: X
IH : forall X L K, ctxs L K * -> member X K ->
(exists E F, X = path E F /\ tm_var E /\ path_var F)
H2 : member X nil
============================
exists E F, X = path E F /\ tm_var E /\ path_var F

Subgoal 2 is:
exists E F, X n1 n2 = path E F /\ tm_var E /\ path_var F

ctxs_member2 < case H2.
Subgoal 2:

Variables: X K1 L1
IH : forall X L K, ctxs L K * -> member X K ->
(exists E F, X = path E F /\ tm_var E /\ path_var F)
H2 : member (X n1 n2) (path n1 n2 :: K1)
H3 : ctxs L1 K1 *
============================
exists E F, X n1 n2 = path E F /\ tm_var E /\ path_var F

ctxs_member2 < case H2.
Subgoal 2.1:

Variables: K1 L1
IH : forall X L K, ctxs L K * -> member X K ->
(exists E F, X = path E F /\ tm_var E /\ path_var F)
H3 : ctxs L1 K1 *
============================
exists E F, path n1 n2 = path E F /\ tm_var E /\ path_var F

Subgoal 2.2 is:
exists E F, X n1 n2 = path E F /\ tm_var E /\ path_var F

ctxs_member2 < search.
Subgoal 2.2:

Variables: X K1 L1
IH : forall X L K, ctxs L K * -> member X K ->
(exists E F, X = path E F /\ tm_var E /\ path_var F)
H3 : ctxs L1 K1 *
H4 : member (X n1 n2) K1
============================
exists E F, X n1 n2 = path E F /\ tm_var E /\ path_var F

ctxs_member2 < apply IH to H3 H4.
Subgoal 2.2:

Variables: K1 L1 E F
IH : forall X L K, ctxs L K * -> member X K ->
(exists E F, X = path E F /\ tm_var E /\ path_var F)
H3 : ctxs L1 K1 *
H4 : member (path (E n1) (F n2)) K1
H5 : tm_var (E n1)
H6 : path_var (F n2)
============================
exists E1 F1, path (E n1) (F n2) = path E1 F1 /\ tm_var E1 /\ path_var F1

ctxs_member2 < search.
Proof completed.
Abella < Theorem member_path_unique :
forall L K X Y F, ctxs L K -> member (path X F) K -> member (path Y F) K ->
X =
Y.

============================
forall L K X Y F, ctxs L K -> member (path X F) K -> member (path Y F) K ->
X =
Y

member_path_unique < induction on 2.

IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
============================
forall L K X Y F, ctxs L K -> member (path X F) K @ ->
member (path Y F) K -> X =
Y

member_path_unique < intros.

Variables: L K X Y F
IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
H1 : ctxs L K
H2 : member (path X F) K @
H3 : member (path Y F) K
============================
X = Y

member_path_unique < case H2.
Subgoal 1:

Variables: L X Y F L1
IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
H1 : ctxs L (path X F :: L1)
H3 : member (path Y F) (path X F :: L1)
============================
X = Y

Subgoal 2 is:
X = Y

member_path_unique < case H3.
Subgoal 1.1:

Variables: L X F L1
IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
H1 : ctxs L (path X F :: L1)
============================
X = X

Subgoal 1.2 is:
X = Y

Subgoal 2 is:
X = Y

member_path_unique < search.
Subgoal 1.2:

Variables: L X Y F L1
IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
H1 : ctxs L (path X F :: L1)
H4 : member (path Y F) L1
============================
X = Y

Subgoal 2 is:
X = Y

member_path_unique < case H1.
Subgoal 1.2:

Variables: Y K1 L2
IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
H4 : member (path (Y n1) n2) K1
H5 : ctxs L2 K1
============================
n1 = Y n1

Subgoal 2 is:
X = Y

member_path_unique < apply member_prune_path to H4.
Subgoal 2:

Variables: L X Y F L1 B
IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
H1 : ctxs L (B :: L1)
H3 : member (path Y F) (B :: L1)
H4 : member (path X F) L1 *
============================
X = Y

member_path_unique < case H3.
Subgoal 2.1:

Variables: L X Y F L1
IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
H1 : ctxs L (path Y F :: L1)
H4 : member (path X F) L1 *
============================
X = Y

Subgoal 2.2 is:
X = Y

member_path_unique < case H1.
Subgoal 2.1:

Variables: X K1 L2
IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
H4 : member (path (X n1) n2) K1 *
H5 : ctxs L2 K1
============================
X n1 = n1

Subgoal 2.2 is:
X = Y

member_path_unique < apply member_prune_path to H4.
Subgoal 2.2:

Variables: L X Y F L1 B
IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
H1 : ctxs L (B :: L1)
H4 : member (path X F) L1 *
H5 : member (path Y F) L1
============================
X = Y

member_path_unique < case H1.
Subgoal 2.2:

Variables: X Y F K1 L2
IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
H4 : member (path (X n1) (F n2)) K1 *
H5 : member (path (Y n1) (F n2)) K1
H6 : ctxs L2 K1
============================
X n1 = Y n1

member_path_unique < apply IH to H6 H4 H5.
Subgoal 2.2:

Variables: Y F K1 L2
IH : forall L K X Y F, ctxs L K -> member (path X F) K * ->
member (path Y F) K -> X =
Y
H4 : member (path (Y n1) (F n2)) K1 *
H5 : member (path (Y n1) (F n2)) K1
H6 : ctxs L2 K1
============================
Y n1 = Y n1

member_path_unique < search.
Proof completed.
Abella < Theorem path_exists :
forall L K M, ctxs L K -> {L |- tm M} -> (exists P, {K |- path M P}).

============================
forall L K M, ctxs L K -> {L |- tm M} -> (exists P, {K |- path M P})

path_exists < induction on 2.

IH : forall L K M, ctxs L K -> {L |- tm M}* -> (exists P, {K |- path M P})
============================
forall L K M, ctxs L K -> {L |- tm M}@ -> (exists P, {K |- path M P})

path_exists < intros.

Variables: L K M
IH : forall L K M, ctxs L K -> {L |- tm M}* -> (exists P, {K |- path M P})
H1 : ctxs L K
H2 : {L |- tm M}@
============================
exists P, {K |- path M P}

path_exists < case H2.
Subgoal 1:

Variables: L K N M1
IH : forall L K M, ctxs L K -> {L |- tm M}* -> (exists P, {K |- path M P})
H1 : ctxs L K
H3 : {L |- tm M1}*
H4 : {L |- tm N}*
============================
exists P, {K |- path (app M1 N) P}

Subgoal 2 is:
exists P, {K |- path (abs R) P}

Subgoal 3 is:
exists P, {K |- path M P}

path_exists < apply IH to H1 H3.
Subgoal 1:

Variables: L K N M1 P
IH : forall L K M, ctxs L K -> {L |- tm M}* -> (exists P, {K |- path M P})
H1 : ctxs L K
H3 : {L |- tm M1}*
H4 : {L |- tm N}*
H5 : {K |- path M1 P}
============================
exists P, {K |- path (app M1 N) P}

Subgoal 2 is:
exists P, {K |- path (abs R) P}

Subgoal 3 is:
exists P, {K |- path M P}

path_exists < search.
Subgoal 2:

Variables: L K R
IH : forall L K M, ctxs L K -> {L |- tm M}* -> (exists P, {K |- path M P})
H1 : ctxs L K
H3 : {L, tm n1 |- tm (R n1)}*
============================
exists P, {K |- path (abs R) P}

Subgoal 3 is:
exists P, {K |- path M P}

path_exists < assert ctxs (tm n1 :: L) (path n1 n2 :: K).
Subgoal 2:

Variables: L K R
IH : forall L K M, ctxs L K -> {L |- tm M}* -> (exists P, {K |- path M P})
H1 : ctxs L K
H3 : {L, tm n1 |- tm (R n1)}*
H4 : ctxs (tm n1 :: L) (path n1 n2 :: K)
============================
exists P, {K |- path (abs R) P}

Subgoal 3 is:
exists P, {K |- path M P}

path_exists < apply IH to H4 H3.
Subgoal 2:

Variables: L K R P
IH : forall L K M, ctxs L K -> {L |- tm M}* -> (exists P, {K |- path M P})
H1 : ctxs L K
H3 : {L, tm n1 |- tm (R n1)}*
H4 : ctxs (tm n1 :: L) (path n1 n2 :: K)
H5 : {K, path n1 n2 |- path (R n1) (P n2)}
============================
exists P, {K |- path (abs R) P}

Subgoal 3 is:
exists P, {K |- path M P}

path_exists < search.
Subgoal 3:

Variables: L K M F
IH : forall L K M, ctxs L K -> {L |- tm M}* -> (exists P, {K |- path M P})
H1 : ctxs L K
H3 : {L, [F] |- tm M}*
H4 : member F L
============================
exists P, {K |- path M P}

path_exists < apply ctxs_member1 to H1 H4.
Subgoal 3:

Variables: L K M E F1
IH : forall L K M, ctxs L K -> {L |- tm M}* -> (exists P, {K |- path M P})
H1 : ctxs L K
H3 : {L, [tm E] |- tm M}*
H4 : member (tm E) L
H5 : tm_var E
H6 : member (path E F1) K
H7 : path_var F1
============================
exists P, {K |- path M P}

path_exists < case H3.
Subgoal 3:

Variables: L K M F1
IH : forall L K M, ctxs L K -> {L |- tm M}* -> (exists P, {K |- path M P})
H1 : ctxs L K
H4 : member (tm M) L
H5 : tm_var M
H6 : member (path M F1) K
H7 : path_var F1
============================
exists P, {K |- path M P}

path_exists < search.
Proof completed.
Abella < Theorem path_app :
forall L K M N Y, ctxs L K -> {L |- tm (app M N)} ->
(forall P, {K |- path (app M N) P} -> {K |- path Y P}) ->
(exists YM YN, Y = app YM YN).

============================
forall L K M N Y, ctxs L K -> {L |- tm (app M N)} ->
(forall P, {K |- path (app M N) P} -> {K |- path Y P}) ->
(exists YM YN, Y = app YM YN)

path_app < intros.

Variables: L K M N Y
H1 : ctxs L K
H2 : {L |- tm (app M N)}
H3 : forall P, {K |- path (app M N) P} -> {K |- path Y P}
============================
exists YM YN, Y = app YM YN

path_app < case H2.
Subgoal 1:

Variables: L K M N Y
H1 : ctxs L K
H3 : forall P, {K |- path (app M N) P} -> {K |- path Y P}
H4 : {L |- tm M}
H5 : {L |- tm N}
============================
exists YM YN, Y = app YM YN

Subgoal 2 is:
exists YM YN, Y = app YM YN

path_app < apply path_exists to H1 H4.
Subgoal 1:

Variables: L K M N Y P
H1 : ctxs L K
H3 : forall P, {K |- path (app M N) P} -> {K |- path Y P}
H4 : {L |- tm M}
H5 : {L |- tm N}
H6 : {K |- path M P}
============================
exists YM YN, Y = app YM YN

Subgoal 2 is:
exists YM YN, Y = app YM YN

path_app < assert {K |- path (app M N) (left P)}.
Subgoal 1:

Variables: L K M N Y P
H1 : ctxs L K
H3 : forall P, {K |- path (app M N) P} -> {K |- path Y P}
H4 : {L |- tm M}
H5 : {L |- tm N}
H6 : {K |- path M P}
H7 : {K |- path (app M N) (left P)}
============================
exists YM YN, Y = app YM YN

Subgoal 2 is:
exists YM YN, Y = app YM YN

path_app < apply H3 to H7.
Subgoal 1:

Variables: L K M N Y P
H1 : ctxs L K
H3 : forall P, {K |- path (app M N) P} -> {K |- path Y P}
H4 : {L |- tm M}
H5 : {L |- tm N}
H6 : {K |- path M P}
H7 : {K |- path (app M N) (left P)}
H8 : {K |- path Y (left P)}
============================
exists YM YN, Y = app YM YN

Subgoal 2 is:
exists YM YN, Y = app YM YN

path_app < case H8.
Subgoal 1.1:

Variables: L K M N P M1 N1
H1 : ctxs L K
H3 : forall P, {K |- path (app M N) P} -> {K |- path (app M1 N1) P}
H4 : {L |- tm M}
H5 : {L |- tm N}
H6 : {K |- path M P}
H7 : {K |- path (app M N) (left P)}
H9 : {K |- path M1 P}
============================
exists YM YN, app M1 N1 = app YM YN

Subgoal 1.2 is:
exists YM YN, Y = app YM YN

Subgoal 2 is:
exists YM YN, Y = app YM YN

path_app < search.
Subgoal 1.2:

Variables: L K M N Y P F
H1 : ctxs L K
H3 : forall P, {K |- path (app M N) P} -> {K |- path Y P}
H4 : {L |- tm M}
H5 : {L |- tm N}
H6 : {K |- path M P}
H7 : {K |- path (app M N) (left P)}
H9 : {K, [F] |- path Y (left P)}
H10 : member F K
============================
exists YM YN, Y = app YM YN

Subgoal 2 is:
exists YM YN, Y = app YM YN

path_app < apply ctxs_member2 to H1 H10.
Subgoal 1.2:

Variables: L K M N Y P E F1
H1 : ctxs L K
H3 : forall P, {K |- path (app M N) P} -> {K |- path Y P}
H4 : {L |- tm M}
H5 : {L |- tm N}
H6 : {K |- path M P}
H7 : {K |- path (app M N) (left P)}
H9 : {K, [path E F1] |- path Y (left P)}
H10 : member (path E F1) K
H11 : tm_var E
H12 : path_var F1
============================
exists YM YN, Y = app YM YN

Subgoal 2 is:
exists YM YN, Y = app YM YN

path_app < case H12.
Subgoal 1.2:

Variables: L K M N Y P E
H1 : ctxs (L n1) (K n1)
H3 : forall P, {K n1 |- path (app M N) P} -> {K n1 |- path Y P}
H4 : {L n1 |- tm M}
H5 : {L n1 |- tm N}
H6 : {K n1 |- path M (P n1)}
H7 : {K n1 |- path (app M N) (left (P n1))}
H9 : {K n1, [path E n1] |- path Y (left (P n1))}
H10 : member (path E n1) (K n1)
H11 : tm_var E
============================
exists YM YN, Y = app YM YN

Subgoal 2 is:
exists YM YN, Y = app YM YN

path_app < case H9.
Subgoal 2:

Variables: L K M N Y F
H1 : ctxs L K
H3 : forall P, {K |- path (app M N) P} -> {K |- path Y P}
H4 : {L, [F] |- tm (app M N)}
H5 : member F L
============================
exists YM YN, Y = app YM YN

path_app < apply ctxs_member1 to H1 H5.
Subgoal 2:

Variables: L K M N Y E F1
H1 : ctxs L K
H3 : forall P, {K |- path (app M N) P} -> {K |- path Y P}
H4 : {L, [tm E] |- tm (app M N)}
H5 : member (tm E) L
H6 : tm_var E
H7 : member (path E F1) K
H8 : path_var F1
============================
exists YM YN, Y = app YM YN

path_app < case H4.
Subgoal 2:

Variables: L K M N Y F1
H1 : ctxs L K
H3 : forall P, {K |- path (app M N) P} -> {K |- path Y P}
H5 : member (tm (app M N)) L
H6 : tm_var (app M N)
H7 : member (path (app M N) F1) K
H8 : path_var F1
============================
exists YM YN, Y = app YM YN

path_app < case H6.
Proof completed.
Abella < Theorem path_abs :
forall L K R Y, ctxs L K -> {L |- tm (abs R)} ->
(forall P, {K |- path (abs R) P} -> {K |- path Y P}) ->
(exists YR, Y = abs YR).

============================
forall L K R Y, ctxs L K -> {L |- tm (abs R)} ->
(forall P, {K |- path (abs R) P} -> {K |- path Y P}) ->
(exists YR, Y = abs YR)

path_abs < intros.

Variables: L K R Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
============================
exists YR, Y = abs YR

path_abs < case H2.
Subgoal 1:

Variables: L K R Y
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H4 : {L, tm n1 |- tm (R n1)}
============================
exists YR, Y = abs YR

Subgoal 2 is:
exists YR, Y = abs YR

path_abs < assert ctxs (tm n1 :: L) (path n1 n2 :: K).
Subgoal 1:

Variables: L K R Y
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H4 : {L, tm n1 |- tm (R n1)}
H5 : ctxs (tm n1 :: L) (path n1 n2 :: K)
============================
exists YR, Y = abs YR

Subgoal 2 is:
exists YR, Y = abs YR

path_abs < apply path_exists to H5 H4.
Subgoal 1:

Variables: L K R Y P
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H4 : {L, tm n1 |- tm (R n1)}
H5 : ctxs (tm n1 :: L) (path n1 n2 :: K)
H6 : {K, path n1 n2 |- path (R n1) (P n2)}
============================
exists YR, Y = abs YR

Subgoal 2 is:
exists YR, Y = abs YR

path_abs < assert {K |- path (abs R) (bnd P)}.
Subgoal 1:

Variables: L K R Y P
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H4 : {L, tm n1 |- tm (R n1)}
H5 : ctxs (tm n1 :: L) (path n1 n2 :: K)
H6 : {K, path n1 n2 |- path (R n1) (P n2)}
H7 : {K |- path (abs R) (bnd P)}
============================
exists YR, Y = abs YR

Subgoal 2 is:
exists YR, Y = abs YR

path_abs < apply H3 to H7.
Subgoal 1:

Variables: L K R Y P
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H4 : {L, tm n1 |- tm (R n1)}
H5 : ctxs (tm n1 :: L) (path n1 n2 :: K)
H6 : {K, path n1 n2 |- path (R n1) (P n2)}
H7 : {K |- path (abs R) (bnd P)}
H8 : {K |- path Y (bnd P)}
============================
exists YR, Y = abs YR

Subgoal 2 is:
exists YR, Y = abs YR

path_abs < case H8.
Subgoal 1.1:

Variables: L K R P R1
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path (abs R1) P}
H4 : {L, tm n1 |- tm (R n1)}
H5 : ctxs (tm n1 :: L) (path n1 n2 :: K)
H6 : {K, path n1 n2 |- path (R n1) (P n2)}
H7 : {K |- path (abs R) (bnd P)}
H9 : {K, path n1 n2 |- path (R1 n1) (P n2)}
============================
exists YR, abs R1 = abs YR

Subgoal 1.2 is:
exists YR, Y = abs YR

Subgoal 2 is:
exists YR, Y = abs YR

path_abs < search.
Subgoal 1.2:

Variables: L K R Y P F
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H4 : {L, tm n1 |- tm (R n1)}
H5 : ctxs (tm n1 :: L) (path n1 n2 :: K)
H6 : {K, path n1 n2 |- path (R n1) (P n2)}
H7 : {K |- path (abs R) (bnd P)}
H9 : {K, [F] |- path Y (bnd P)}
H10 : member F K
============================
exists YR, Y = abs YR

Subgoal 2 is:
exists YR, Y = abs YR

path_abs < apply ctxs_member2 to H1 H10.
Subgoal 1.2:

Variables: L K R Y P E F1
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H4 : {L, tm n1 |- tm (R n1)}
H5 : ctxs (tm n1 :: L) (path n1 n2 :: K)
H6 : {K, path n1 n2 |- path (R n1) (P n2)}
H7 : {K |- path (abs R) (bnd P)}
H9 : {K, [path E F1] |- path Y (bnd P)}
H10 : member (path E F1) K
H11 : tm_var E
H12 : path_var F1
============================
exists YR, Y = abs YR

Subgoal 2 is:
exists YR, Y = abs YR

path_abs < case H9.
Subgoal 1.2:

Variables: L K R Y P
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H4 : {L, tm n1 |- tm (R n1)}
H5 : ctxs (tm n1 :: L) (path n1 n2 :: K)
H6 : {K, path n1 n2 |- path (R n1) (P n2)}
H7 : {K |- path (abs R) (bnd P)}
H10 : member (path Y (bnd P)) K
H11 : tm_var Y
H12 : path_var (bnd P)
============================
exists YR, Y = abs YR

Subgoal 2 is:
exists YR, Y = abs YR

path_abs < case H12.
Subgoal 2:

Variables: L K R Y F
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H4 : {L, [F] |- tm (abs R)}
H5 : member F L
============================
exists YR, Y = abs YR

path_abs < apply ctxs_member1 to H1 H5.
Subgoal 2:

Variables: L K R Y E F1
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H4 : {L, [tm E] |- tm (abs R)}
H5 : member (tm E) L
H6 : tm_var E
H7 : member (path E F1) K
H8 : path_var F1
============================
exists YR, Y = abs YR

path_abs < case H4.
Subgoal 2:

Variables: L K R Y F1
H1 : ctxs L K
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H5 : member (tm (abs R)) L
H6 : tm_var (abs R)
H7 : member (path (abs R) F1) K
H8 : path_var F1
============================
exists YR, Y = abs YR

path_abs < case H6.
Proof completed.
Abella < Theorem path_equal :
forall L K X Y, ctxs L K -> {L |- tm X} ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y.

============================
forall L K X Y, ctxs L K -> {L |- tm X} ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y

path_equal < induction on 2.

IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
============================
forall L K X Y, ctxs L K -> {L |- tm X}@ ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y

path_equal < intros.

Variables: L K X Y
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm X}@
H3 : forall P, {K |- path X P} -> {K |- path Y P}
============================
X = Y

path_equal < case H2 (keep).
Subgoal 1:

Variables: L K Y N M
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app M N)}@
H3 : forall P, {K |- path (app M N) P} -> {K |- path Y P}
H4 : {L |- tm M}*
H5 : {L |- tm N}*
============================
app M N = Y

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < apply path_app to H1 H2 H3.
Subgoal 1:

Variables: L K N M YM YN
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app M N)}@
H3 : forall P, {K |- path (app M N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm M}*
H5 : {L |- tm N}*
============================
app M N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < assert forall P, {K |- path M P} -> {K |- path YM P}.
Subgoal 1.1:

Variables: L K N M YM YN
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app M N)}@
H3 : forall P, {K |- path (app M N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm M}*
H5 : {L |- tm N}*
============================
forall P, {K |- path M P} -> {K |- path YM P}

Subgoal 1 is:
app M N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < intros.
Subgoal 1.1:

Variables: L K N M YM YN P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app M N)}@
H3 : forall P, {K |- path (app M N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm M}*
H5 : {L |- tm N}*
H6 : {K |- path M P}
============================
{K |- path YM P}

Subgoal 1 is:
app M N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < assert {K |- path (app M N) (left P)}.
Subgoal 1.1:

Variables: L K N M YM YN P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app M N)}@
H3 : forall P, {K |- path (app M N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm M}*
H5 : {L |- tm N}*
H6 : {K |- path M P}
H7 : {K |- path (app M N) (left P)}
============================
{K |- path YM P}

Subgoal 1 is:
app M N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < apply H3 to H7.
Subgoal 1.1:

Variables: L K N M YM YN P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app M N)}@
H3 : forall P, {K |- path (app M N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm M}*
H5 : {L |- tm N}*
H6 : {K |- path M P}
H7 : {K |- path (app M N) (left P)}
H8 : {K |- path (app YM YN) (left P)}
============================
{K |- path YM P}

Subgoal 1 is:
app M N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < case H8.
Subgoal 1.1.1:

Variables: L K N M YM YN P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app M N)}@
H3 : forall P, {K |- path (app M N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm M}*
H5 : {L |- tm N}*
H6 : {K |- path M P}
H7 : {K |- path (app M N) (left P)}
H9 : {K |- path YM P}
============================
{K |- path YM P}

Subgoal 1.1.2 is:
{K |- path YM P}

Subgoal 1 is:
app M N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < search.
Subgoal 1.1.2:

Variables: L K N M YM YN P F
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app M N)}@
H3 : forall P, {K |- path (app M N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm M}*
H5 : {L |- tm N}*
H6 : {K |- path M P}
H7 : {K |- path (app M N) (left P)}
H9 : {K, [F] |- path (app YM YN) (left P)}
H10 : member F K
============================
{K |- path YM P}

Subgoal 1 is:
app M N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < apply ctxs_member2 to H1 H10.
Subgoal 1.1.2:

Variables: L K N M YM YN P E F1
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app M N)}@
H3 : forall P, {K |- path (app M N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm M}*
H5 : {L |- tm N}*
H6 : {K |- path M P}
H7 : {K |- path (app M N) (left P)}
H9 : {K, [path E F1] |- path (app YM YN) (left P)}
H10 : member (path E F1) K
H11 : tm_var E
H12 : path_var F1
============================
{K |- path YM P}

Subgoal 1 is:
app M N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < case H12.
Subgoal 1.1.2:

Variables: L K N M YM YN P E
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs (L n1) (K n1)
H2 : {L n1 |- tm (app M N)}@
H3 : forall P, {K n1 |- path (app M N) P} -> {K n1 |- path (app YM YN) P}
H4 : {L n1 |- tm M}*
H5 : {L n1 |- tm N}*
H6 : {K n1 |- path M (P n1)}
H7 : {K n1 |- path (app M N) (left (P n1))}
H9 : {K n1, [path E n1] |- path (app YM YN) (left (P n1))}
H10 : member (path E n1) (K n1)
H11 : tm_var E
============================
{K n1 |- path YM (P n1)}

Subgoal 1 is:
app M N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < case H9.
Subgoal 1:

Variables: L K N M YM YN
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app M N)}@
H3 : forall P, {K |- path (app M N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm M}*
H5 : {L |- tm N}*
H6 : forall P, {K |- path M P} -> {K |- path YM P}
============================
app M N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < apply IH to H1 H4 H6.
Subgoal 1:

Variables: L K N YM YN
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app YM N)}@
H3 : forall P, {K |- path (app YM N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm YM}*
H5 : {L |- tm N}*
H6 : forall P, {K |- path YM P} -> {K |- path YM P}
============================
app YM N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < assert forall P, {K |- path N P} -> {K |- path YN P}.
Subgoal 1.2:

Variables: L K N YM YN
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app YM N)}@
H3 : forall P, {K |- path (app YM N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm YM}*
H5 : {L |- tm N}*
H6 : forall P, {K |- path YM P} -> {K |- path YM P}
============================
forall P, {K |- path N P} -> {K |- path YN P}

Subgoal 1 is:
app YM N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < intros.
Subgoal 1.2:

Variables: L K N YM YN P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app YM N)}@
H3 : forall P, {K |- path (app YM N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm YM}*
H5 : {L |- tm N}*
H6 : forall P, {K |- path YM P} -> {K |- path YM P}
H7 : {K |- path N P}
============================
{K |- path YN P}

Subgoal 1 is:
app YM N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < assert {K |- path (app M N) (right P)}.
Subgoal 1.2:

Variables: L K N YM YN P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app YM N)}@
H3 : forall P, {K |- path (app YM N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm YM}*
H5 : {L |- tm N}*
H6 : forall P, {K |- path YM P} -> {K |- path YM P}
H7 : {K |- path N P}
H8 : {K |- path (app YM N) (right P)}
============================
{K |- path YN P}

Subgoal 1 is:
app YM N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < apply H3 to H8.
Subgoal 1.2:

Variables: L K N YM YN P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app YM N)}@
H3 : forall P, {K |- path (app YM N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm YM}*
H5 : {L |- tm N}*
H6 : forall P, {K |- path YM P} -> {K |- path YM P}
H7 : {K |- path N P}
H8 : {K |- path (app YM N) (right P)}
H9 : {K |- path (app YM YN) (right P)}
============================
{K |- path YN P}

Subgoal 1 is:
app YM N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < case H9.
Subgoal 1.2.1:

Variables: L K N YM YN P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app YM N)}@
H3 : forall P, {K |- path (app YM N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm YM}*
H5 : {L |- tm N}*
H6 : forall P, {K |- path YM P} -> {K |- path YM P}
H7 : {K |- path N P}
H8 : {K |- path (app YM N) (right P)}
H10 : {K |- path YN P}
============================
{K |- path YN P}

Subgoal 1.2.2 is:
{K |- path YN P}

Subgoal 1 is:
app YM N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < search.
Subgoal 1.2.2:

Variables: L K N YM YN P F
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app YM N)}@
H3 : forall P, {K |- path (app YM N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm YM}*
H5 : {L |- tm N}*
H6 : forall P, {K |- path YM P} -> {K |- path YM P}
H7 : {K |- path N P}
H8 : {K |- path (app YM N) (right P)}
H10 : {K, [F] |- path (app YM YN) (right P)}
H11 : member F K
============================
{K |- path YN P}

Subgoal 1 is:
app YM N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < apply ctxs_member2 to H1 H11.
Subgoal 1.2.2:

Variables: L K N YM YN P E F1
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app YM N)}@
H3 : forall P, {K |- path (app YM N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm YM}*
H5 : {L |- tm N}*
H6 : forall P, {K |- path YM P} -> {K |- path YM P}
H7 : {K |- path N P}
H8 : {K |- path (app YM N) (right P)}
H10 : {K, [path E F1] |- path (app YM YN) (right P)}
H11 : member (path E F1) K
H12 : tm_var E
H13 : path_var F1
============================
{K |- path YN P}

Subgoal 1 is:
app YM N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < case H13.
Subgoal 1.2.2:

Variables: L K N YM YN P E
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs (L n1) (K n1)
H2 : {L n1 |- tm (app YM N)}@
H3 : forall P, {K n1 |- path (app YM N) P} -> {K n1 |- path (app YM YN) P}
H4 : {L n1 |- tm YM}*
H5 : {L n1 |- tm N}*
H6 : forall P, {K n1 |- path YM P} -> {K n1 |- path YM P}
H7 : {K n1 |- path N (P n1)}
H8 : {K n1 |- path (app YM N) (right (P n1))}
H10 : {K n1, [path E n1] |- path (app YM YN) (right (P n1))}
H11 : member (path E n1) (K n1)
H12 : tm_var E
============================
{K n1 |- path YN (P n1)}

Subgoal 1 is:
app YM N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < case H10.
Subgoal 1:

Variables: L K N YM YN
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app YM N)}@
H3 : forall P, {K |- path (app YM N) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm YM}*
H5 : {L |- tm N}*
H6 : forall P, {K |- path YM P} -> {K |- path YM P}
H7 : forall P, {K |- path N P} -> {K |- path YN P}
============================
app YM N = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < apply IH to H1 H5 H7.
Subgoal 1:

Variables: L K YM YN
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (app YM YN)}@
H3 : forall P, {K |- path (app YM YN) P} -> {K |- path (app YM YN) P}
H4 : {L |- tm YM}*
H5 : {L |- tm YN}*
H6 : forall P, {K |- path YM P} -> {K |- path YM P}
H7 : forall P, {K |- path YN P} -> {K |- path YN P}
============================
app YM YN = app YM YN

Subgoal 2 is:
abs R = Y

Subgoal 3 is:
X = Y

path_equal < search.
Subgoal 2:

Variables: L K Y R
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}@
H3 : forall P, {K |- path (abs R) P} -> {K |- path Y P}
H4 : {L, tm n1 |- tm (R n1)}*
============================
abs R = Y

Subgoal 3 is:
X = Y

path_equal < apply path_abs to H1 H2 H3.
Subgoal 2:

Variables: L K R YR
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}@
H3 : forall P, {K |- path (abs R) P} -> {K |- path (abs YR) P}
H4 : {L, tm n1 |- tm (R n1)}*
============================
abs R = abs YR

Subgoal 3 is:
X = Y

path_equal < assert forall P, {K, path n1 n2 |- path (R n1) P} ->
{K, path n1 n2 |- path (YR n1) P}.
Subgoal 2.1:

Variables: L K R YR
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}@
H3 : forall P, {K |- path (abs R) P} -> {K |- path (abs YR) P}
H4 : {L, tm n1 |- tm (R n1)}*
============================
forall P, {K, path n1 n2 |- path (R n1) P} ->
{K, path n1 n2 |- path (YR n1) P}

Subgoal 2 is:
abs R = abs YR

Subgoal 3 is:
X = Y

path_equal < intros.
Subgoal 2.1:

Variables: L K R YR P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}@
H3 : forall P, {K |- path (abs R) P} -> {K |- path (abs YR) P}
H4 : {L, tm n1 |- tm (R n1)}*
H5 : {K, path n1 n2 |- path (R n1) (P n2)}
============================
{K, path n1 n2 |- path (YR n1) (P n2)}

Subgoal 2 is:
abs R = abs YR

Subgoal 3 is:
X = Y

path_equal < assert {K |- path (abs R) (bnd P)}.
Subgoal 2.1:

Variables: L K R YR P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}@
H3 : forall P, {K |- path (abs R) P} -> {K |- path (abs YR) P}
H4 : {L, tm n1 |- tm (R n1)}*
H5 : {K, path n1 n2 |- path (R n1) (P n2)}
H6 : {K |- path (abs R) (bnd P)}
============================
{K, path n1 n2 |- path (YR n1) (P n2)}

Subgoal 2 is:
abs R = abs YR

Subgoal 3 is:
X = Y

path_equal < apply H3 to H6.
Subgoal 2.1:

Variables: L K R YR P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}@
H3 : forall P, {K |- path (abs R) P} -> {K |- path (abs YR) P}
H4 : {L, tm n1 |- tm (R n1)}*
H5 : {K, path n1 n2 |- path (R n1) (P n2)}
H6 : {K |- path (abs R) (bnd P)}
H7 : {K |- path (abs YR) (bnd P)}
============================
{K, path n1 n2 |- path (YR n1) (P n2)}

Subgoal 2 is:
abs R = abs YR

Subgoal 3 is:
X = Y

path_equal < case H7.
Subgoal 2.1.1:

Variables: L K R YR P
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}@
H3 : forall P, {K |- path (abs R) P} -> {K |- path (abs YR) P}
H4 : {L, tm n1 |- tm (R n1)}*
H5 : {K, path n1 n2 |- path (R n1) (P n2)}
H6 : {K |- path (abs R) (bnd P)}
H8 : {K, path n1 n2 |- path (YR n1) (P n2)}
============================
{K, path n1 n2 |- path (YR n1) (P n2)}

Subgoal 2.1.2 is:
{K, path n1 n2 |- path (YR n1) (P n2)}

Subgoal 2 is:
abs R = abs YR

Subgoal 3 is:
X = Y

path_equal < search.
Subgoal 2.1.2:

Variables: L K R YR P F
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}@
H3 : forall P, {K |- path (abs R) P} -> {K |- path (abs YR) P}
H4 : {L, tm n1 |- tm (R n1)}*
H5 : {K, path n1 n2 |- path (R n1) (P n2)}
H6 : {K |- path (abs R) (bnd P)}
H8 : {K, [F] |- path (abs YR) (bnd P)}
H9 : member F K
============================
{K, path n1 n2 |- path (YR n1) (P n2)}

Subgoal 2 is:
abs R = abs YR

Subgoal 3 is:
X = Y

path_equal < apply ctxs_member2 to H1 H9.
Subgoal 2.1.2:

Variables: L K R YR P E F1
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}@
H3 : forall P, {K |- path (abs R) P} -> {K |- path (abs YR) P}
H4 : {L, tm n1 |- tm (R n1)}*
H5 : {K, path n1 n2 |- path (R n1) (P n2)}
H6 : {K |- path (abs R) (bnd P)}
H8 : {K, [path E F1] |- path (abs YR) (bnd P)}
H9 : member (path E F1) K
H10 : tm_var E
H11 : path_var F1
============================
{K, path n1 n2 |- path (YR n1) (P n2)}

Subgoal 2 is:
abs R = abs YR

Subgoal 3 is:
X = Y

path_equal < case H11.
Subgoal 2.1.2:

Variables: L K R YR P E
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs (L n3) (K n3)
H2 : {L n3 |- tm (abs R)}@
H3 : forall P, {K n3 |- path (abs R) P} -> {K n3 |- path (abs YR) P}
H4 : {L n3, tm n1 |- tm (R n1)}*
H5 : {K n3, path n1 n2 |- path (R n1) (P n3 n2)}
H6 : {K n3 |- path (abs R) (bnd (P n3))}
H8 : {K n3, [path E n3] |- path (abs YR) (bnd (P n3))}
H9 : member (path E n3) (K n3)
H10 : tm_var E
============================
{K n3, path n1 n2 |- path (YR n1) (P n3 n2)}

Subgoal 2 is:
abs R = abs YR

Subgoal 3 is:
X = Y

path_equal < case H8.
Subgoal 2:

Variables: L K R YR
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}@
H3 : forall P, {K |- path (abs R) P} -> {K |- path (abs YR) P}
H4 : {L, tm n1 |- tm (R n1)}*
H5 : forall P, {K, path n1 n2 |- path (R n1) P} ->
{K, path n1 n2 |- path (YR n1) P}
============================
abs R = abs YR

Subgoal 3 is:
X = Y

path_equal < assert ctxs (tm n1 :: L) (path n1 n2 :: K).
Subgoal 2:

Variables: L K R YR
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs R)}@
H3 : forall P, {K |- path (abs R) P} -> {K |- path (abs YR) P}
H4 : {L, tm n1 |- tm (R n1)}*
H5 : forall P, {K, path n1 n2 |- path (R n1) P} ->
{K, path n1 n2 |- path (YR n1) P}
H6 : ctxs (tm n1 :: L) (path n1 n2 :: K)
============================
abs R = abs YR

Subgoal 3 is:
X = Y

path_equal < apply IH to H6 H4 H5.
Subgoal 2:

Variables: L K YR
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm (abs (z1\YR z1))}@
H3 : forall P, {K |- path (abs (z1\YR z1)) P} -> {K |- path (abs YR) P}
H4 : {L, tm n1 |- tm (YR n1)}*
H5 : forall P, {K, path n1 n2 |- path (YR n1) P} ->
{K, path n1 n2 |- path (YR n1) P}
H6 : ctxs (tm n1 :: L) (path n1 n2 :: K)
============================
abs (z1\YR z1) = abs YR

Subgoal 3 is:
X = Y

path_equal < search.
Subgoal 3:

Variables: L K X Y F
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm X}@
H3 : forall P, {K |- path X P} -> {K |- path Y P}
H4 : {L, [F] |- tm X}*
H5 : member F L
============================
X = Y

path_equal < apply ctxs_member1 to H1 H5.
Subgoal 3:

Variables: L K X Y E F1
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm X}@
H3 : forall P, {K |- path X P} -> {K |- path Y P}
H4 : {L, [tm E] |- tm X}*
H5 : member (tm E) L
H6 : tm_var E
H7 : member (path E F1) K
H8 : path_var F1
============================
X = Y

path_equal < case H4.
Subgoal 3:

Variables: L K X Y F1
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm X}@
H3 : forall P, {K |- path X P} -> {K |- path Y P}
H5 : member (tm X) L
H6 : tm_var X
H7 : member (path X F1) K
H8 : path_var F1
============================
X = Y

path_equal < assert {K |- path X F1}.
Subgoal 3:

Variables: L K X Y F1
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm X}@
H3 : forall P, {K |- path X P} -> {K |- path Y P}
H5 : member (tm X) L
H6 : tm_var X
H7 : member (path X F1) K
H8 : path_var F1
H9 : {K |- path X F1}
============================
X = Y

path_equal < apply H3 to H9.
Subgoal 3:

Variables: L K X Y F1
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs L K
H2 : {L |- tm X}@
H3 : forall P, {K |- path X P} -> {K |- path Y P}
H5 : member (tm X) L
H6 : tm_var X
H7 : member (path X F1) K
H8 : path_var F1
H9 : {K |- path X F1}
H10 : {K |- path Y F1}
============================
X = Y

path_equal < case H8.
Subgoal 3:

Variables: L K X Y
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs (L n1) (K n1)
H2 : {L n1 |- tm X}@
H3 : forall P, {K n1 |- path X P} -> {K n1 |- path Y P}
H5 : member (tm X) (L n1)
H6 : tm_var X
H7 : member (path X n1) (K n1)
H9 : {K n1 |- path X n1}
H10 : {K n1 |- path Y n1}
============================
X = Y

path_equal < case H10.
Subgoal 3:

Variables: L K X Y F2
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs (L n1) (K n1)
H2 : {L n1 |- tm X}@
H3 : forall P, {K n1 |- path X P} -> {K n1 |- path Y P}
H5 : member (tm X) (L n1)
H6 : tm_var X
H7 : member (path X n1) (K n1)
H9 : {K n1 |- path X n1}
H11 : {K n1, [F2 n1] |- path Y n1}
H12 : member (F2 n1) (K n1)
============================
X = Y

path_equal < apply ctxs_member2 to H1 H12.
Subgoal 3:

Variables: L K X Y E1 F3
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs (L n1) (K n1)
H2 : {L n1 |- tm X}@
H3 : forall P, {K n1 |- path X P} -> {K n1 |- path Y P}
H5 : member (tm X) (L n1)
H6 : tm_var X
H7 : member (path X n1) (K n1)
H9 : {K n1 |- path X n1}
H11 : {K n1, [path E1 (F3 n1)] |- path Y n1}
H12 : member (path E1 (F3 n1)) (K n1)
H13 : tm_var E1
H14 : path_var (F3 n1)
============================
X = Y

path_equal < case H11.
Subgoal 3:

Variables: L K X Y
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs (L n1) (K n1)
H2 : {L n1 |- tm X}@
H3 : forall P, {K n1 |- path X P} -> {K n1 |- path Y P}
H5 : member (tm X) (L n1)
H6 : tm_var X
H7 : member (path X n1) (K n1)
H9 : {K n1 |- path X n1}
H12 : member (path Y n1) (K n1)
H13 : tm_var Y
H14 : path_var n1
============================
X = Y

path_equal < apply member_path_unique to H1 H7 H12.
Subgoal 3:

Variables: L K Y
IH : forall L K X Y, ctxs L K -> {L |- tm X}* ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X =
Y
H1 : ctxs (L n1) (K n1)
H2 : {L n1 |- tm Y}@
H3 : forall P, {K n1 |- path Y P} -> {K n1 |- path Y P}
H5 : member (tm Y) (L n1)
H6 : tm_var Y
H7 : member (path Y n1) (K n1)
H9 : {K n1 |- path Y n1}
H12 : member (path Y n1) (K n1)
H13 : tm_var Y
H14 : path_var n1
============================
Y = Y

path_equal < search.
Proof completed.
Abella <