Welcome to Abella 2.0.5-dev.

Abella <Specification "copy".Reading specification "copy".

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

============================ forall L E, nabla x, member (E x) L -> (exists F, E = y\F) member_fresh <induction on 1.

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

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

Subgoal 1: Variables: L3 L2 IH : forall L E, 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_fresh <search.

Subgoal 2: Variables: E L3 L2 IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F) H2 : member (E n1) L3 * ============================ exists F, E = y\F member_fresh <apply IH to H2.

Subgoal 2: Variables: L3 L2 F IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F) H2 : member F L3 * ============================ exists F1, z1\F = y\F1 member_fresh <search.Proof completed.

Abella <Define ctxs : olist -> olist -> prop by ctxs nil nil; ctxs (copy X Y :: L1) (copy2 X Y :: L2) := ctxs L1 L2.

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

Abella <Theorem ctx_mem1 : forall F L1 L2, ctxs L1 L2 -> member F L1 -> (exists X Y, F = copy X Y).

============================ forall F L1 L2, ctxs L1 L2 -> member F L1 -> (exists X Y, F = copy X Y) ctx_mem1 <induction on 1.

IH : forall F L1 L2, ctxs L1 L2 * -> member F L1 -> (exists X Y, F = copy X Y) ============================ forall F L1 L2, ctxs L1 L2 @ -> member F L1 -> (exists X Y, F = copy X Y) ctx_mem1 <intros.

Variables: F L1 L2 IH : forall F L1 L2, ctxs L1 L2 * -> member F L1 -> (exists X Y, F = copy X Y) H1 : ctxs L1 L2 @ H2 : member F L1 ============================ exists X Y, F = copy X Y ctx_mem1 <case H1.

Subgoal 1: Variables: F IH : forall F L1 L2, ctxs L1 L2 * -> member F L1 -> (exists X Y, F = copy X Y) H2 : member F nil ============================ exists X Y, F = copy X Y Subgoal 2 is: exists X Y, F = copy X Y ctx_mem1 <case H2.

Subgoal 2: Variables: F L4 Y X L3 IH : forall F L1 L2, ctxs L1 L2 * -> member F L1 -> (exists X Y, F = copy X Y) H2 : member F (copy X Y :: L3) H3 : ctxs L3 L4 * ============================ exists X Y, F = copy X Y ctx_mem1 <case H2.

Subgoal 2.1: Variables: L4 Y X L3 IH : forall F L1 L2, ctxs L1 L2 * -> member F L1 -> (exists X Y, F = copy X Y) H3 : ctxs L3 L4 * ============================ exists X1 Y1, copy X Y = copy X1 Y1 Subgoal 2.2 is: exists X Y, F = copy X Y ctx_mem1 <search.

Subgoal 2.2: Variables: F L4 Y X L3 IH : forall F L1 L2, ctxs L1 L2 * -> member F L1 -> (exists X Y, F = copy X Y) H3 : ctxs L3 L4 * H4 : member F L3 ============================ exists X Y, F = copy X Y ctx_mem1 <apply IH to H3 H4.

Subgoal 2.2: Variables: L4 Y X L3 X1 Y1 IH : forall F L1 L2, ctxs L1 L2 * -> member F L1 -> (exists X Y, F = copy X Y) H3 : ctxs L3 L4 * H4 : member (copy X1 Y1) L3 ============================ exists X Y, copy X1 Y1 = copy X Y ctx_mem1 <search.Proof completed.

Abella <Theorem ctx_mem2 : forall F L1 L2, ctxs L1 L2 -> member F L2 -> (exists X Y, F = copy2 X Y).

============================ forall F L1 L2, ctxs L1 L2 -> member F L2 -> (exists X Y, F = copy2 X Y) ctx_mem2 <induction on 1.

IH : forall F L1 L2, ctxs L1 L2 * -> member F L2 -> (exists X Y, F = copy2 X Y) ============================ forall F L1 L2, ctxs L1 L2 @ -> member F L2 -> (exists X Y, F = copy2 X Y) ctx_mem2 <intros.

Variables: F L1 L2 IH : forall F L1 L2, ctxs L1 L2 * -> member F L2 -> (exists X Y, F = copy2 X Y) H1 : ctxs L1 L2 @ H2 : member F L2 ============================ exists X Y, F = copy2 X Y ctx_mem2 <case H1.

