Welcome to Abella 2.0.7-dev.

Abella < Type is_o o -> prop.

Abella < Import "list" with is_o := is_o.
Importing from "list".

Abella < Define adj : (list o) -> o -> (list o) -> prop by 
adj L A (A :: L) := is_o A /\ is_list L;
adj (B :: K) A (B :: L) := is_o B /\ adj K A L.

Abella < Theorem adj_1_is_list : 
forall K A L, adj K A L -> is_list K.

============================
 forall K A L, adj K A L -> is_list K

adj_1_is_list < induction on 1.

IH : forall K A L, adj K A L * -> is_list K
============================
 forall K A L, adj K A L @ -> is_list K

adj_1_is_list < intros.

Variables: K A L
IH : forall K A L, adj K A L * -> is_list K
H1 : adj K A L @
============================
 is_list K

adj_1_is_list < case H1.

Subgoal 1:

Variables: K A
IH : forall K A L, adj K A L * -> is_list K
H2 : is_o A
H3 : is_list K
============================
 is_list K

Subgoal 2 is:
 is_list (B :: K1)

adj_1_is_list < search.

Subgoal 2:

Variables: A L1 B K1
IH : forall K A L, adj K A L * -> is_list K
H2 : is_o B
H3 : adj K1 A L1 *
============================
 is_list (B :: K1)

adj_1_is_list < apply IH to H3.

Subgoal 2:

Variables: A L1 B K1
IH : forall K A L, adj K A L * -> is_list K
H2 : is_o B
H3 : adj K1 A L1 *
H4 : is_list K1
============================
 is_list (B :: K1)

adj_1_is_list < search.
Proof completed.

Abella < Theorem adj_2_is_o : 
forall K A L, adj K A L -> is_o A.

============================
 forall K A L, adj K A L -> is_o A

adj_2_is_o < induction on 1.

IH : forall K A L, adj K A L * -> is_o A
============================
 forall K A L, adj K A L @ -> is_o A

adj_2_is_o < intros.

Variables: K A L
IH : forall K A L, adj K A L * -> is_o A
H1 : adj K A L @
============================
 is_o A

adj_2_is_o < case H1.

Subgoal 1:

Variables: K A
IH : forall K A L, adj K A L * -> is_o A
H2 : is_o A
H3 : is_list K
============================
 is_o A

Subgoal 2 is:
 is_o A

adj_2_is_o < search.

Subgoal 2:

Variables: A L1 B K1
IH : forall K A L, adj K A L * -> is_o A
H2 : is_o B
H3 : adj K1 A L1 *
============================
 is_o A

adj_2_is_o < apply IH to H3.

Subgoal 2:

Variables: A L1 B K1
IH : forall K A L, adj K A L * -> is_o A
H2 : is_o B
H3 : adj K1 A L1 *
H4 : is_o A
============================
 is_o A

adj_2_is_o < search.
Proof completed.

Abella < Theorem adj_3_is_list : 
forall K A L, adj K A L -> is_list L.

============================
 forall K A L, adj K A L -> is_list L

adj_3_is_list < induction on 1.

IH : forall K A L, adj K A L * -> is_list L
============================
 forall K A L, adj K A L @ -> is_list L

adj_3_is_list < intros.

Variables: K A L
IH : forall K A L, adj K A L * -> is_list L
H1 : adj K A L @
============================
 is_list L

adj_3_is_list < case H1.

Subgoal 1:

Variables: K A
IH : forall K A L, adj K A L * -> is_list L
H2 : is_o A
H3 : is_list K
============================
 is_list (A :: K)

Subgoal 2 is:
 is_list (B :: L1)

adj_3_is_list < search.

Subgoal 2:

Variables: A L1 B K1
IH : forall K A L, adj K A L * -> is_list L
H2 : is_o B
H3 : adj K1 A L1 *
============================
 is_list (B :: L1)

adj_3_is_list < apply IH to H3.

Subgoal 2:

Variables: A L1 B K1
IH : forall K A L, adj K A L * -> is_list L
H2 : is_o B
H3 : adj K1 A L1 *
H4 : is_list L1
============================
 is_list (B :: L1)

adj_3_is_list < search.
Proof completed.

Abella < Theorem adj_exists : 
forall A L, is_o A -> is_list L -> (exists M, adj L A M).

============================
 forall A L, is_o A -> is_list L -> (exists M, adj L A M)

adj_exists < intros.

Variables: A L
H1 : is_o A
H2 : is_list L
============================
 exists M, adj L A M

adj_exists < search.
Proof completed.

Abella < Theorem adj_swap : 
forall A J K B L, adj J A K -> adj K B L ->
  (exists U, adj J B U /\ adj U A L).

============================
 forall A J K B L, adj J A K -> adj K B L ->
   (exists U, adj J B U /\ adj U A L)

adj_swap < induction on 2.

IH : forall A J K B L, adj J A K -> adj K B L * ->
       (exists U, adj J B U /\ adj U A L)
============================
 forall A J K B L, adj J A K -> adj K B L @ ->
   (exists U, adj J B U /\ adj U A L)

adj_swap < intros.

Variables: A J K B L
IH : forall A J K B L, adj J A K -> adj K B L * ->
       (exists U, adj J B U /\ adj U A L)
H1 : adj J A K
H2 : adj K B L @
============================
 exists U, adj J B U /\ adj U A L

adj_swap < case H2.

Subgoal 1:

Variables: A J K B
IH : forall A J K B L, adj J A K -> adj K B L * ->
       (exists U, adj J B U /\ adj U A L)
H1 : adj J A K
H3 : is_o B
H4 : is_list K
============================
 exists U, adj J B U /\ adj U A (B :: K)

Subgoal 2 is:
 exists U, adj J B U /\ adj U A (B1 :: L1)

adj_swap < case H1.

Subgoal 1.1:

Variables: A J B
IH : forall A J K B L, adj J A K -> adj K B L * ->
       (exists U, adj J B U /\ adj U A L)
H3 : is_o B
H4 : is_list (A :: J)
H5 : is_o A
H6 : is_list J
============================
 exists U, adj J B U /\ adj U A (B :: A :: J)

Subgoal 1.2 is:
 exists U, adj (B1 :: K1) B U /\ adj U A (B :: B1 :: L1)

Subgoal 2 is:
 exists U, adj J B U /\ adj U A (B1 :: L1)

adj_swap < search.

Subgoal 1.2:

Variables: A B L1 B1 K1
IH : forall A J K B L, adj J A K -> adj K B L * ->
       (exists U, adj J B U /\ adj U A L)
H3 : is_o B
H4 : is_list (B1 :: L1)
H5 : is_o B1
H6 : adj K1 A L1
============================
 exists U, adj (B1 :: K1) B U /\ adj U A (B :: B1 :: L1)

Subgoal 2 is:
 exists U, adj J B U /\ adj U A (B1 :: L1)

adj_swap < apply adj_1_is_list to H6.

Subgoal 1.2:

Variables: A B L1 B1 K1
IH : forall A J K B L, adj J A K -> adj K B L * ->
       (exists U, adj J B U /\ adj U A L)
H3 : is_o B
H4 : is_list (B1 :: L1)
H5 : is_o B1
H6 : adj K1 A L1
H7 : is_list K1
============================
 exists U, adj (B1 :: K1) B U /\ adj U A (B :: B1 :: L1)

Subgoal 2 is:
 exists U, adj J B U /\ adj U A (B1 :: L1)

adj_swap < search.

Subgoal 2:

Variables: A J B L1 B1 K1
IH : forall A J K B L, adj J A K -> adj K B L * ->
       (exists U, adj J B U /\ adj U A L)
H1 : adj J A (B1 :: K1)
H3 : is_o B1
H4 : adj K1 B L1 *
============================
 exists U, adj J B U /\ adj U A (B1 :: L1)

adj_swap < case H1.

Subgoal 2.1:

Variables: B L1 B1 K1
IH : forall A J K B L, adj J A K -> adj K B L * ->
       (exists U, adj J B U /\ adj U A L)
H3 : is_o B1
H4 : adj K1 B L1 *
H5 : is_o B1
H6 : is_list K1
============================
 exists U, adj K1 B U /\ adj U B1 (B1 :: L1)

Subgoal 2.2 is:
 exists U, adj (B1 :: K2) B U /\ adj U A (B1 :: L1)

adj_swap < apply adj_3_is_list to H4.

Subgoal 2.1:

Variables: B L1 B1 K1
IH : forall A J K B L, adj J A K -> adj K B L * ->
       (exists U, adj J B U /\ adj U A L)
H3 : is_o B1
H4 : adj K1 B L1 *
H5 : is_o B1
H6 : is_list K1
H7 : is_list L1
============================
 exists U, adj K1 B U /\ adj U B1 (B1 :: L1)

Subgoal 2.2 is:
 exists U, adj (B1 :: K2) B U /\ adj U A (B1 :: L1)

adj_swap < search.

Subgoal 2.2:

Variables: A B L1 B1 K1 K2
IH : forall A J K B L, adj J A K -> adj K B L * ->
       (exists U, adj J B U /\ adj U A L)
H3 : is_o B1
H4 : adj K1 B L1 *
H5 : is_o B1
H6 : adj K2 A K1
============================
 exists U, adj (B1 :: K2) B U /\ adj U A (B1 :: L1)

adj_swap < apply IH to H6 H4.

Subgoal 2.2:

Variables: A B L1 B1 K1 K2 U
IH : forall A J K B L, adj J A K -> adj K B L * ->
       (exists U, adj J B U /\ adj U A L)
H3 : is_o B1
H4 : adj K1 B L1 *
H5 : is_o B1
H6 : adj K2 A K1
H7 : adj K2 B U
H8 : adj U A L1
============================
 exists U, adj (B1 :: K2) B U /\ adj U A (B1 :: L1)

adj_swap < search.
Proof completed.

Abella < Theorem adj_same : 
forall A L B, adj L A (B :: L) -> A = B.

============================
 forall A L B, adj L A (B :: L) -> A = B

adj_same < induction on 1.

IH : forall A L B, adj L A (B :: L) * -> A = B
============================
 forall A L B, adj L A (B :: L) @ -> A = B

adj_same < intros.

Variables: A L B
IH : forall A L B, adj L A (B :: L) * -> A = B
H1 : adj L A (B :: L) @
============================
 A = B

adj_same < case H1.

Subgoal 1:

Variables: L B
IH : forall A L B, adj L A (B :: L) * -> A = B
H2 : is_o B
H3 : is_list L
============================
 B = B

Subgoal 2 is:
 A = B

adj_same < search.

Subgoal 2:

Variables: A B K
IH : forall A L B, adj L A (B :: L) * -> A = B
H2 : is_o B
H3 : adj K A (B :: K) *
============================
 A = B

adj_same < apply IH to H3.

Subgoal 2:

Variables: B K
IH : forall A L B, adj L A (B :: L) * -> A = B
H2 : is_o B
H3 : adj K B (B :: K) *
============================
 B = B

adj_same < search.
Proof completed.

Abella < Theorem adj_append_1 : 
forall J A K L KL, adj J A K -> append K L KL ->
  (exists JL, append J L JL /\ adj JL A KL).

============================
 forall J A K L KL, adj J A K -> append K L KL ->
   (exists JL, append J L JL /\ adj JL A KL)

adj_append_1 < induction on 1.

IH : forall J A K L KL, adj J A K * -> append K L KL ->
       (exists JL, append J L JL /\ adj JL A KL)
============================
 forall J A K L KL, adj J A K @ -> append K L KL ->
   (exists JL, append J L JL /\ adj JL A KL)

adj_append_1 < intros.

Variables: J A K L KL
IH : forall J A K L KL, adj J A K * -> append K L KL ->
       (exists JL, append J L JL /\ adj JL A KL)
H1 : adj J A K @
H2 : append K L KL
============================
 exists JL, append J L JL /\ adj JL A KL

adj_append_1 < case H1.

Subgoal 1:

Variables: J A L KL
IH : forall J A K L KL, adj J A K * -> append K L KL ->
       (exists JL, append J L JL /\ adj JL A KL)
H2 : append (A :: J) L KL
H3 : is_o A
H4 : is_list J
============================
 exists JL, append J L JL /\ adj JL A KL

Subgoal 2 is:
 exists JL, append (B :: K1) L JL /\ adj JL A KL

adj_append_1 < case H2.

Subgoal 1:

Variables: J A L L1
IH : forall J A K L KL, adj J A K * -> append K L KL ->
       (exists JL, append J L JL /\ adj JL A KL)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : append J L L1
============================
 exists JL, append J L JL /\ adj JL A (A :: L1)

Subgoal 2 is:
 exists JL, append (B :: K1) L JL /\ adj JL A KL

adj_append_1 < apply append_2_is_list to H6.

Subgoal 1:

Variables: J A L L1
IH : forall J A K L KL, adj J A K * -> append K L KL ->
       (exists JL, append J L JL /\ adj JL A KL)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : append J L L1
H7 : is_list L
============================
 exists JL, append J L JL /\ adj JL A (A :: L1)

Subgoal 2 is:
 exists JL, append (B :: K1) L JL /\ adj JL A KL

adj_append_1 < apply append_3_is_list to H6.

Subgoal 1:

Variables: J A L L1
IH : forall J A K L KL, adj J A K * -> append K L KL ->
       (exists JL, append J L JL /\ adj JL A KL)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : append J L L1
H7 : is_list L
H8 : is_list L1
============================
 exists JL, append J L JL /\ adj JL A (A :: L1)

Subgoal 2 is:
 exists JL, append (B :: K1) L JL /\ adj JL A KL

adj_append_1 < search.

Subgoal 2:

Variables: A L KL L1 B K1
IH : forall J A K L KL, adj J A K * -> append K L KL ->
       (exists JL, append J L JL /\ adj JL A KL)
H2 : append (B :: L1) L KL
H3 : is_o B
H4 : adj K1 A L1 *
============================
 exists JL, append (B :: K1) L JL /\ adj JL A KL

adj_append_1 < case H2.

Subgoal 2:

Variables: A L L1 B K1 L2
IH : forall J A K L KL, adj J A K * -> append K L KL ->
       (exists JL, append J L JL /\ adj JL A KL)
H3 : is_o B
H4 : adj K1 A L1 *
H5 : is_o B
H6 : append L1 L L2
============================
 exists JL, append (B :: K1) L JL /\ adj JL A (B :: L2)

adj_append_1 < apply IH to H4 H6.

Subgoal 2:

Variables: A L L1 B K1 L2 JL
IH : forall J A K L KL, adj J A K * -> append K L KL ->
       (exists JL, append J L JL /\ adj JL A KL)
H3 : is_o B
H4 : adj K1 A L1 *
H5 : is_o B
H6 : append L1 L L2
H7 : append K1 L JL
H8 : adj JL A L2
============================
 exists JL, append (B :: K1) L JL /\ adj JL A (B :: L2)

adj_append_1 < search.
Proof completed.

Abella < Theorem adj_1_append : 
forall J A K L JL, adj J A K -> append J L JL ->
  (exists KL, append K L KL /\ adj JL A KL).

============================
 forall J A K L JL, adj J A K -> append J L JL ->
   (exists KL, append K L KL /\ adj JL A KL)

adj_1_append < induction on 1.

IH : forall J A K L JL, adj J A K * -> append J L JL ->
       (exists KL, append K L KL /\ adj JL A KL)
============================
 forall J A K L JL, adj J A K @ -> append J L JL ->
   (exists KL, append K L KL /\ adj JL A KL)

adj_1_append < intros.

Variables: J A K L JL
IH : forall J A K L JL, adj J A K * -> append J L JL ->
       (exists KL, append K L KL /\ adj JL A KL)
H1 : adj J A K @
H2 : append J L JL
============================
 exists KL, append K L KL /\ adj JL A KL

adj_1_append < case H1.

Subgoal 1:

Variables: J A L JL
IH : forall J A K L JL, adj J A K * -> append J L JL ->
       (exists KL, append K L KL /\ adj JL A KL)
H2 : append J L JL
H3 : is_o A
H4 : is_list J
============================
 exists KL, append (A :: J) L KL /\ adj JL A KL

Subgoal 2 is:
 exists KL, append (B :: L1) L KL /\ adj JL A KL

adj_1_append < apply append_2_is_list to H2.

Subgoal 1:

Variables: J A L JL
IH : forall J A K L JL, adj J A K * -> append J L JL ->
       (exists KL, append K L KL /\ adj JL A KL)
H2 : append J L JL
H3 : is_o A
H4 : is_list J
H5 : is_list L
============================
 exists KL, append (A :: J) L KL /\ adj JL A KL

Subgoal 2 is:
 exists KL, append (B :: L1) L KL /\ adj JL A KL

adj_1_append < apply append_3_is_list to H2.

Subgoal 1:

Variables: J A L JL
IH : forall J A K L JL, adj J A K * -> append J L JL ->
       (exists KL, append K L KL /\ adj JL A KL)
H2 : append J L JL
H3 : is_o A
H4 : is_list J
H5 : is_list L
H6 : is_list JL
============================
 exists KL, append (A :: J) L KL /\ adj JL A KL

Subgoal 2 is:
 exists KL, append (B :: L1) L KL /\ adj JL A KL

adj_1_append < search.

Subgoal 2:

Variables: A L JL L1 B K1
IH : forall J A K L JL, adj J A K * -> append J L JL ->
       (exists KL, append K L KL /\ adj JL A KL)
H2 : append (B :: K1) L JL
H3 : is_o B
H4 : adj K1 A L1 *
============================
 exists KL, append (B :: L1) L KL /\ adj JL A KL

adj_1_append < case H2.

Subgoal 2:

Variables: A L L1 B K1 L2
IH : forall J A K L JL, adj J A K * -> append J L JL ->
       (exists KL, append K L KL /\ adj JL A KL)
H3 : is_o B
H4 : adj K1 A L1 *
H5 : is_o B
H6 : append K1 L L2
============================
 exists KL, append (B :: L1) L KL /\ adj (B :: L2) A KL

adj_1_append < apply IH to H4 H6.

Subgoal 2:

Variables: A L L1 B K1 L2 KL
IH : forall J A K L JL, adj J A K * -> append J L JL ->
       (exists KL, append K L KL /\ adj JL A KL)
H3 : is_o B
H4 : adj K1 A L1 *
H5 : is_o B
H6 : append K1 L L2
H7 : append L1 L KL
H8 : adj L2 A KL
============================
 exists KL, append (B :: L1) L KL /\ adj (B :: L2) A KL

adj_1_append < search.
Proof completed.

Abella < Define perm : (list o) -> (list o) -> prop by 
perm nil nil;
perm K L := exists A KK LL, adj KK A K /\ adj LL A L /\ perm KK LL.

Abella < Theorem perm_1_is_list : 
forall K L, perm K L -> is_list K.

============================
 forall K L, perm K L -> is_list K

perm_1_is_list < intros.

Variables: K L
H1 : perm K L
============================
 is_list K

perm_1_is_list < case H1.

Subgoal 1:

============================
 is_list nil

Subgoal 2 is:
 is_list K

perm_1_is_list < search.

Subgoal 2:

Variables: K L A KK LL
H2 : adj KK A K
H3 : adj LL A L
H4 : perm KK LL
============================
 is_list K

perm_1_is_list < backchain adj_3_is_list.
Proof completed.

Abella < Theorem perm_2_is_list : 
forall K L, perm K L -> is_list L.

============================
 forall K L, perm K L -> is_list L

perm_2_is_list < intros.

Variables: K L
H1 : perm K L
============================
 is_list L

perm_2_is_list < case H1.

Subgoal 1:

============================
 is_list nil

Subgoal 2 is:
 is_list L

perm_2_is_list < search.

Subgoal 2:

Variables: K L A KK LL
H2 : adj KK A K
H3 : adj LL A L
H4 : perm KK LL
============================
 is_list L

perm_2_is_list < backchain adj_3_is_list.
Proof completed.

Abella < Theorem perm_refl : 
forall L, is_list L -> perm L L.

============================
 forall L, is_list L -> perm L L

perm_refl < induction on 1.

IH : forall L, is_list L * -> perm L L
============================
 forall L, is_list L @ -> perm L L

perm_refl < intros.

Variables: L
IH : forall L, is_list L * -> perm L L
H1 : is_list L @
============================
 perm L L

perm_refl < case H1.

Subgoal 1:

IH : forall L, is_list L * -> perm L L
============================
 perm nil nil

Subgoal 2 is:
 perm (A :: L1) (A :: L1)

perm_refl < search.

Subgoal 2:

Variables: L1 A
IH : forall L, is_list L * -> perm L L
H2 : is_o A
H3 : is_list L1 *
============================
 perm (A :: L1) (A :: L1)

perm_refl < apply IH to H3.

Subgoal 2:

Variables: L1 A
IH : forall L, is_list L * -> perm L L
H2 : is_o A
H3 : is_list L1 *
H4 : perm L1 L1
============================
 perm (A :: L1) (A :: L1)

perm_refl < search.
Proof completed.

Abella < Theorem perm_sym : 
forall K L, perm K L -> perm L K.

============================
 forall K L, perm K L -> perm L K

perm_sym < induction on 1.

IH : forall K L, perm K L * -> perm L K
============================
 forall K L, perm K L @ -> perm L K

perm_sym < intros.

Variables: K L
IH : forall K L, perm K L * -> perm L K
H1 : perm K L @
============================
 perm L K

perm_sym < case H1.

Subgoal 1:

IH : forall K L, perm K L * -> perm L K
============================
 perm nil nil

Subgoal 2 is:
 perm L K

perm_sym < search.

Subgoal 2:

Variables: K L A KK LL
IH : forall K L, perm K L * -> perm L K
H2 : adj KK A K
H3 : adj LL A L
H4 : perm KK LL *
============================
 perm L K

perm_sym < apply IH to H4.

Subgoal 2:

Variables: K L A KK LL
IH : forall K L, perm K L * -> perm L K
H2 : adj KK A K
H3 : adj LL A L
H4 : perm KK LL *
H5 : perm LL KK
============================
 perm L K

perm_sym < search.
Proof completed.

Abella < Theorem perm_cons_1 : 
forall A K L, perm (A :: K) L -> (exists J, adj J A L /\ perm K J).

============================
 forall A K L, perm (A :: K) L -> (exists J, adj J A L /\ perm K J)

perm_cons_1 < induction on 1.

IH : forall A K L, perm (A :: K) L * -> (exists J, adj J A L /\ perm K J)
============================
 forall A K L, perm (A :: K) L @ -> (exists J, adj J A L /\ perm K J)

perm_cons_1 < intros.

Variables: A K L
IH : forall A K L, perm (A :: K) L * -> (exists J, adj J A L /\ perm K J)
H1 : perm (A :: K) L @
============================
 exists J, adj J A L /\ perm K J

perm_cons_1 < case H1.

Variables: A K L A1 KK LL
IH : forall A K L, perm (A :: K) L * -> (exists J, adj J A L /\ perm K J)
H2 : adj KK A1 (A :: K)
H3 : adj LL A1 L
H4 : perm KK LL *
============================
 exists J, adj J A L /\ perm K J

perm_cons_1 < case H2.

Subgoal 1:

Variables: A K L LL
IH : forall A K L, perm (A :: K) L * -> (exists J, adj J A L /\ perm K J)
H3 : adj LL A L
H4 : perm K LL *
H5 : is_o A
H6 : is_list K
============================
 exists J, adj J A L /\ perm K J

Subgoal 2 is:
 exists J, adj J A L /\ perm K J

perm_cons_1 < search.

Subgoal 2:

Variables: A K L A1 LL K1
IH : forall A K L, perm (A :: K) L * -> (exists J, adj J A L /\ perm K J)
H3 : adj LL A1 L
H4 : perm (A :: K1) LL *
H5 : is_o A
H6 : adj K1 A1 K
============================
 exists J, adj J A L /\ perm K J

perm_cons_1 < apply IH to H4.

Subgoal 2:

Variables: A K L A1 LL K1 J
IH : forall A K L, perm (A :: K) L * -> (exists J, adj J A L /\ perm K J)
H3 : adj LL A1 L
H4 : perm (A :: K1) LL *
H5 : is_o A
H6 : adj K1 A1 K
H7 : adj J A LL
H8 : perm K1 J
============================
 exists J, adj J A L /\ perm K J

perm_cons_1 < apply adj_swap to H7 H3.

Subgoal 2:

Variables: A K L A1 LL K1 J U
IH : forall A K L, perm (A :: K) L * -> (exists J, adj J A L /\ perm K J)
H3 : adj LL A1 L
H4 : perm (A :: K1) LL *
H5 : is_o A
H6 : adj K1 A1 K
H7 : adj J A LL
H8 : perm K1 J
H9 : adj J A1 U
H10 : adj U A L
============================
 exists J, adj J A L /\ perm K J