Subgoal 1: Variables: F IH : forall F L1 L2, ctxs L1 L2 * -> member F L2 -> (exists X Y, F = copy2 X Y) H2 : member F nil ============================ exists X Y, F = copy2 X Y Subgoal 2 is: exists X Y, F = copy2 X Y ctx_mem2 <case H2.

Subgoal 2: Variables: F L4 Y X L3 IH : forall F L1 L2, ctxs L1 L2 * -> member F L2 -> (exists X Y, F = copy2 X Y) H2 : member F (copy2 X Y :: L4) H3 : ctxs L3 L4 * ============================ exists X Y, F = copy2 X Y ctx_mem2 <case H2.

Subgoal 2.1: Variables: L4 Y X L3 IH : forall F L1 L2, ctxs L1 L2 * -> member F L2 -> (exists X Y, F = copy2 X Y) H3 : ctxs L3 L4 * ============================ exists X1 Y1, copy2 X Y = copy2 X1 Y1 Subgoal 2.2 is: exists X Y, F = copy2 X Y ctx_mem2 <search.

Subgoal 2.2: Variables: F L4 Y X L3 IH : forall F L1 L2, ctxs L1 L2 * -> member F L2 -> (exists X Y, F = copy2 X Y) H3 : ctxs L3 L4 * H4 : member F L4 ============================ exists X Y, F = copy2 X Y ctx_mem2 <apply IH to H3 H4.

Subgoal 2.2: Variables: L4 Y X L3 X1 Y1 IH : forall F L1 L2, ctxs L1 L2 * -> member F L2 -> (exists X Y, F = copy2 X Y) H3 : ctxs L3 L4 * H4 : member (copy2 X1 Y1) L4 ============================ exists X Y, copy2 X1 Y1 = copy2 X Y ctx_mem2 <search.Proof completed.

Abella <Theorem copy2_align : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)} -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}).

============================ forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)} -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) copy2_align <induction on 2.

IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) ============================ forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}@ -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) copy2_align <intros.

Variables: M N K L IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H2 : {L, copy2 n1 n1 |- copy2 (M n1) (N n1)}@ ============================ {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <case H2.

Subgoal 1: Variables: K L Q M1 P N1 IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H3 : {L, copy2 n1 n1 |- copy2 (N1 n1) (P n1)}* H4 : {L, copy2 n1 n1 |- copy2 (M1 n1) (Q n1)}* ============================ {L, copy2 n1 n2 |- copy2 (app (N1 n1) (M1 n1)) (app (P n2) (Q n2))} Subgoal 2 is: {L, copy2 n1 n2 |- copy2 (abs (R n1)) (abs (S n2))} Subgoal 3 is: {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <apply IH to H1 H3.

Subgoal 1: Variables: K L Q M1 P N1 IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H3 : {L, copy2 n1 n1 |- copy2 (N1 n1) (P n1)}* H4 : {L, copy2 n1 n1 |- copy2 (M1 n1) (Q n1)}* H5 : {L, copy2 n1 n2 |- copy2 (N1 n1) (P n2)} ============================ {L, copy2 n1 n2 |- copy2 (app (N1 n1) (M1 n1)) (app (P n2) (Q n2))} Subgoal 2 is: {L, copy2 n1 n2 |- copy2 (abs (R n1)) (abs (S n2))} Subgoal 3 is: {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <apply IH to H1 H4.

Subgoal 1: Variables: K L Q M1 P N1 IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H3 : {L, copy2 n1 n1 |- copy2 (N1 n1) (P n1)}* H4 : {L, copy2 n1 n1 |- copy2 (M1 n1) (Q n1)}* H5 : {L, copy2 n1 n2 |- copy2 (N1 n1) (P n2)} H6 : {L, copy2 n1 n2 |- copy2 (M1 n1) (Q n2)} ============================ {L, copy2 n1 n2 |- copy2 (app (N1 n1) (M1 n1)) (app (P n2) (Q n2))} Subgoal 2 is: {L, copy2 n1 n2 |- copy2 (abs (R n1)) (abs (S n2))} Subgoal 3 is: {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <search.

Subgoal 2: Variables: K L S R IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H3 : {L, copy2 n1 n1, copy2 n2 n3 |- copy2 (R n1 n2) (S n1 n3)}* ============================ {L, copy2 n1 n2 |- copy2 (abs (R n1)) (abs (S n2))} Subgoal 3 is: {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <apply IH to _ H3.

Subgoal 2: Variables: K L S R IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H3 : {L, copy2 n1 n1, copy2 n2 n3 |- copy2 (R n1 n2) (S n1 n3)}* H4 : {L, copy2 n2 n3, copy2 n1 n4 |- copy2 (R n1 n2) (S n4 n3)} ============================ {L, copy2 n1 n2 |- copy2 (abs (R n1)) (abs (S n2))} Subgoal 3 is: {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <search.

Subgoal 3: Variables: M N K L F IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H3 : {L, copy2 n1 n1, [F n1] |- copy2 (M n1) (N n1)}* H4 : member (F n1) (copy2 n1 n1 :: L) ============================ {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <case H4.

Subgoal 3.1: Variables: M N K L IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H3 : {L, copy2 n1 n1, [copy2 n1 n1] |- copy2 (M n1) (N n1)}* ============================ {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} Subgoal 3.2 is: {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <case H3.

Subgoal 3.1: Variables: K L IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L ============================ {L, copy2 n1 n2 |- copy2 n1 n2} Subgoal 3.2 is: {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <search.

Subgoal 3.2: Variables: M N K L F IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H3 : {L, copy2 n1 n1, [F n1] |- copy2 (M n1) (N n1)}* H5 : member (F n1) L ============================ {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <apply member_fresh to H5.

Subgoal 3.2: Variables: M N K L F1 IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H3 : {L, copy2 n1 n1, [F1] |- copy2 (M n1) (N n1)}* H5 : member F1 L ============================ {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <apply ctx_mem2 to H1 H5.

Subgoal 3.2: Variables: M N K L X Y IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H3 : {L, copy2 n1 n1, [copy2 X Y] |- copy2 (M n1) (N n1)}* H5 : member (copy2 X Y) L ============================ {L, copy2 n1 n2 |- copy2 (M n1) (N n2)} copy2_align <case H3.

Subgoal 3.2: Variables: K L X Y IH : forall M N K L, nabla z, ctxs K L -> {L, copy2 z z |- copy2 (M z) (N z)}* -> (nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}) H1 : ctxs K L H5 : member (copy2 X Y) L ============================ {L, copy2 n1 n2 |- copy2 X Y} copy2_align <search.Proof completed.

Abella <Theorem ctxs_member1 : forall X Y L K, ctxs L K -> member (copy X Y) L -> member (copy2 X Y) K.

============================ forall X Y L K, ctxs L K -> member (copy X Y) L -> member (copy2 X Y) K ctxs_member1 <induction on 1.

IH : forall X Y L K, ctxs L K * -> member (copy X Y) L -> member (copy2 X Y) K ============================ forall X Y L K, ctxs L K @ -> member (copy X Y) L -> member (copy2 X Y) K ctxs_member1 <intros.

Variables: X Y L K IH : forall X Y L K, ctxs L K * -> member (copy X Y) L -> member (copy2 X Y) K H1 : ctxs L K @ H2 : member (copy X Y) L ============================ member (copy2 X Y) K ctxs_member1 <case H1.

Subgoal 1: Variables: X Y IH : forall X Y L K, ctxs L K * -> member (copy X Y) L -> member (copy2 X Y) K H2 : member (copy X Y) nil ============================ member (copy2 X Y) nil Subgoal 2 is: member (copy2 X Y) (copy2 X1 Y1 :: L2) ctxs_member1 <case H2.

Subgoal 2: Variables: X Y L2 Y1 X1 L1 IH : forall X Y L K, ctxs L K * -> member (copy X Y) L -> member (copy2 X Y) K H2 : member (copy X Y) (copy X1 Y1 :: L1) H3 : ctxs L1 L2 * ============================ member (copy2 X Y) (copy2 X1 Y1 :: L2) ctxs_member1 <case H2.

Subgoal 2.1: Variables: L2 Y1 X1 L1 IH : forall X Y L K, ctxs L K * -> member (copy X Y) L -> member (copy2 X Y) K H3 : ctxs L1 L2 * ============================ member (copy2 X1 Y1) (copy2 X1 Y1 :: L2) Subgoal 2.2 is: member (copy2 X Y) (copy2 X1 Y1 :: L2) ctxs_member1 <search.

Subgoal 2.2: Variables: X Y L2 Y1 X1 L1 IH : forall X Y L K, ctxs L K * -> member (copy X Y) L -> member (copy2 X Y) K H3 : ctxs L1 L2 * H4 : member (copy X Y) L1 ============================ member (copy2 X Y) (copy2 X1 Y1 :: L2) ctxs_member1 <apply IH to H3 H4.

Subgoal 2.2: Variables: X Y L2 Y1 X1 L1 IH : forall X Y L K, ctxs L K * -> member (copy X Y) L -> member (copy2 X Y) K H3 : ctxs L1 L2 * H4 : member (copy X Y) L1 H5 : member (copy2 X Y) L2 ============================ member (copy2 X Y) (copy2 X1 Y1 :: L2) ctxs_member1 <search.Proof completed.

Abella <Theorem copy_copy2 : forall L K M N, ctxs L K -> {L |- copy M N} -> {K |- copy2 M N}.

============================ forall L K M N, ctxs L K -> {L |- copy M N} -> {K |- copy2 M N} copy_copy2 <induction on 2.

IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} ============================ forall L K M N, ctxs L K -> {L |- copy M N}@ -> {K |- copy2 M N} copy_copy2 <intros.

Variables: L K M N IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} H1 : ctxs L K H2 : {L |- copy M N}@ ============================ {K |- copy2 M N} copy_copy2 <case H2.

Subgoal 1: Variables: L K Q M1 P N1 IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} H1 : ctxs L K H3 : {L |- copy N1 P}* H4 : {L |- copy M1 Q}* ============================ {K |- copy2 (app N1 M1) (app P Q)} Subgoal 2 is: {K |- copy2 (abs R) (abs S)} Subgoal 3 is: {K |- copy2 M N} copy_copy2 <apply IH to H1 H3.

Subgoal 1: Variables: L K Q M1 P N1 IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} H1 : ctxs L K H3 : {L |- copy N1 P}* H4 : {L |- copy M1 Q}* H5 : {K |- copy2 N1 P} ============================ {K |- copy2 (app N1 M1) (app P Q)} Subgoal 2 is: {K |- copy2 (abs R) (abs S)} Subgoal 3 is: {K |- copy2 M N} copy_copy2 <apply IH to H1 H4.

Subgoal 1: Variables: L K Q M1 P N1 IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} H1 : ctxs L K H3 : {L |- copy N1 P}* H4 : {L |- copy M1 Q}* H5 : {K |- copy2 N1 P} H6 : {K |- copy2 M1 Q} ============================ {K |- copy2 (app N1 M1) (app P Q)} Subgoal 2 is: {K |- copy2 (abs R) (abs S)} Subgoal 3 is: {K |- copy2 M N} copy_copy2 <search.

Subgoal 2: Variables: L K S R IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} H1 : ctxs L K H3 : {L, copy n1 n1 |- copy (R n1) (S n1)}* ============================ {K |- copy2 (abs R) (abs S)} Subgoal 3 is: {K |- copy2 M N} copy_copy2 <apply IH to _ H3.

Subgoal 2: Variables: L K S R IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} H1 : ctxs L K H3 : {L, copy n1 n1 |- copy (R n1) (S n1)}* H4 : {K, copy2 n1 n1 |- copy2 (R n1) (S n1)} ============================ {K |- copy2 (abs R) (abs S)} Subgoal 3 is: {K |- copy2 M N} copy_copy2 <apply copy2_align to H1 H4.

Subgoal 2: Variables: L K S R IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} H1 : ctxs L K H3 : {L, copy n1 n1 |- copy (R n1) (S n1)}* H4 : {K, copy2 n1 n1 |- copy2 (R n1) (S n1)} H5 : {K, copy2 n1 n2 |- copy2 (R n1) (S n2)} ============================ {K |- copy2 (abs R) (abs S)} Subgoal 3 is: {K |- copy2 M N} copy_copy2 <search.

Subgoal 3: Variables: L K M N F IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} H1 : ctxs L K H3 : {L, [F] |- copy M N}* H4 : member F L ============================ {K |- copy2 M N} copy_copy2 <apply ctx_mem1 to H1 H4.

Subgoal 3: Variables: L K M N X Y IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} H1 : ctxs L K H3 : {L, [copy X Y] |- copy M N}* H4 : member (copy X Y) L ============================ {K |- copy2 M N} copy_copy2 <case H3.