perm_cons_1 < apply adj_1_is_list to H6.

Subgoal 2:

Variables: A K L A1 LL K1 J U
IH : forall A K L, perm (A :: K) L * -> (exists J, adj J A L /\ perm K J)
H3 : adj LL A1 L
H4 : perm (A :: K1) LL *
H5 : is_o A
H6 : adj K1 A1 K
H7 : adj J A LL
H8 : perm K1 J
H9 : adj J A1 U
H10 : adj U A L
H11 : is_list K1
============================
 exists J, adj J A L /\ perm K J

perm_cons_1 < apply adj_1_is_list to H7.

Subgoal 2:

Variables: A K L A1 LL K1 J U
IH : forall A K L, perm (A :: K) L * -> (exists J, adj J A L /\ perm K J)
H3 : adj LL A1 L
H4 : perm (A :: K1) LL *
H5 : is_o A
H6 : adj K1 A1 K
H7 : adj J A LL
H8 : perm K1 J
H9 : adj J A1 U
H10 : adj U A L
H11 : is_list K1
H12 : is_list J
============================
 exists J, adj J A L /\ perm K J

perm_cons_1 < search.
Proof completed.

Abella < Theorem perm_cons_2 : 
forall A K L, perm K (A :: L) -> (exists J, adj J A K /\ perm J L).

============================
 forall A K L, perm K (A :: L) -> (exists J, adj J A K /\ perm J L)

perm_cons_2 < intros.

Variables: A K L
H1 : perm K (A :: L)
============================
 exists J, adj J A K /\ perm J L

perm_cons_2 < apply perm_sym to *H1.

Variables: A K L
H2 : perm (A :: L) K
============================
 exists J, adj J A K /\ perm J L

perm_cons_2 < apply perm_cons_1 to *H2.

Variables: A K L J
H3 : adj J A K
H4 : perm L J
============================
 exists J, adj J A K /\ perm J L

perm_cons_2 < apply perm_sym to *H4.

Variables: A K L J
H3 : adj J A K
H5 : perm J L
============================
 exists J, adj J A K /\ perm J L

perm_cons_2 < search.
Proof completed.

Abella < Theorem adj_preserves_perm : 
forall A JJ J KK K, adj JJ A J -> adj KK A K -> perm JJ KK -> perm J K.

============================
 forall A JJ J KK K, adj JJ A J -> adj KK A K -> perm JJ KK -> perm J K

adj_preserves_perm < intros.

Variables: A JJ J KK K
H1 : adj JJ A J
H2 : adj KK A K
H3 : perm JJ KK
============================
 perm J K

adj_preserves_perm < search.
Proof completed.

Abella < Theorem perm_trans_lem : 
forall J K L, is_list K -> perm J K -> perm K L -> perm J L.

============================
 forall J K L, is_list K -> perm J K -> perm K L -> perm J L

perm_trans_lem < induction on 1.

IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
============================
 forall J K L, is_list K @ -> perm J K -> perm K L -> perm J L

perm_trans_lem < intros.

Variables: J K L
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H1 : is_list K @
H2 : perm J K
H3 : perm K L
============================
 perm J L

perm_trans_lem < case H1.

Subgoal 1:

Variables: J L
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H2 : perm J nil
H3 : perm nil L
============================
 perm J L

Subgoal 2 is:
 perm J L

perm_trans_lem < case H2.

Subgoal 1.1:

Variables: L
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H3 : perm nil L
============================
 perm nil L

Subgoal 1.2 is:
 perm J L

Subgoal 2 is:
 perm J L

perm_trans_lem < case H3.

Subgoal 1.1.1:

IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
============================
 perm nil nil

Subgoal 1.1.2 is:
 perm nil L

Subgoal 1.2 is:
 perm J L

Subgoal 2 is:
 perm J L

perm_trans_lem < search.

Subgoal 1.1.2:

Variables: L A KK LL
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : adj KK A nil
H5 : adj LL A L
H6 : perm KK LL
============================
 perm nil L

Subgoal 1.2 is:
 perm J L

Subgoal 2 is:
 perm J L

perm_trans_lem < case H4.

Subgoal 1.2:

Variables: J L A KK LL
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H3 : perm nil L
H4 : adj KK A J
H5 : adj LL A nil
H6 : perm KK LL
============================
 perm J L

Subgoal 2 is:
 perm J L

perm_trans_lem < case H5.

Subgoal 2:

Variables: J L L1 A
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H2 : perm J (A :: L1)
H3 : perm (A :: L1) L
H4 : is_o A
H5 : is_list L1 *
============================
 perm J L

perm_trans_lem < case H2.

Subgoal 2:

Variables: J L L1 A A1 KK LL
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H3 : perm (A :: L1) L
H4 : is_o A
H5 : is_list L1 *
H6 : adj KK A1 J
H7 : adj LL A1 (A :: L1)
H8 : perm KK LL
============================
 perm J L

perm_trans_lem < case H3.

Subgoal 2:

Variables: J L L1 A A1 KK LL A2 KK1 LL1
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H6 : adj KK A1 J
H7 : adj LL A1 (A :: L1)
H8 : perm KK LL
H9 : adj KK1 A2 (A :: L1)
H10 : adj LL1 A2 L
H11 : perm KK1 LL1
============================
 perm J L

perm_trans_lem < case H7.

Subgoal 2.1:

Variables: J L L1 A KK A2 KK1 LL1
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H6 : adj KK A J
H8 : perm KK L1
H9 : adj KK1 A2 (A :: L1)
H10 : adj LL1 A2 L
H11 : perm KK1 LL1
H12 : is_o A
H13 : is_list L1
============================
 perm J L

Subgoal 2.2 is:
 perm J L

perm_trans_lem < case H9.

Subgoal 2.1.1:

Variables: J L L1 A KK LL1
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H6 : adj KK A J
H8 : perm KK L1
H10 : adj LL1 A L
H11 : perm L1 LL1
H12 : is_o A
H13 : is_list L1
H14 : is_o A
H15 : is_list L1
============================
 perm J L

Subgoal 2.1.2 is:
 perm J L

Subgoal 2.2 is:
 perm J L

perm_trans_lem < apply IH to *H5 *H8 *H11.

Subgoal 2.1.1:

Variables: J L L1 A KK LL1
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H6 : adj KK A J
H10 : adj LL1 A L
H12 : is_o A
H13 : is_list L1
H14 : is_o A
H15 : is_list L1
H16 : perm KK LL1
============================
 perm J L

Subgoal 2.1.2 is:
 perm J L

Subgoal 2.2 is:
 perm J L

perm_trans_lem < search.

Subgoal 2.1.2:

Variables: J L L1 A KK A2 LL1 K1
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H6 : adj KK A J
H8 : perm KK L1
H10 : adj LL1 A2 L
H11 : perm (A :: K1) LL1
H12 : is_o A
H13 : is_list L1
H14 : is_o A
H15 : adj K1 A2 L1
============================
 perm J L

Subgoal 2.2 is:
 perm J L

perm_trans_lem < apply perm_cons_1 to *H11.

Subgoal 2.1.2:

Variables: J L L1 A KK A2 LL1 K1 J1
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H6 : adj KK A J
H8 : perm KK L1
H10 : adj LL1 A2 L
H12 : is_o A
H13 : is_list L1
H14 : is_o A
H15 : adj K1 A2 L1
H16 : adj J1 A LL1
H17 : perm K1 J1
============================
 perm J L

Subgoal 2.2 is:
 perm J L

perm_trans_lem < apply adj_swap to *H16 *H10.

Subgoal 2.1.2:

Variables: J L L1 A KK A2 LL1 K1 J1 U
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H6 : adj KK A J
H8 : perm KK L1
H12 : is_o A
H13 : is_list L1
H14 : is_o A
H15 : adj K1 A2 L1
H17 : perm K1 J1
H18 : adj J1 A2 U
H19 : adj U A L
============================
 perm J L

Subgoal 2.2 is:
 perm J L

perm_trans_lem < apply adj_preserves_perm to *H15 *H18 *H17.

Subgoal 2.1.2:

Variables: J L L1 A KK A2 LL1 K1 J1 U
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H6 : adj KK A J
H8 : perm KK L1
H12 : is_o A
H13 : is_list L1
H14 : is_o A
H19 : adj U A L
H20 : perm L1 U
============================
 perm J L

Subgoal 2.2 is:
 perm J L

perm_trans_lem < apply IH to *H5 *H8 *H20.

Subgoal 2.1.2:

Variables: J L L1 A KK A2 LL1 K1 J1 U
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H6 : adj KK A J
H12 : is_o A
H13 : is_list L1
H14 : is_o A
H19 : adj U A L
H21 : perm KK U
============================
 perm J L

Subgoal 2.2 is:
 perm J L

perm_trans_lem < backchain adj_preserves_perm.

Subgoal 2.2:

Variables: J L L1 A A1 KK A2 KK1 LL1 K1
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H6 : adj KK A1 J
H8 : perm KK (A :: K1)
H9 : adj KK1 A2 (A :: L1)
H10 : adj LL1 A2 L
H11 : perm KK1 LL1
H12 : is_o A
H13 : adj K1 A1 L1
============================
 perm J L

perm_trans_lem < apply perm_cons_2 to *H8.

Subgoal 2.2:

Variables: J L L1 A A1 KK A2 KK1 LL1 K1 J1
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H6 : adj KK A1 J
H9 : adj KK1 A2 (A :: L1)
H10 : adj LL1 A2 L
H11 : perm KK1 LL1
H12 : is_o A
H13 : adj K1 A1 L1
H14 : adj J1 A KK
H15 : perm J1 K1
============================
 perm J L

perm_trans_lem < apply adj_swap to *H14 *H6.

Subgoal 2.2:

Variables: J L L1 A A1 KK A2 KK1 LL1 K1 J1 U
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H9 : adj KK1 A2 (A :: L1)
H10 : adj LL1 A2 L
H11 : perm KK1 LL1
H12 : is_o A
H13 : adj K1 A1 L1
H15 : perm J1 K1
H16 : adj J1 A1 U
H17 : adj U A J
============================
 perm J L

perm_trans_lem < apply adj_preserves_perm to *H16 *H13 *H15.

Subgoal 2.2:

Variables: J L L1 A A1 KK A2 KK1 LL1 K1 J1 U
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H9 : adj KK1 A2 (A :: L1)
H10 : adj LL1 A2 L
H11 : perm KK1 LL1
H12 : is_o A
H17 : adj U A J
H18 : perm U L1
============================
 perm J L

perm_trans_lem < apply adj_preserves_perm to *H9 *H10 *H11.

Subgoal 2.2:

Variables: J L L1 A A1 KK A2 KK1 LL1 K1 J1 U
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H12 : is_o A
H17 : adj U A J
H18 : perm U L1
H19 : perm (A :: L1) L
============================
 perm J L

perm_trans_lem < apply perm_cons_1 to *H19.

Subgoal 2.2:

Variables: J L L1 A A1 KK A2 KK1 LL1 K1 J1 U J2
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H5 : is_list L1 *
H12 : is_o A
H17 : adj U A J
H18 : perm U L1
H20 : adj J2 A L
H21 : perm L1 J2
============================
 perm J L

perm_trans_lem < apply IH to *H5 *H18 *H21.

Subgoal 2.2:

Variables: J L L1 A A1 KK A2 KK1 LL1 K1 J1 U J2
IH : forall J K L, is_list K * -> perm J K -> perm K L -> perm J L
H4 : is_o A
H12 : is_o A
H17 : adj U A J
H20 : adj J2 A L
H22 : perm U J2
============================
 perm J L

perm_trans_lem < backchain adj_preserves_perm.
Proof completed.

Abella < Theorem perm_trans : 
forall J K L, perm J K -> perm K L -> perm J L.

============================
 forall J K L, perm J K -> perm K L -> perm J L

perm_trans < intros.

Variables: J K L
H1 : perm J K
H2 : perm K L
============================
 perm J L

perm_trans < apply perm_2_is_list to H1.

Variables: J K L
H1 : perm J K
H2 : perm K L
H3 : is_list K
============================
 perm J L

perm_trans < backchain perm_trans_lem.
Proof completed.

Abella < Theorem adj_same_source : 
forall J A K L, adj J A K -> adj J A L -> perm K L.

============================
 forall J A K L, adj J A K -> adj J A L -> perm K L

adj_same_source < intros.

Variables: J A K L
H1 : adj J A K
H2 : adj J A L
============================
 perm K L

adj_same_source < apply adj_1_is_list to H1.

Variables: J A K L
H1 : adj J A K
H2 : adj J A L
H3 : is_list J
============================
 perm K L

adj_same_source < apply perm_refl to H3.

Variables: J A K L
H1 : adj J A K
H2 : adj J A L
H3 : is_list J
H4 : perm J J
============================
 perm K L

adj_same_source < search.
Proof completed.

Abella < Theorem adj_same_result : 
forall J K A L, adj J A L -> adj K A L -> perm J K.

============================
 forall J K A L, adj J A L -> adj K A L -> perm J K

adj_same_result < induction on 1.

IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
============================
 forall J K A L, adj J A L @ -> adj K A L -> perm J K

adj_same_result < intros.

Variables: J K A L
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H1 : adj J A L @
H2 : adj K A L
============================
 perm J K

adj_same_result < case H1.

Subgoal 1:

Variables: J K A
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H2 : adj K A (A :: J)
H3 : is_o A
H4 : is_list J
============================
 perm J K

Subgoal 2 is:
 perm (B :: K1) K

adj_same_result < case H2.

Subgoal 1.1:

Variables: J A
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : is_list J
============================
 perm J J

Subgoal 1.2 is:
 perm J (A :: K1)

Subgoal 2 is:
 perm (B :: K1) K

adj_same_result < backchain perm_refl.

Subgoal 1.2:

Variables: J A K1
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 A J
============================
 perm J (A :: K1)

Subgoal 2 is:
 perm (B :: K1) K

adj_same_result < apply adj_1_is_list to H6.

Subgoal 1.2:

Variables: J A K1
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 A J
H7 : is_list K1
============================
 perm J (A :: K1)

Subgoal 2 is:
 perm (B :: K1) K

adj_same_result < apply perm_refl to H7.

Subgoal 1.2:

Variables: J A K1
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 A J
H7 : is_list K1
H8 : perm K1 K1
============================
 perm J (A :: K1)

Subgoal 2 is:
 perm (B :: K1) K

adj_same_result < search.

Subgoal 2:

Variables: K A L1 B K1
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H2 : adj K A (B :: L1)
H3 : is_o B
H4 : adj K1 A L1 *
============================
 perm (B :: K1) K

adj_same_result < case H2.

Subgoal 2.1:

Variables: L1 B K1
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H3 : is_o B
H4 : adj K1 B L1 *
H5 : is_o B
H6 : is_list L1
============================
 perm (B :: K1) L1

Subgoal 2.2 is:
 perm (B :: K1) (B :: K2)

adj_same_result < apply adj_1_is_list to H4.

Subgoal 2.1:

Variables: L1 B K1
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H3 : is_o B
H4 : adj K1 B L1 *
H5 : is_o B
H6 : is_list L1
H7 : is_list K1
============================
 perm (B :: K1) L1

Subgoal 2.2 is:
 perm (B :: K1) (B :: K2)

adj_same_result < apply perm_refl to H7.

Subgoal 2.1:

Variables: L1 B K1
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H3 : is_o B
H4 : adj K1 B L1 *
H5 : is_o B
H6 : is_list L1
H7 : is_list K1
H8 : perm K1 K1
============================
 perm (B :: K1) L1

Subgoal 2.2 is:
 perm (B :: K1) (B :: K2)

adj_same_result < search.

Subgoal 2.2:

Variables: A L1 B K1 K2
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H3 : is_o B
H4 : adj K1 A L1 *
H5 : is_o B
H6 : adj K2 A L1
============================
 perm (B :: K1) (B :: K2)

adj_same_result < apply IH to H4 H6.

Subgoal 2.2:

Variables: A L1 B K1 K2
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H3 : is_o B
H4 : adj K1 A L1 *
H5 : is_o B
H6 : adj K2 A L1
H7 : perm K1 K2
============================
 perm (B :: K1) (B :: K2)

adj_same_result < apply adj_1_is_list to H4.

Subgoal 2.2:

Variables: A L1 B K1 K2
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H3 : is_o B
H4 : adj K1 A L1 *
H5 : is_o B
H6 : adj K2 A L1
H7 : perm K1 K2
H8 : is_list K1
============================
 perm (B :: K1) (B :: K2)

adj_same_result < apply adj_1_is_list to H6.

Subgoal 2.2:

Variables: A L1 B K1 K2
IH : forall J K A L, adj J A L * -> adj K A L -> perm J K
H3 : is_o B
H4 : adj K1 A L1 *
H5 : is_o B
H6 : adj K2 A L1
H7 : perm K1 K2
H8 : is_list K1
H9 : is_list K2
============================
 perm (B :: K1) (B :: K2)

adj_same_result < search.
Proof completed.

Abella < Theorem adj_same_result_diff : 
forall J A K B L, adj J A L -> adj K B L -> A = B /\ perm J K \/
  (exists KK, adj KK A K).

============================
 forall J A K B L, adj J A L -> adj K B L -> A = B /\ perm J K \/
   (exists KK, adj KK A K)

adj_same_result_diff < induction on 1.

IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
============================
 forall J A K B L, adj J A L @ -> adj K B L -> A = B /\ perm J K \/
   (exists KK, adj KK A K)

adj_same_result_diff < intros.

Variables: J A K B L
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H1 : adj J A L @
H2 : adj K B L
============================
 A = B /\ perm J K \/ (exists KK, adj KK A K)

adj_same_result_diff < case H1.

Subgoal 1:

Variables: J A K B
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H2 : adj K B (A :: J)
H3 : is_o A
H4 : is_list J
============================
 A = B /\ perm J K \/ (exists KK, adj KK A K)

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/ (exists KK, adj KK A K)

adj_same_result_diff < case H2.

Subgoal 1.1:

Variables: J A
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : is_list J
============================
 A = A /\ perm J J \/ (exists KK, adj KK A J)

Subgoal 1.2 is:
 A = B /\ perm J (A :: K1) \/ (exists KK, adj KK A (A :: K1))

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/ (exists KK, adj KK A K)

adj_same_result_diff < apply perm_refl to H4.

Subgoal 1.1:

Variables: J A
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : is_list J
H7 : perm J J
============================
 A = A /\ perm J J \/ (exists KK, adj KK A J)

Subgoal 1.2 is:
 A = B /\ perm J (A :: K1) \/ (exists KK, adj KK A (A :: K1))

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/ (exists KK, adj KK A K)

adj_same_result_diff < search.

Subgoal 1.2:

Variables: J A B K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 B J
============================
 A = B /\ perm J (A :: K1) \/ (exists KK, adj KK A (A :: K1))

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/ (exists KK, adj KK A K)

adj_same_result_diff < right.

Subgoal 1.2:

Variables: J A B K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 B J
============================
 exists KK, adj KK A (A :: K1)

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/ (exists KK, adj KK A K)

adj_same_result_diff < witness K1.

Subgoal 1.2:

Variables: J A B K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 B J
============================
 adj K1 A (A :: K1)

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/ (exists KK, adj KK A K)

adj_same_result_diff < apply adj_1_is_list to H6.

Subgoal 1.2:

Variables: J A B K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 B J
H7 : is_list K1
============================
 adj K1 A (A :: K1)

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/ (exists KK, adj KK A K)

adj_same_result_diff < search.

Subgoal 2:

Variables: A K B L1 B1 K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H2 : adj K B (B1 :: L1)
H3 : is_o B1
H4 : adj K1 A L1 *
============================
 A = B /\ perm (B1 :: K1) K \/ (exists KK, adj KK A K)

adj_same_result_diff < case H2.

Subgoal 2.1:

Variables: A L1 B1 K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : is_list L1
============================
 A = B1 /\ perm (B1 :: K1) L1 \/ (exists KK, adj KK A L1)

Subgoal 2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/ (exists KK, adj KK A (B1 :: K2))

adj_same_result_diff < right.

Subgoal 2.1:

Variables: A L1 B1 K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : is_list L1
============================
 exists KK, adj KK A L1

Subgoal 2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/ (exists KK, adj KK A (B1 :: K2))

adj_same_result_diff < search.

Subgoal 2.2:

Variables: A B L1 B1 K1 K2
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : adj K2 B L1
============================
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/ (exists KK, adj KK A (B1 :: K2))

adj_same_result_diff < apply IH to H4 H6.

Subgoal 2.2:

Variables: A B L1 B1 K1 K2
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : adj K2 B L1
H7 : A = B /\ perm K1 K2 \/ (exists KK, adj KK A K2)
============================
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/ (exists KK, adj KK A (B1 :: K2))

adj_same_result_diff < case H7.

Subgoal 2.2.1:

Variables: B L1 B1 K1 K2
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o B1
H4 : adj K1 B L1 *
H5 : is_o B1
H6 : adj K2 B L1
H8 : perm K1 K2
============================
 B = B /\ perm (B1 :: K1) (B1 :: K2) \/ (exists KK, adj KK B (B1 :: K2))

Subgoal 2.2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/ (exists KK, adj KK A (B1 :: K2))

adj_same_result_diff < apply adj_1_is_list to H4.

Subgoal 2.2.1:

Variables: B L1 B1 K1 K2
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o B1
H4 : adj K1 B L1 *
H5 : is_o B1
H6 : adj K2 B L1
H8 : perm K1 K2
H9 : is_list K1
============================
 B = B /\ perm (B1 :: K1) (B1 :: K2) \/ (exists KK, adj KK B (B1 :: K2))

Subgoal 2.2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/ (exists KK, adj KK A (B1 :: K2))

adj_same_result_diff < apply adj_1_is_list to H6.

Subgoal 2.2.1:

Variables: B L1 B1 K1 K2
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o B1
H4 : adj K1 B L1 *
H5 : is_o B1
H6 : adj K2 B L1
H8 : perm K1 K2
H9 : is_list K1
H10 : is_list K2
============================
 B = B /\ perm (B1 :: K1) (B1 :: K2) \/ (exists KK, adj KK B (B1 :: K2))

Subgoal 2.2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/ (exists KK, adj KK A (B1 :: K2))

adj_same_result_diff < search.

Subgoal 2.2.2:

Variables: A B L1 B1 K1 K2 KK
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists KK, adj KK A K)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : adj K2 B L1
H8 : adj KK A K2
============================
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/ (exists KK, adj KK A (B1 :: K2))

adj_same_result_diff < search.
Proof completed.

Abella < Theorem adj_same_result_diff_both : 
forall J A K B L, adj J A L -> adj K B L -> A = B /\ perm J K \/
  (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK).