Subgoal 3: Variables: L K M N IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} H1 : ctxs L K H4 : member (copy M N) L ============================ {K |- copy2 M N} copy_copy2 <apply ctxs_member1 to H1 H4.

Subgoal 3: Variables: L K M N IH : forall L K M N, ctxs L K -> {L |- copy M N}* -> {K |- copy2 M N} H1 : ctxs L K H4 : member (copy M N) L H5 : member (copy2 M N) K ============================ {K |- copy2 M N} copy_copy2 <search.Proof completed.

Abella <Theorem copy_align : forall M N L, nabla x y, {L, copy x y |- copy (M x) (N y)} -> (nabla z, {L, copy z z |- copy (M z) (N z)}).

============================ forall M N L, nabla x y, {L, copy x y |- copy (M x) (N y)} -> (nabla z, {L, copy z z |- copy (M z) (N z)}) copy_align <intros.

Variables: M N L H1 : {L, copy n1 n2 |- copy (M n1) (N n2)} ============================ {L, copy n1 n1 |- copy (M n1) (N n1)} copy_align <inst H1 with n2 = n1.

Variables: M N L H1 : {L, copy n1 n2 |- copy (M n1) (N n2)} H2 : {L, copy n1 n1 |- copy (M n1) (N n1)} ============================ {L, copy n1 n1 |- copy (M n1) (N n1)} copy_align <search.Proof completed.

Abella <Theorem ctxs_member2 : forall X Y L K, ctxs L K -> member (copy2 X Y) K -> member (copy X Y) L.

============================ forall X Y L K, ctxs L K -> member (copy2 X Y) K -> member (copy X Y) L ctxs_member2 <induction on 1.

IH : forall X Y L K, ctxs L K * -> member (copy2 X Y) K -> member (copy X Y) L ============================ forall X Y L K, ctxs L K @ -> member (copy2 X Y) K -> member (copy X Y) L ctxs_member2 <intros.

Variables: X Y L K IH : forall X Y L K, ctxs L K * -> member (copy2 X Y) K -> member (copy X Y) L H1 : ctxs L K @ H2 : member (copy2 X Y) K ============================ member (copy X Y) L ctxs_member2 <case H1.

Subgoal 1: Variables: X Y IH : forall X Y L K, ctxs L K * -> member (copy2 X Y) K -> member (copy X Y) L H2 : member (copy2 X Y) nil ============================ member (copy X Y) nil Subgoal 2 is: member (copy X Y) (copy X1 Y1 :: L1) ctxs_member2 <case H2.

Subgoal 2: Variables: X Y L2 Y1 X1 L1 IH : forall X Y L K, ctxs L K * -> member (copy2 X Y) K -> member (copy X Y) L H2 : member (copy2 X Y) (copy2 X1 Y1 :: L2) H3 : ctxs L1 L2 * ============================ member (copy X Y) (copy X1 Y1 :: L1) ctxs_member2 <case H2.

Subgoal 2.1: Variables: L2 Y1 X1 L1 IH : forall X Y L K, ctxs L K * -> member (copy2 X Y) K -> member (copy X Y) L H3 : ctxs L1 L2 * ============================ member (copy X1 Y1) (copy X1 Y1 :: L1) Subgoal 2.2 is: member (copy X Y) (copy X1 Y1 :: L1) ctxs_member2 <search.

Subgoal 2.2: Variables: X Y L2 Y1 X1 L1 IH : forall X Y L K, ctxs L K * -> member (copy2 X Y) K -> member (copy X Y) L H3 : ctxs L1 L2 * H4 : member (copy2 X Y) L2 ============================ member (copy X Y) (copy X1 Y1 :: L1) ctxs_member2 <apply IH to H3 H4.