============================
 forall J A K B L, adj J A L -> adj K B L -> A = B /\ perm J K \/
   (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < induction on 1.

IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
============================
 forall J A K B L, adj J A L @ -> adj K B L -> A = B /\ perm J K \/
   (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < intros.

Variables: J A K B L
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H1 : adj J A L @
H2 : adj K B L
============================
 A = B /\ perm J K \/ (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < case H1.

Subgoal 1:

Variables: J A K B
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H2 : adj K B (A :: J)
H3 : is_o A
H4 : is_list J
============================
 A = B /\ perm J K \/ (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < case H2.

Subgoal 1.1:

Variables: J A
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : is_list J
============================
 A = A /\ perm J J \/ (exists JJ KK, adj JJ A J /\ adj KK A J /\ perm JJ KK)

Subgoal 1.2 is:
 A = B /\ perm J (A :: K1) \/
   (exists JJ KK, adj JJ B J /\ adj KK A (A :: K1) /\ perm JJ KK)

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < apply perm_refl to H4.

Subgoal 1.1:

Variables: J A
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : is_list J
H7 : perm J J
============================
 A = A /\ perm J J \/ (exists JJ KK, adj JJ A J /\ adj KK A J /\ perm JJ KK)

Subgoal 1.2 is:
 A = B /\ perm J (A :: K1) \/
   (exists JJ KK, adj JJ B J /\ adj KK A (A :: K1) /\ perm JJ KK)

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < search.

Subgoal 1.2:

Variables: J A B K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 B J
============================
 A = B /\ perm J (A :: K1) \/
   (exists JJ KK, adj JJ B J /\ adj KK A (A :: K1) /\ perm JJ KK)

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < right.

Subgoal 1.2:

Variables: J A B K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 B J
============================
 exists JJ KK, adj JJ B J /\ adj KK A (A :: K1) /\ perm JJ KK

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < witness K1, K1.

Subgoal 1.2:

Variables: J A B K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 B J
============================
 adj K1 B J /\ adj K1 A (A :: K1) /\ perm K1 K1

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < apply adj_1_is_list to H6.

Subgoal 1.2:

Variables: J A B K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 B J
H7 : is_list K1
============================
 adj K1 B J /\ adj K1 A (A :: K1) /\ perm K1 K1

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < apply perm_refl to H7.

Subgoal 1.2:

Variables: J A B K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o A
H4 : is_list J
H5 : is_o A
H6 : adj K1 B J
H7 : is_list K1
H8 : perm K1 K1
============================
 adj K1 B J /\ adj K1 A (A :: K1) /\ perm K1 K1

Subgoal 2 is:
 A = B /\ perm (B1 :: K1) K \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < search.

Subgoal 2:

Variables: A K B L1 B1 K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H2 : adj K B (B1 :: L1)
H3 : is_o B1
H4 : adj K1 A L1 *
============================
 A = B /\ perm (B1 :: K1) K \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A K /\ perm JJ KK)

adj_same_result_diff_both < case H2.

Subgoal 2.1:

Variables: A L1 B1 K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : is_list L1
============================
 A = B1 /\ perm (B1 :: K1) L1 \/
   (exists JJ KK, adj JJ B1 (B1 :: K1) /\ adj KK A L1 /\ perm JJ KK)

Subgoal 2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < right.

Subgoal 2.1:

Variables: A L1 B1 K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : is_list L1
============================
 exists JJ KK, adj JJ B1 (B1 :: K1) /\ adj KK A L1 /\ perm JJ KK

Subgoal 2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < apply adj_1_is_list to H4.

Subgoal 2.1:

Variables: A L1 B1 K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : is_list L1
H7 : is_list K1
============================
 exists JJ KK, adj JJ B1 (B1 :: K1) /\ adj KK A L1 /\ perm JJ KK

Subgoal 2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < apply perm_refl to H7.

Subgoal 2.1:

Variables: A L1 B1 K1
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : is_list L1
H7 : is_list K1
H8 : perm K1 K1
============================
 exists JJ KK, adj JJ B1 (B1 :: K1) /\ adj KK A L1 /\ perm JJ KK

Subgoal 2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < search.

Subgoal 2.2:

Variables: A B L1 B1 K1 K2
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : adj K2 B L1
============================
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < apply IH to H4 H6.

Subgoal 2.2:

Variables: A B L1 B1 K1 K2
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : adj K2 B L1
H7 : A = B /\ perm K1 K2 \/
       (exists JJ KK, adj JJ B K1 /\ adj KK A K2 /\ perm JJ KK)
============================
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < case H7.

Subgoal 2.2.1:

Variables: B L1 B1 K1 K2
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 B L1 *
H5 : is_o B1
H6 : adj K2 B L1
H8 : perm K1 K2
============================
 B = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK B (B1 :: K2) /\ perm JJ KK)

Subgoal 2.2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < apply adj_1_is_list to H4.

Subgoal 2.2.1:

Variables: B L1 B1 K1 K2
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 B L1 *
H5 : is_o B1
H6 : adj K2 B L1
H8 : perm K1 K2
H9 : is_list K1
============================
 B = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK B (B1 :: K2) /\ perm JJ KK)

Subgoal 2.2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < apply adj_1_is_list to H6.

Subgoal 2.2.1:

Variables: B L1 B1 K1 K2
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 B L1 *
H5 : is_o B1
H6 : adj K2 B L1
H8 : perm K1 K2
H9 : is_list K1
H10 : is_list K2
============================
 B = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK B (B1 :: K2) /\ perm JJ KK)

Subgoal 2.2.2 is:
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < search.

Subgoal 2.2.2:

Variables: A B L1 B1 K1 K2 JJ KK
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : adj K2 B L1
H8 : adj JJ B K1
H9 : adj KK A K2
H10 : perm JJ KK
============================
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < apply perm_1_is_list to H10.

Subgoal 2.2.2:

Variables: A B L1 B1 K1 K2 JJ KK
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : adj K2 B L1
H8 : adj JJ B K1
H9 : adj KK A K2
H10 : perm JJ KK
H11 : is_list JJ
============================
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < apply perm_2_is_list to H10.

Subgoal 2.2.2:

Variables: A B L1 B1 K1 K2 JJ KK
IH : forall J A K B L, adj J A L * -> adj K B L -> A = B /\ perm J K \/
       (exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK)
H3 : is_o B1
H4 : adj K1 A L1 *
H5 : is_o B1
H6 : adj K2 B L1
H8 : adj JJ B K1
H9 : adj KK A K2
H10 : perm JJ KK
H11 : is_list JJ
H12 : is_list KK
============================
 A = B /\ perm (B1 :: K1) (B1 :: K2) \/
   (exists JJ KK, adj JJ B (B1 :: K1) /\ adj KK A (B1 :: K2) /\ perm JJ KK)

adj_same_result_diff_both < search.
Proof completed.

Abella < Theorem perm_invert : 
forall A J K JJ KK, perm J K -> adj JJ A J -> adj KK A K -> perm JJ KK.

============================
 forall A J K JJ KK, perm J K -> adj JJ A J -> adj KK A K -> perm JJ KK

perm_invert < induction on 1.

IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
============================
 forall A J K JJ KK, perm J K @ -> adj JJ A J -> adj KK A K -> perm JJ KK

perm_invert < intros.

Variables: A J K JJ KK
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H1 : perm J K @
H2 : adj JJ A J
H3 : adj KK A K
============================
 perm JJ KK

perm_invert < case H1.

Subgoal 1:

Variables: A JJ KK
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A nil
H3 : adj KK A nil
============================
 perm JJ KK

Subgoal 2 is:
 perm JJ KK

perm_invert < case H2.

Subgoal 2:

Variables: A J K JJ KK A1 KK1 LL
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A J
H3 : adj KK A K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
============================
 perm JJ KK

perm_invert < apply adj_same_result_diff to H2 H4.

Subgoal 2:

Variables: A J K JJ KK A1 KK1 LL
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A J
H3 : adj KK A K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H7 : A = A1 /\ perm JJ KK1 \/ (exists KK, adj KK A KK1)
============================
 perm JJ KK

perm_invert < case H7.

Subgoal 2.1:

Variables: J K JJ KK A1 KK1 LL
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H8 : perm JJ KK1
============================
 perm JJ KK

Subgoal 2.2 is:
 perm JJ KK

perm_invert < apply adj_same_result_diff to H3 H5.

Subgoal 2.1:

Variables: J K JJ KK A1 KK1 LL
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H8 : perm JJ KK1
H9 : A1 = A1 /\ perm KK LL \/ (exists KK1, adj KK1 A1 LL)
============================
 perm JJ KK

Subgoal 2.2 is:
 perm JJ KK

perm_invert < case H9.

Subgoal 2.1.1:

Variables: J K JJ KK A1 KK1 LL
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H8 : perm JJ KK1
H10 : perm KK LL
============================
 perm JJ KK

Subgoal 2.1.2 is:
 perm JJ KK

Subgoal 2.2 is:
 perm JJ KK

perm_invert < apply perm_trans to *H8 *H6.

Subgoal 2.1.1:

Variables: J K JJ KK A1 KK1 LL
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H10 : perm KK LL
H11 : perm JJ LL
============================
 perm JJ KK

Subgoal 2.1.2 is:
 perm JJ KK

Subgoal 2.2 is:
 perm JJ KK

perm_invert < apply perm_sym to *H10.

Subgoal 2.1.1:

Variables: J K JJ KK A1 KK1 LL
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H11 : perm JJ LL
H12 : perm LL KK
============================
 perm JJ KK

Subgoal 2.1.2 is:
 perm JJ KK

Subgoal 2.2 is:
 perm JJ KK

perm_invert < backchain perm_trans.

Subgoal 2.1.2:

Variables: J K JJ KK A1 KK1 LL KK2
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H8 : perm JJ KK1
H10 : adj KK2 A1 LL
============================
 perm JJ KK

Subgoal 2.2 is:
 perm JJ KK

perm_invert < apply adj_same_result to H3 H5.

Subgoal 2.1.2:

Variables: J K JJ KK A1 KK1 LL KK2
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H8 : perm JJ KK1
H10 : adj KK2 A1 LL
H11 : perm KK LL
============================
 perm JJ KK

Subgoal 2.2 is:
 perm JJ KK

perm_invert < apply perm_trans to *H8 *H6.

Subgoal 2.1.2:

Variables: J K JJ KK A1 KK1 LL KK2
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H10 : adj KK2 A1 LL
H11 : perm KK LL
H12 : perm JJ LL
============================
 perm JJ KK

Subgoal 2.2 is:
 perm JJ KK

perm_invert < apply perm_sym to *H11.

Subgoal 2.1.2:

Variables: J K JJ KK A1 KK1 LL KK2
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H10 : adj KK2 A1 LL
H12 : perm JJ LL
H13 : perm LL KK
============================
 perm JJ KK

Subgoal 2.2 is:
 perm JJ KK

perm_invert < backchain perm_trans.

Subgoal 2.2:

Variables: A J K JJ KK A1 KK1 LL KK2
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A J
H3 : adj KK A K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H8 : adj KK2 A KK1
============================
 perm JJ KK

perm_invert < apply adj_same_result_diff to H3 H5.

Subgoal 2.2:

Variables: A J K JJ KK A1 KK1 LL KK2
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A J
H3 : adj KK A K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H8 : adj KK2 A KK1
H9 : A = A1 /\ perm KK LL \/ (exists KK1, adj KK1 A LL)
============================
 perm JJ KK

perm_invert < case H9.

Subgoal 2.2.1:

Variables: J K JJ KK A1 KK1 LL KK2
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H8 : adj KK2 A1 KK1
H10 : perm KK LL
============================
 perm JJ KK

Subgoal 2.2.2 is:
 perm JJ KK

perm_invert < apply perm_sym to *H10.

Subgoal 2.2.1:

Variables: J K JJ KK A1 KK1 LL KK2
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H8 : adj KK2 A1 KK1
H11 : perm LL KK
============================
 perm JJ KK

Subgoal 2.2.2 is:
 perm JJ KK

perm_invert < apply perm_trans to *H6 *H11.

Subgoal 2.2.1:

Variables: J K JJ KK A1 KK1 LL KK2
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H8 : adj KK2 A1 KK1
H12 : perm KK1 KK
============================
 perm JJ KK

Subgoal 2.2.2 is:
 perm JJ KK

perm_invert < apply adj_same_result to H2 H4.

Subgoal 2.2.1:

Variables: J K JJ KK A1 KK1 LL KK2
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A1 J
H3 : adj KK A1 K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H8 : adj KK2 A1 KK1
H12 : perm KK1 KK
H13 : perm JJ KK1
============================
 perm JJ KK

Subgoal 2.2.2 is:
 perm JJ KK

perm_invert < backchain perm_trans.

Subgoal 2.2.2:

Variables: A J K JJ KK A1 KK1 LL KK2 KK3
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A J
H3 : adj KK A K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H8 : adj KK2 A KK1
H10 : adj KK3 A LL
============================
 perm JJ KK

perm_invert < apply IH to H6 H8 H10.

Subgoal 2.2.2:

Variables: A J K JJ KK A1 KK1 LL KK2 KK3
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A J
H3 : adj KK A K
H4 : adj KK1 A1 J
H5 : adj LL A1 K
H6 : perm KK1 LL *
H8 : adj KK2 A KK1
H10 : adj KK3 A LL
H11 : perm KK2 KK3
============================
 perm JJ KK

perm_invert < apply adj_swap to *H10 *H5.

Subgoal 2.2.2:

Variables: A J K JJ KK A1 KK1 LL KK2 KK3 U
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A J
H3 : adj KK A K
H4 : adj KK1 A1 J
H6 : perm KK1 LL *
H8 : adj KK2 A KK1
H11 : perm KK2 KK3
H12 : adj KK3 A1 U
H13 : adj U A K
============================
 perm JJ KK

perm_invert < apply adj_swap to *H8 *H4.

Subgoal 2.2.2:

Variables: A J K JJ KK A1 KK1 LL KK2 KK3 U U1
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H2 : adj JJ A J
H3 : adj KK A K
H6 : perm KK1 LL *
H11 : perm KK2 KK3
H12 : adj KK3 A1 U
H13 : adj U A K
H14 : adj KK2 A1 U1
H15 : adj U1 A J
============================
 perm JJ KK

perm_invert < apply adj_same_result to *H2 *H15.

Subgoal 2.2.2:

Variables: A J K JJ KK A1 KK1 LL KK2 KK3 U U1
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H3 : adj KK A K
H6 : perm KK1 LL *
H11 : perm KK2 KK3
H12 : adj KK3 A1 U
H13 : adj U A K
H14 : adj KK2 A1 U1
H16 : perm JJ U1
============================
 perm JJ KK

perm_invert < apply adj_same_result to *H13 *H3.

Subgoal 2.2.2:

Variables: A J K JJ KK A1 KK1 LL KK2 KK3 U U1
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H6 : perm KK1 LL *
H11 : perm KK2 KK3
H12 : adj KK3 A1 U
H14 : adj KK2 A1 U1
H16 : perm JJ U1
H17 : perm U KK
============================
 perm JJ KK

perm_invert < apply adj_preserves_perm to *H14 *H12 *H11.

Subgoal 2.2.2:

Variables: A J K JJ KK A1 KK1 LL KK2 KK3 U U1
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H6 : perm KK1 LL *
H16 : perm JJ U1
H17 : perm U KK
H18 : perm U1 U
============================
 perm JJ KK

perm_invert < apply perm_trans to *H16 *H18.

Subgoal 2.2.2:

Variables: A J K JJ KK A1 KK1 LL KK2 KK3 U U1
IH : forall A J K JJ KK, perm J K * -> adj JJ A J -> adj KK A K -> perm JJ KK
H6 : perm KK1 LL *
H17 : perm U KK
H19 : perm JJ U
============================
 perm JJ KK

perm_invert < backchain perm_trans.
Proof completed.

Abella < Theorem adj_perm_result : 
forall J K A JJ, perm J K -> adj JJ A J ->
  (exists KK, adj KK A K /\ perm JJ KK).

============================
 forall J K A JJ, perm J K -> adj JJ A J ->
   (exists KK, adj KK A K /\ perm JJ KK)

adj_perm_result < induction on 1.

IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
============================
 forall J K A JJ, perm J K @ -> adj JJ A J ->
   (exists KK, adj KK A K /\ perm JJ KK)

adj_perm_result < intros.

Variables: J K A JJ
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H1 : perm J K @
H2 : adj JJ A J
============================
 exists KK, adj KK A K /\ perm JJ KK

adj_perm_result < case H1.

Subgoal 1:

Variables: A JJ
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A nil
============================
 exists KK, adj KK A nil /\ perm JJ KK

Subgoal 2 is:
 exists KK, adj KK A K /\ perm JJ KK

adj_perm_result < case H2.

Subgoal 2:

Variables: J K A JJ A1 KK LL
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
============================
 exists KK, adj KK A K /\ perm JJ KK

adj_perm_result < apply adj_same_result_diff to H2 H3.

Subgoal 2:

Variables: J K A JJ A1 KK LL
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H6 : A = A1 /\ perm JJ KK \/ (exists KK1, adj KK1 A KK)
============================
 exists KK, adj KK A K /\ perm JJ KK

adj_perm_result < case H6.

Subgoal 2.1:

Variables: J K JJ A1 KK LL
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A1 J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H7 : perm JJ KK
============================
 exists KK, adj KK A1 K /\ perm JJ KK

Subgoal 2.2 is:
 exists KK, adj KK A K /\ perm JJ KK

adj_perm_result < apply perm_trans to H7 H5.

Subgoal 2.1:

Variables: J K JJ A1 KK LL
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A1 J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H7 : perm JJ KK
H8 : perm JJ LL
============================
 exists KK, adj KK A1 K /\ perm JJ KK

Subgoal 2.2 is:
 exists KK, adj KK A K /\ perm JJ KK

adj_perm_result < search.

Subgoal 2.2:

Variables: J K A JJ A1 KK LL KK1
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H7 : adj KK1 A KK
============================
 exists KK, adj KK A K /\ perm JJ KK

adj_perm_result < apply IH to H5 H7.

Subgoal 2.2:

Variables: J K A JJ A1 KK LL KK1 KK2
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H7 : adj KK1 A KK
H8 : adj KK2 A LL
H9 : perm KK1 KK2
============================
 exists KK, adj KK A K /\ perm JJ KK

adj_perm_result < apply adj_swap to H7 H3.

Subgoal 2.2:

Variables: J K A JJ A1 KK LL KK1 KK2 U
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H7 : adj KK1 A KK
H8 : adj KK2 A LL
H9 : perm KK1 KK2
H10 : adj KK1 A1 U
H11 : adj U A J
============================
 exists KK, adj KK A K /\ perm JJ KK

adj_perm_result < apply adj_swap to H8 H4.

Subgoal 2.2:

Variables: J K A JJ A1 KK LL KK1 KK2 U U1
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H7 : adj KK1 A KK
H8 : adj KK2 A LL
H9 : perm KK1 KK2
H10 : adj KK1 A1 U
H11 : adj U A J
H12 : adj KK2 A1 U1
H13 : adj U1 A K
============================
 exists KK, adj KK A K /\ perm JJ KK

adj_perm_result < witness U1.

Subgoal 2.2:

Variables: J K A JJ A1 KK LL KK1 KK2 U U1
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H7 : adj KK1 A KK
H8 : adj KK2 A LL
H9 : perm KK1 KK2
H10 : adj KK1 A1 U
H11 : adj U A J
H12 : adj KK2 A1 U1
H13 : adj U1 A K
============================
 adj U1 A K /\ perm JJ U1

adj_perm_result < split.

Subgoal 2.2.1:

Variables: J K A JJ A1 KK LL KK1 KK2 U U1
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H7 : adj KK1 A KK
H8 : adj KK2 A LL
H9 : perm KK1 KK2
H10 : adj KK1 A1 U
H11 : adj U A J
H12 : adj KK2 A1 U1
H13 : adj U1 A K
============================
 adj U1 A K

Subgoal 2.2.2 is:
 perm JJ U1

adj_perm_result < search.

Subgoal 2.2.2:

Variables: J K A JJ A1 KK LL KK1 KK2 U U1
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H7 : adj KK1 A KK
H8 : adj KK2 A LL
H9 : perm KK1 KK2
H10 : adj KK1 A1 U
H11 : adj U A J
H12 : adj KK2 A1 U1
H13 : adj U1 A K
============================
 perm JJ U1

adj_perm_result < apply adj_same_result to H2 H11.

Subgoal 2.2.2:

Variables: J K A JJ A1 KK LL KK1 KK2 U U1
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H7 : adj KK1 A KK
H8 : adj KK2 A LL
H9 : perm KK1 KK2
H10 : adj KK1 A1 U
H11 : adj U A J
H12 : adj KK2 A1 U1
H13 : adj U1 A K
H14 : perm JJ U
============================
 perm JJ U1

adj_perm_result < apply adj_preserves_perm to H10 H12 H9.

Subgoal 2.2.2:

Variables: J K A JJ A1 KK LL KK1 KK2 U U1
IH : forall J K A JJ, perm J K * -> adj JJ A J ->
       (exists KK, adj KK A K /\ perm JJ KK)
H2 : adj JJ A J
H3 : adj KK A1 J
H4 : adj LL A1 K
H5 : perm KK LL *
H7 : adj KK1 A KK
H8 : adj KK2 A LL
H9 : perm KK1 KK2
H10 : adj KK1 A1 U
H11 : adj U A J
H12 : adj KK2 A1 U1
H13 : adj U1 A K
H14 : perm JJ U
H15 : perm U U1
============================
 perm JJ U1

adj_perm_result < backchain perm_trans.
Proof completed.

Abella < Theorem adj_perm_source : 
forall J K A L, perm J K -> adj J A L -> (exists LL, adj K A LL /\ perm L LL).

============================
 forall J K A L, perm J K -> adj J A L ->
   (exists LL, adj K A LL /\ perm L LL)

adj_perm_source < intros.

Variables: J K A L
H1 : perm J K
H2 : adj J A L
============================
 exists LL, adj K A LL /\ perm L LL

adj_perm_source < apply adj_2_is_o to H2.

Variables: J K A L
H1 : perm J K
H2 : adj J A L
H3 : is_o A
============================
 exists LL, adj K A LL /\ perm L LL

adj_perm_source < apply perm_2_is_list to H1.

Variables: J K A L
H1 : perm J K
H2 : adj J A L
H3 : is_o A
H4 : is_list K
============================
 exists LL, adj K A LL /\ perm L LL

adj_perm_source < apply adj_exists to H3 H4.

Variables: J K A L M
H1 : perm J K
H2 : adj J A L
H3 : is_o A
H4 : is_list K
H5 : adj K A M
============================
 exists LL, adj K A LL /\ perm L LL

adj_perm_source < search.
Proof completed.

Abella < Theorem adj_nil_1 : 
forall A L, adj nil A L -> L = A :: nil.

============================
 forall A L, adj nil A L -> L = A :: nil

adj_nil_1 < intros.

Variables: A L
H1 : adj nil A L
============================
 L = A :: nil

adj_nil_1 < case H1.

Variables: A
H2 : is_o A
H3 : is_list nil
============================
 A :: nil = A :: nil

adj_nil_1 < search.
Proof completed.

Abella < Theorem perm_nil_1 : 
forall L, perm nil L -> L = nil.

============================
 forall L, perm nil L -> L = nil

perm_nil_1 < intros.

Variables: L
H1 : perm nil L
============================
 L = nil

perm_nil_1 < case H1.

Subgoal 1:

============================
 nil = nil

Subgoal 2 is:
 L = nil

perm_nil_1 < search.

Subgoal 2:

Variables: L A KK LL
H2 : adj KK A nil
H3 : adj LL A L
H4 : perm KK LL
============================
 L = nil

perm_nil_1 < case H2.
Proof completed.

Abella < Theorem adj_det : 
forall A B L, adj L A (B :: nil) -> A = B /\ L = nil.

============================
 forall A B L, adj L A (B :: nil) -> A = B /\ L = nil

adj_det < intros.

Variables: A B L
H1 : adj L A (B :: nil)
============================
 A = B /\ L = nil

adj_det < case H1.

Subgoal 1:

Variables: B
H2 : is_o B
H3 : is_list nil
============================
 B = B /\ nil = nil

Subgoal 2 is:
 A = B /\ B :: K = nil

adj_det < search.

Subgoal 2:

Variables: A B K
H2 : is_o B
H3 : adj K A nil
============================
 A = B /\ B :: K = nil

adj_det < case H3.
Proof completed.

Abella < Theorem perm_singleton : 
forall A L, perm (A :: nil) L -> L = A :: nil.

============================
 forall A L, perm (A :: nil) L -> L = A :: nil

perm_singleton < intros.

Variables: A L
H1 : perm (A :: nil) L
============================
 L = A :: nil

perm_singleton < case H1.

Variables: A L A1 KK LL
H2 : adj KK A1 (A :: nil)
H3 : adj LL A1 L
H4 : perm KK LL
============================
 L = A :: nil

perm_singleton < apply adj_det to H2.

Variables: A L LL
H2 : adj nil A (A :: nil)
H3 : adj LL A L
H4 : perm nil LL
============================
 L = A :: nil

perm_singleton < apply perm_nil_1 to H4.

Variables: A L
H2 : adj nil A (A :: nil)
H3 : adj nil A L
H4 : perm nil nil
============================
 L = A :: nil

perm_singleton < apply adj_nil_1 to H3.

Variables: A
H2 : adj nil A (A :: nil)
H3 : adj nil A (A :: nil)
H4 : perm nil nil
============================
 A :: nil = A :: nil

perm_singleton < search.
Proof completed.

Abella < Theorem append_perm : 
forall J K L JJ KK, append J K L -> perm J JJ -> perm K KK ->
  (exists LL, append JJ KK LL /\ perm L LL).

============================
 forall J K L JJ KK, append J K L -> perm J JJ -> perm K KK ->
   (exists LL, append JJ KK LL /\ perm L LL)

append_perm < induction on 1.

IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
============================
 forall J K L JJ KK, append J K L @ -> perm J JJ -> perm K KK ->
   (exists LL, append JJ KK LL /\ perm L LL)

append_perm < intros.

Variables: J K L JJ KK
IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
H1 : append J K L @
H2 : perm J JJ
H3 : perm K KK
============================
 exists LL, append JJ KK LL /\ perm L LL