Subgoal 2.2: Variables: X Y L2 Y1 X1 L1 IH : forall X Y L K, ctxs L K * -> member (copy2 X Y) K -> member (copy X Y) L H3 : ctxs L1 L2 * H4 : member (copy2 X Y) L2 H5 : member (copy X Y) L1 ============================ member (copy X Y) (copy X1 Y1 :: L1) ctxs_member2 <search.Proof completed.

Abella <Theorem copy2_copy : forall L K M N, ctxs L K -> {K |- copy2 M N} -> {L |- copy M N}.

============================ forall L K M N, ctxs L K -> {K |- copy2 M N} -> {L |- copy M N} copy2_copy <induction on 2.

IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} ============================ forall L K M N, ctxs L K -> {K |- copy2 M N}@ -> {L |- copy M N} copy2_copy <intros.

Variables: L K M N IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} H1 : ctxs L K H2 : {K |- copy2 M N}@ ============================ {L |- copy M N} copy2_copy <case H2.

Subgoal 1: Variables: L K Q M1 P N1 IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} H1 : ctxs L K H3 : {K |- copy2 N1 P}* H4 : {K |- copy2 M1 Q}* ============================ {L |- copy (app N1 M1) (app P Q)} Subgoal 2 is: {L |- copy (abs R) (abs S)} Subgoal 3 is: {L |- copy M N} copy2_copy <apply IH to H1 H3.

Subgoal 1: Variables: L K Q M1 P N1 IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} H1 : ctxs L K H3 : {K |- copy2 N1 P}* H4 : {K |- copy2 M1 Q}* H5 : {L |- copy N1 P} ============================ {L |- copy (app N1 M1) (app P Q)} Subgoal 2 is: {L |- copy (abs R) (abs S)} Subgoal 3 is: {L |- copy M N} copy2_copy <apply IH to H1 H4.

Subgoal 1: Variables: L K Q M1 P N1 IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} H1 : ctxs L K H3 : {K |- copy2 N1 P}* H4 : {K |- copy2 M1 Q}* H5 : {L |- copy N1 P} H6 : {L |- copy M1 Q} ============================ {L |- copy (app N1 M1) (app P Q)} Subgoal 2 is: {L |- copy (abs R) (abs S)} Subgoal 3 is: {L |- copy M N} copy2_copy <search.

Subgoal 2: Variables: L K S R IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} H1 : ctxs L K H3 : {K, copy2 n1 n2 |- copy2 (R n1) (S n2)}* ============================ {L |- copy (abs R) (abs S)} Subgoal 3 is: {L |- copy M N} copy2_copy <apply IH to _ H3.

Subgoal 2: Variables: L K S R IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} H1 : ctxs L K H3 : {K, copy2 n1 n2 |- copy2 (R n1) (S n2)}* H4 : {L, copy n1 n2 |- copy (R n1) (S n2)} ============================ {L |- copy (abs R) (abs S)} Subgoal 3 is: {L |- copy M N} copy2_copy <apply copy_align to H4.

Subgoal 2: Variables: L K S R IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} H1 : ctxs L K H3 : {K, copy2 n1 n2 |- copy2 (R n1) (S n2)}* H4 : {L, copy n1 n2 |- copy (R n1) (S n2)} H5 : {L, copy n1 n1 |- copy (R n1) (S n1)} ============================ {L |- copy (abs R) (abs S)} Subgoal 3 is: {L |- copy M N} copy2_copy <search.

Subgoal 3: Variables: L K M N F IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} H1 : ctxs L K H3 : {K, [F] |- copy2 M N}* H4 : member F K ============================ {L |- copy M N} copy2_copy <apply ctx_mem2 to H1 H4.

Subgoal 3: Variables: L K M N X Y IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} H1 : ctxs L K H3 : {K, [copy2 X Y] |- copy2 M N}* H4 : member (copy2 X Y) K ============================ {L |- copy M N} copy2_copy <case H3.

Subgoal 3: Variables: L K M N IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} H1 : ctxs L K H4 : member (copy2 M N) K ============================ {L |- copy M N} copy2_copy <apply ctxs_member2 to H1 H4.

Subgoal 3: Variables: L K M N IH : forall L K M N, ctxs L K -> {K |- copy2 M N}* -> {L |- copy M N} H1 : ctxs L K H4 : member (copy2 M N) K H5 : member (copy M N) L ============================ {L |- copy M N} copy2_copy <search.Proof completed.

Abella <