append_perm < case H1.

Subgoal 1:

Variables: L JJ KK
IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
H2 : perm nil JJ
H3 : perm L KK
H4 : is_list L
============================
 exists LL, append JJ KK LL /\ perm L LL

Subgoal 2 is:
 exists LL, append JJ KK LL /\ perm (A :: L1) LL

append_perm < case H2.

Subgoal 1.1:

Variables: L KK
IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
H3 : perm L KK
H4 : is_list L
============================
 exists LL, append nil KK LL /\ perm L LL

Subgoal 1.2 is:
 exists LL, append JJ KK LL /\ perm L LL

Subgoal 2 is:
 exists LL, append JJ KK LL /\ perm (A :: L1) LL

append_perm < apply perm_2_is_list to H3.

Subgoal 1.1:

Variables: L KK
IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
H3 : perm L KK
H4 : is_list L
H5 : is_list KK
============================
 exists LL, append nil KK LL /\ perm L LL

Subgoal 1.2 is:
 exists LL, append JJ KK LL /\ perm L LL

Subgoal 2 is:
 exists LL, append JJ KK LL /\ perm (A :: L1) LL

append_perm < search.

Subgoal 1.2:

Variables: L JJ KK A KK1 LL
IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
H3 : perm L KK
H4 : is_list L
H5 : adj KK1 A nil
H6 : adj LL A JJ
H7 : perm KK1 LL
============================
 exists LL, append JJ KK LL /\ perm L LL

Subgoal 2 is:
 exists LL, append JJ KK LL /\ perm (A :: L1) LL

append_perm < case H5.

Subgoal 2:

Variables: K JJ KK L1 A J1
IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
H2 : perm (A :: J1) JJ
H3 : perm K KK
H4 : is_o A
H5 : append J1 K L1 *
============================
 exists LL, append JJ KK LL /\ perm (A :: L1) LL

append_perm < apply perm_cons_1 to *H2.

Subgoal 2:

Variables: K JJ KK L1 A J1 J2
IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
H3 : perm K KK
H4 : is_o A
H5 : append J1 K L1 *
H6 : adj J2 A JJ
H7 : perm J1 J2
============================
 exists LL, append JJ KK LL /\ perm (A :: L1) LL

append_perm < apply IH to H5 H7 H3.

Subgoal 2:

Variables: K JJ KK L1 A J1 J2 LL
IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
H3 : perm K KK
H4 : is_o A
H5 : append J1 K L1 *
H6 : adj J2 A JJ
H7 : perm J1 J2
H8 : append J2 KK LL
H9 : perm L1 LL
============================
 exists LL, append JJ KK LL /\ perm (A :: L1) LL

append_perm < apply adj_1_append to H6 H8.

Subgoal 2:

Variables: K JJ KK L1 A J1 J2 LL KL
IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
H3 : perm K KK
H4 : is_o A
H5 : append J1 K L1 *
H6 : adj J2 A JJ
H7 : perm J1 J2
H8 : append J2 KK LL
H9 : perm L1 LL
H10 : append JJ KK KL
H11 : adj LL A KL
============================
 exists LL, append JJ KK LL /\ perm (A :: L1) LL

append_perm < apply adj_3_is_list to H11.

Subgoal 2:

Variables: K JJ KK L1 A J1 J2 LL KL
IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
H3 : perm K KK
H4 : is_o A
H5 : append J1 K L1 *
H6 : adj J2 A JJ
H7 : perm J1 J2
H8 : append J2 KK LL
H9 : perm L1 LL
H10 : append JJ KK KL
H11 : adj LL A KL
H12 : is_list KL
============================
 exists LL, append JJ KK LL /\ perm (A :: L1) LL

append_perm < apply perm_1_is_list to H9.

Subgoal 2:

Variables: K JJ KK L1 A J1 J2 LL KL
IH : forall J K L JJ KK, append J K L * -> perm J JJ -> perm K KK ->
       (exists LL, append JJ KK LL /\ perm L LL)
H3 : perm K KK
H4 : is_o A
H5 : append J1 K L1 *
H6 : adj J2 A JJ
H7 : perm J1 J2
H8 : append J2 KK LL
H9 : perm L1 LL
H10 : append JJ KK KL
H11 : adj LL A KL
H12 : is_list KL
H13 : is_list L1
============================
 exists LL, append JJ KK LL /\ perm (A :: L1) LL

append_perm < search.
Proof completed.

Abella < Theorem adj_perm : 
forall J K JJ A, perm J K -> adj JJ A J -> (exists KK, adj KK A K).

============================
 forall J K JJ A, perm J K -> adj JJ A J -> (exists KK, adj KK A K)

adj_perm < induction on 2.

IH : forall J K JJ A, perm J K -> adj JJ A J * -> (exists KK, adj KK A K)
============================
 forall J K JJ A, perm J K -> adj JJ A J @ -> (exists KK, adj KK A K)

adj_perm < intros.

Variables: J K JJ A
IH : forall J K JJ A, perm J K -> adj JJ A J * -> (exists KK, adj KK A K)
H1 : perm J K
H2 : adj JJ A J @
============================
 exists KK, adj KK A K

adj_perm < case H2.

Subgoal 1:

Variables: K JJ A
IH : forall J K JJ A, perm J K -> adj JJ A J * -> (exists KK, adj KK A K)
H1 : perm (A :: JJ) K
H3 : is_o A
H4 : is_list JJ
============================
 exists KK, adj KK A K

Subgoal 2 is:
 exists KK, adj KK A K

adj_perm < apply perm_cons_1 to *H1.

Subgoal 1:

Variables: K JJ A J1
IH : forall J K JJ A, perm J K -> adj JJ A J * -> (exists KK, adj KK A K)
H3 : is_o A
H4 : is_list JJ
H5 : adj J1 A K
H6 : perm JJ J1
============================
 exists KK, adj KK A K

Subgoal 2 is:
 exists KK, adj KK A K

adj_perm < search.

Subgoal 2:

Variables: K A L B K1
IH : forall J K JJ A, perm J K -> adj JJ A J * -> (exists KK, adj KK A K)
H1 : perm (B :: L) K
H3 : is_o B
H4 : adj K1 A L *
============================
 exists KK, adj KK A K

adj_perm < apply perm_cons_1 to *H1.

Subgoal 2:

Variables: K A L B K1 J1
IH : forall J K JJ A, perm J K -> adj JJ A J * -> (exists KK, adj KK A K)
H3 : is_o B
H4 : adj K1 A L *
H5 : adj J1 B K
H6 : perm L J1
============================
 exists KK, adj KK A K

adj_perm < apply IH to H6 H4.

Subgoal 2:

Variables: K A L B K1 J1 KK
IH : forall J K JJ A, perm J K -> adj JJ A J * -> (exists KK, adj KK A K)
H3 : is_o B
H4 : adj K1 A L *
H5 : adj J1 B K
H6 : perm L J1
H7 : adj KK A J1
============================
 exists KK, adj KK A K

adj_perm < apply adj_swap to H7 H5.

Subgoal 2:

Variables: K A L B K1 J1 KK U
IH : forall J K JJ A, perm J K -> adj JJ A J * -> (exists KK, adj KK A K)
H3 : is_o B
H4 : adj K1 A L *
H5 : adj J1 B K
H6 : perm L J1
H7 : adj KK A J1
H8 : adj KK B U
H9 : adj U A K
============================
 exists KK, adj KK A K

adj_perm < search.
Proof completed.

Abella < Theorem adj_perm_full : 
forall J K JJ A, perm J K -> adj JJ A J ->
  (exists KK, adj KK A K /\ perm JJ KK).

============================
 forall J K JJ A, perm J K -> adj JJ A J ->
   (exists KK, adj KK A K /\ perm JJ KK)

adj_perm_full < induction on 2.

IH : forall J K JJ A, perm J K -> adj JJ A J * ->
       (exists KK, adj KK A K /\ perm JJ KK)
============================
 forall J K JJ A, perm J K -> adj JJ A J @ ->
   (exists KK, adj KK A K /\ perm JJ KK)

adj_perm_full < intros.

Variables: J K JJ A
IH : forall J K JJ A, perm J K -> adj JJ A J * ->
       (exists KK, adj KK A K /\ perm JJ KK)
H1 : perm J K
H2 : adj JJ A J @
============================
 exists KK, adj KK A K /\ perm JJ KK

adj_perm_full < case H2.

Subgoal 1:

Variables: K JJ A
IH : forall J K JJ A, perm J K -> adj JJ A J * ->
       (exists KK, adj KK A K /\ perm JJ KK)
H1 : perm (A :: JJ) K
H3 : is_o A
H4 : is_list JJ
============================
 exists KK, adj KK A K /\ perm JJ KK

Subgoal 2 is:
 exists KK, adj KK A K /\ perm (B :: K1) KK

adj_perm_full < apply perm_cons_1 to *H1.

Subgoal 1:

Variables: K JJ A J1
IH : forall J K JJ A, perm J K -> adj JJ A J * ->
       (exists KK, adj KK A K /\ perm JJ KK)
H3 : is_o A
H4 : is_list JJ
H5 : adj J1 A K
H6 : perm JJ J1
============================
 exists KK, adj KK A K /\ perm JJ KK

Subgoal 2 is:
 exists KK, adj KK A K /\ perm (B :: K1) KK

adj_perm_full < search.

Subgoal 2:

Variables: K A L B K1
IH : forall J K JJ A, perm J K -> adj JJ A J * ->
       (exists KK, adj KK A K /\ perm JJ KK)
H1 : perm (B :: L) K
H3 : is_o B
H4 : adj K1 A L *
============================
 exists KK, adj KK A K /\ perm (B :: K1) KK

adj_perm_full < apply perm_cons_1 to *H1.

Subgoal 2:

Variables: K A L B K1 J1
IH : forall J K JJ A, perm J K -> adj JJ A J * ->
       (exists KK, adj KK A K /\ perm JJ KK)
H3 : is_o B
H4 : adj K1 A L *
H5 : adj J1 B K
H6 : perm L J1
============================
 exists KK, adj KK A K /\ perm (B :: K1) KK

adj_perm_full < apply IH to H6 H4.

Subgoal 2:

Variables: K A L B K1 J1 KK
IH : forall J K JJ A, perm J K -> adj JJ A J * ->
       (exists KK, adj KK A K /\ perm JJ KK)
H3 : is_o B
H4 : adj K1 A L *
H5 : adj J1 B K
H6 : perm L J1
H7 : adj KK A J1
H8 : perm K1 KK
============================
 exists KK, adj KK A K /\ perm (B :: K1) KK

adj_perm_full < apply adj_swap to H7 H5.

Subgoal 2:

Variables: K A L B K1 J1 KK U
IH : forall J K JJ A, perm J K -> adj JJ A J * ->
       (exists KK, adj KK A K /\ perm JJ KK)
H3 : is_o B
H4 : adj K1 A L *
H5 : adj J1 B K
H6 : perm L J1
H7 : adj KK A J1
H8 : perm K1 KK
H9 : adj KK B U
H10 : adj U A K
============================
 exists KK, adj KK A K /\ perm (B :: K1) KK

adj_perm_full < apply adj_1_is_list to H4.

Subgoal 2:

Variables: K A L B K1 J1 KK U
IH : forall J K JJ A, perm J K -> adj JJ A J * ->
       (exists KK, adj KK A K /\ perm JJ KK)
H3 : is_o B
H4 : adj K1 A L *
H5 : adj J1 B K
H6 : perm L J1
H7 : adj KK A J1
H8 : perm K1 KK
H9 : adj KK B U
H10 : adj U A K
H11 : is_list K1
============================
 exists KK, adj KK A K /\ perm (B :: K1) KK

adj_perm_full < search.
Proof completed.

Abella < Theorem adj_member : 
forall J A L, adj J A L -> member A L.

============================
 forall J A L, adj J A L -> member A L

adj_member < induction on 1.

IH : forall J A L, adj J A L * -> member A L
============================
 forall J A L, adj J A L @ -> member A L

adj_member < intros.

Variables: J A L
IH : forall J A L, adj J A L * -> member A L
H1 : adj J A L @
============================
 member A L

adj_member < case H1.

Subgoal 1:

Variables: J A
IH : forall J A L, adj J A L * -> member A L
H2 : is_o A
H3 : is_list J
============================
 member A (A :: J)

Subgoal 2 is:
 member A (B :: L1)

adj_member < search.

Subgoal 2:

Variables: A L1 B K
IH : forall J A L, adj J A L * -> member A L
H2 : is_o B
H3 : adj K A L1 *
============================
 member A (B :: L1)

adj_member < apply IH to H3.

Subgoal 2:

Variables: A L1 B K
IH : forall J A L, adj J A L * -> member A L
H2 : is_o B
H3 : adj K A L1 *
H4 : member A L1
============================
 member A (B :: L1)

adj_member < search.
Proof completed.

Abella < Theorem member_adj : 
forall A L, is_list L -> member A L -> (exists J, adj J A L).

============================
 forall A L, is_list L -> member A L -> (exists J, adj J A L)

member_adj < induction on 2.

IH : forall A L, is_list L -> member A L * -> (exists J, adj J A L)
============================
 forall A L, is_list L -> member A L @ -> (exists J, adj J A L)

member_adj < intros.

Variables: A L
IH : forall A L, is_list L -> member A L * -> (exists J, adj J A L)
H1 : is_list L
H2 : member A L @
============================
 exists J, adj J A L

member_adj < case H2.

Subgoal 1:

Variables: A L1
IH : forall A L, is_list L -> member A L * -> (exists J, adj J A L)
H1 : is_list (A :: L1)
============================
 exists J, adj J A (A :: L1)

Subgoal 2 is:
 exists J, adj J A (B :: L1)

member_adj < case H1.

Subgoal 1:

Variables: A L1
IH : forall A L, is_list L -> member A L * -> (exists J, adj J A L)
H3 : is_o A
H4 : is_list L1
============================
 exists J, adj J A (A :: L1)

Subgoal 2 is:
 exists J, adj J A (B :: L1)

member_adj < search.

Subgoal 2:

Variables: A L1 B
IH : forall A L, is_list L -> member A L * -> (exists J, adj J A L)
H1 : is_list (B :: L1)
H3 : member A L1 *
============================
 exists J, adj J A (B :: L1)

member_adj < case H1.

Subgoal 2:

Variables: A L1 B
IH : forall A L, is_list L -> member A L * -> (exists J, adj J A L)
H3 : member A L1 *
H4 : is_o B
H5 : is_list L1
============================
 exists J, adj J A (B :: L1)

member_adj < apply IH to *H5 *H3.

Subgoal 2:

Variables: A L1 B J
IH : forall A L, is_list L -> member A L * -> (exists J, adj J A L)
H4 : is_o B
H6 : adj J A L1
============================
 exists J, adj J A (B :: L1)

member_adj < search.
Proof completed.

Abella < Theorem member_adj_rel : 
forall JJ A J B, adj JJ A J -> member B J -> A = B \/ member B JJ.

============================
 forall JJ A J B, adj JJ A J -> member B J -> A = B \/ member B JJ

member_adj_rel < induction on 1.

IH : forall JJ A J B, adj JJ A J * -> member B J -> A = B \/ member B JJ
============================
 forall JJ A J B, adj JJ A J @ -> member B J -> A = B \/ member B JJ

member_adj_rel < intros.

Variables: JJ A J B
IH : forall JJ A J B, adj JJ A J * -> member B J -> A = B \/ member B JJ
H1 : adj JJ A J @
H2 : member B J
============================
 A = B \/ member B JJ

member_adj_rel < case H1.

Subgoal 1:

Variables: JJ A B
IH : forall JJ A J B, adj JJ A J * -> member B J -> A = B \/ member B JJ
H2 : member B (A :: JJ)
H3 : is_o A
H4 : is_list JJ
============================
 A = B \/ member B JJ

Subgoal 2 is:
 A = B \/ member B (B1 :: K)

member_adj_rel < case H2.

Subgoal 1.1:

Variables: JJ A
IH : forall JJ A J B, adj JJ A J * -> member B J -> A = B \/ member B JJ
H3 : is_o A
H4 : is_list JJ
============================
 A = A \/ member A JJ

Subgoal 1.2 is:
 A = B \/ member B JJ

Subgoal 2 is:
 A = B \/ member B (B1 :: K)

member_adj_rel < search.

Subgoal 1.2:

Variables: JJ A B
IH : forall JJ A J B, adj JJ A J * -> member B J -> A = B \/ member B JJ
H3 : is_o A
H4 : is_list JJ
H5 : member B JJ
============================
 A = B \/ member B JJ

Subgoal 2 is:
 A = B \/ member B (B1 :: K)

member_adj_rel < search.

Subgoal 2:

Variables: A B L B1 K
IH : forall JJ A J B, adj JJ A J * -> member B J -> A = B \/ member B JJ
H2 : member B (B1 :: L)
H3 : is_o B1
H4 : adj K A L *
============================
 A = B \/ member B (B1 :: K)

member_adj_rel < case H2.

Subgoal 2.1:

Variables: A L B1 K
IH : forall JJ A J B, adj JJ A J * -> member B J -> A = B \/ member B JJ
H3 : is_o B1
H4 : adj K A L *
============================
 A = B1 \/ member B1 (B1 :: K)

Subgoal 2.2 is:
 A = B \/ member B (B1 :: K)

member_adj_rel < search.

Subgoal 2.2:

Variables: A B L B1 K
IH : forall JJ A J B, adj JJ A J * -> member B J -> A = B \/ member B JJ
H3 : is_o B1
H4 : adj K A L *
H5 : member B L
============================
 A = B \/ member B (B1 :: K)

member_adj_rel < apply IH to *H4 H5.

Subgoal 2.2:

Variables: A B L B1 K
IH : forall JJ A J B, adj JJ A J * -> member B J -> A = B \/ member B JJ
H3 : is_o B1
H5 : member B L
H6 : A = B \/ member B K
============================
 A = B \/ member B (B1 :: K)

member_adj_rel < case H6.

Subgoal 2.2.1:

Variables: B L B1 K
IH : forall JJ A J B, adj JJ A J * -> member B J -> A = B \/ member B JJ
H3 : is_o B1
H5 : member B L
============================
 B = B \/ member B (B1 :: K)

Subgoal 2.2.2 is:
 A = B \/ member B (B1 :: K)

member_adj_rel < search.

Subgoal 2.2.2:

Variables: A B L B1 K
IH : forall JJ A J B, adj JJ A J * -> member B J -> A = B \/ member B JJ
H3 : is_o B1
H5 : member B L
H7 : member B K
============================
 A = B \/ member B (B1 :: K)

member_adj_rel < search.
Proof completed.

Abella < Theorem adj_preserves_member_lem : 
forall A J B L, is_list J -> member A J -> adj J B L -> member A L.

============================
 forall A J B L, is_list J -> member A J -> adj J B L -> member A L

adj_preserves_member_lem < induction on 2.

IH : forall A J B L, is_list J -> member A J * -> adj J B L -> member A L
============================
 forall A J B L, is_list J -> member A J @ -> adj J B L -> member A L

adj_preserves_member_lem < intros.

Variables: A J B L
IH : forall A J B L, is_list J -> member A J * -> adj J B L -> member A L
H1 : is_list J
H2 : member A J @
H3 : adj J B L
============================
 member A L

adj_preserves_member_lem < case H2.

Subgoal 1:

Variables: A B L L1
IH : forall A J B L, is_list J -> member A J * -> adj J B L -> member A L
H1 : is_list (A :: L1)
H3 : adj (A :: L1) B L
============================
 member A L

Subgoal 2 is:
 member A L

adj_preserves_member_lem < case H3.

Subgoal 1.1:

Variables: A B L1
IH : forall A J B L, is_list J -> member A J * -> adj J B L -> member A L
H1 : is_list (A :: L1)
H4 : is_o B
H5 : is_list (A :: L1)
============================
 member A (B :: A :: L1)

Subgoal 1.2 is:
 member A (A :: L2)

Subgoal 2 is:
 member A L

adj_preserves_member_lem < search.

Subgoal 1.2:

Variables: A B L1 L2
IH : forall A J B L, is_list J -> member A J * -> adj J B L -> member A L
H1 : is_list (A :: L1)
H4 : is_o A
H5 : adj L1 B L2
============================
 member A (A :: L2)

Subgoal 2 is:
 member A L

adj_preserves_member_lem < search.

Subgoal 2:

Variables: A B L L1 B1
IH : forall A J B L, is_list J -> member A J * -> adj J B L -> member A L
H1 : is_list (B1 :: L1)
H3 : adj (B1 :: L1) B L
H4 : member A L1 *
============================
 member A L

adj_preserves_member_lem < case H3.

Subgoal 2.1:

Variables: A B L1 B1
IH : forall A J B L, is_list J -> member A J * -> adj J B L -> member A L
H1 : is_list (B1 :: L1)
H4 : member A L1 *
H5 : is_o B
H6 : is_list (B1 :: L1)
============================
 member A (B :: B1 :: L1)

Subgoal 2.2 is:
 member A (B1 :: L2)

adj_preserves_member_lem < search.

Subgoal 2.2:

Variables: A B L1 B1 L2
IH : forall A J B L, is_list J -> member A J * -> adj J B L -> member A L
H1 : is_list (B1 :: L1)
H4 : member A L1 *
H5 : is_o B1
H6 : adj L1 B L2
============================
 member A (B1 :: L2)

adj_preserves_member_lem < case H1.

Subgoal 2.2:

Variables: A B L1 B1 L2
IH : forall A J B L, is_list J -> member A J * -> adj J B L -> member A L
H4 : member A L1 *
H5 : is_o B1
H6 : adj L1 B L2
H7 : is_o B1
H8 : is_list L1
============================
 member A (B1 :: L2)

adj_preserves_member_lem < apply IH to H8 H4 H6.

Subgoal 2.2:

Variables: A B L1 B1 L2
IH : forall A J B L, is_list J -> member A J * -> adj J B L -> member A L
H4 : member A L1 *
H5 : is_o B1
H6 : adj L1 B L2
H7 : is_o B1
H8 : is_list L1
H9 : member A L2
============================
 member A (B1 :: L2)

adj_preserves_member_lem < search.
Proof completed.

Abella < Theorem adj_preserves_member : 
forall A J B L, member A J -> adj J B L -> member A L.

============================
 forall A J B L, member A J -> adj J B L -> member A L

adj_preserves_member < intros.

Variables: A J B L
H1 : member A J
H2 : adj J B L
============================
 member A L

adj_preserves_member < apply adj_1_is_list to H2.

Variables: A J B L
H1 : member A J
H2 : adj J B L
H3 : is_list J
============================
 member A L

adj_preserves_member < backchain adj_preserves_member_lem.
Proof completed.

Abella < Theorem perm_preserves_member : 
forall A K L, perm K L -> member A K -> member A L.

============================
 forall A K L, perm K L -> member A K -> member A L

perm_preserves_member < induction on 2.

IH : forall A K L, perm K L -> member A K * -> member A L
============================
 forall A K L, perm K L -> member A K @ -> member A L

perm_preserves_member < intros.

Variables: A K L
IH : forall A K L, perm K L -> member A K * -> member A L
H1 : perm K L
H2 : member A K @
============================
 member A L

perm_preserves_member < case H2.

Subgoal 1:

Variables: A L L1
IH : forall A K L, perm K L -> member A K * -> member A L
H1 : perm (A :: L1) L
============================
 member A L

Subgoal 2 is:
 member A L

perm_preserves_member < apply perm_cons_1 to *H1.

Subgoal 1:

Variables: A L L1 J
IH : forall A K L, perm K L -> member A K * -> member A L
H3 : adj J A L
H4 : perm L1 J
============================
 member A L

Subgoal 2 is:
 member A L

perm_preserves_member < backchain adj_member.

Subgoal 2:

Variables: A L L1 B
IH : forall A K L, perm K L -> member A K * -> member A L
H1 : perm (B :: L1) L
H3 : member A L1 *
============================
 member A L

perm_preserves_member < apply perm_cons_1 to *H1.

Subgoal 2:

Variables: A L L1 B J
IH : forall A K L, perm K L -> member A K * -> member A L
H3 : member A L1 *
H4 : adj J B L
H5 : perm L1 J
============================
 member A L

perm_preserves_member < apply IH to *H5 *H3.

Subgoal 2:

Variables: A L L1 B J
IH : forall A K L, perm K L -> member A K * -> member A L
H4 : adj J B L
H6 : member A J
============================
 member A L

perm_preserves_member < backchain adj_preserves_member.
Proof completed.

Abella <