Welcome to Abella 2.0.7-dev.

Abella < Type is_o o -> prop.

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

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

Abella < Theorem append_1_is_list : 
forall J K L, append J K L -> is_list J.

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

append_1_is_list < induction on 1.

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

append_1_is_list < intros.

Variables: J K L
IH : forall J K L, append J K L * -> is_list J
H1 : append J K L @
============================
 is_list J

append_1_is_list < case H1.

Subgoal 1:

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

Subgoal 2 is:
 is_list (A :: J1)

append_1_is_list < search.

Subgoal 2:

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

append_1_is_list < apply IH to H3.

Subgoal 2:

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

append_1_is_list < search.
Proof completed.

Abella < Theorem append_2_is_list : 
forall J K L, append J K L -> is_list K.

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

append_2_is_list < induction on 1.

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

append_2_is_list < intros.

Variables: J K L
IH : forall J K L, append J K L * -> is_list K
H1 : append J K L @
============================
 is_list K

append_2_is_list < case H1.

Subgoal 1:

Variables: L
IH : forall J K L, append J K L * -> is_list K
H2 : is_list L
============================
 is_list L

Subgoal 2 is:
 is_list K

append_2_is_list < search.

Subgoal 2:

Variables: K L1 A J1
IH : forall J K L, append J K L * -> is_list K
H2 : is_o A
H3 : append J1 K L1 *
============================
 is_list K

append_2_is_list < apply IH to H3.

Subgoal 2:

Variables: K L1 A J1
IH : forall J K L, append J K L * -> is_list K
H2 : is_o A
H3 : append J1 K L1 *
H4 : is_list K
============================
 is_list K

append_2_is_list < search.
Proof completed.

Abella < Theorem append_3_is_list : 
forall J K L, append J K L -> is_list L.

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

append_3_is_list < induction on 1.

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

append_3_is_list < intros.

Variables: J K L
IH : forall J K L, append J K L * -> is_list L
H1 : append J K L @
============================
 is_list L

append_3_is_list < case H1.

Subgoal 1:

Variables: L
IH : forall J K L, append J K L * -> is_list L
H2 : is_list L
============================
 is_list L

Subgoal 2 is:
 is_list (A :: L1)

append_3_is_list < search.

Subgoal 2:

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

append_3_is_list < apply IH to H3.

Subgoal 2:

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

append_3_is_list < search.
Proof completed.

Abella < Theorem can_append : 
forall J K, is_list J -> is_list K -> (exists L, append J K L).

============================
 forall J K, is_list J -> is_list K -> (exists L, append J K L)

can_append < induction on 1.

IH : forall J K, is_list J * -> is_list K -> (exists L, append J K L)
============================
 forall J K, is_list J @ -> is_list K -> (exists L, append J K L)

can_append < intros.

Variables: J K
IH : forall J K, is_list J * -> is_list K -> (exists L, append J K L)
H1 : is_list J @
H2 : is_list K
============================
 exists L, append J K L

can_append < case H1.

Subgoal 1:

Variables: K
IH : forall J K, is_list J * -> is_list K -> (exists L, append J K L)
H2 : is_list K
============================
 exists L, append nil K L

Subgoal 2 is:
 exists L1, append (A :: L) K L1

can_append < search.

Subgoal 2:

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

can_append < apply IH to H4 H2.

Subgoal 2:

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

can_append < search.
Proof completed.

Abella < Define rev : (list o) -> (list o) -> prop by 
rev nil nil;
rev (A :: J) L := exists K, rev J K /\ append K (A :: nil) L.

Abella < Theorem rev_1_is_list : 
forall J K, rev J K -> is_list J.

============================
 forall J K, rev J K -> is_list J

rev_1_is_list < induction on 1.

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

rev_1_is_list < intros.

Variables: J K
IH : forall J K, rev J K * -> is_list J
H1 : rev J K @
============================
 is_list J

rev_1_is_list < case H1.

Subgoal 1:

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

Subgoal 2 is:
 is_list (A :: J1)

rev_1_is_list < search.

Subgoal 2:

Variables: K K1 J1 A
IH : forall J K, rev J K * -> is_list J
H2 : rev J1 K1 *
H3 : append K1 (A :: nil) K
============================
 is_list (A :: J1)

rev_1_is_list < apply IH to H2.

Subgoal 2:

Variables: K K1 J1 A
IH : forall J K, rev J K * -> is_list J
H2 : rev J1 K1 *
H3 : append K1 (A :: nil) K
H4 : is_list J1
============================
 is_list (A :: J1)

rev_1_is_list < apply append_2_is_list to H3.

Subgoal 2:

Variables: K K1 J1 A
IH : forall J K, rev J K * -> is_list J
H2 : rev J1 K1 *
H3 : append K1 (A :: nil) K
H4 : is_list J1
H5 : is_list (A :: nil)
============================
 is_list (A :: J1)

rev_1_is_list < case H5.

Subgoal 2:

Variables: K K1 J1 A
IH : forall J K, rev J K * -> is_list J
H2 : rev J1 K1 *
H3 : append K1 (A :: nil) K
H4 : is_list J1
H6 : is_o A
H7 : is_list nil
============================
 is_list (A :: J1)

rev_1_is_list < search.
Proof completed.

Abella < Theorem rev_2_is_list : 
forall J K, rev J K -> is_list K.

============================
 forall J K, rev J K -> is_list K

rev_2_is_list < intros.

Variables: J K
H1 : rev J K
============================
 is_list K

rev_2_is_list < case H1.

Subgoal 1:

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

Subgoal 2 is:
 is_list K

rev_2_is_list < search.

Subgoal 2:

Variables: K K1 J1 A
H2 : rev J1 K1
H3 : append K1 (A :: nil) K
============================
 is_list K

rev_2_is_list < apply append_3_is_list to H3.

Subgoal 2:

Variables: K K1 J1 A
H2 : rev J1 K1
H3 : append K1 (A :: nil) K
H4 : is_list K
============================
 is_list K

rev_2_is_list < search.
Proof completed.

Abella < Theorem can_rev : 
forall J, is_list J -> (exists K, rev J K).

============================
 forall J, is_list J -> (exists K, rev J K)

can_rev < induction on 1.

IH : forall J, is_list J * -> (exists K, rev J K)
============================
 forall J, is_list J @ -> (exists K, rev J K)

can_rev < intros.

Variables: J
IH : forall J, is_list J * -> (exists K, rev J K)
H1 : is_list J @
============================
 exists K, rev J K

can_rev < case H1.

Subgoal 1:

IH : forall J, is_list J * -> (exists K, rev J K)
============================
 exists K, rev nil K

Subgoal 2 is:
 exists K, rev (A :: L) K

can_rev < search.

Subgoal 2:

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

can_rev < apply IH to H3.

Subgoal 2:

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

can_rev < apply can_append to _ _ with J = K, K = A :: nil.

Subgoal 2.1:

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

Subgoal 2 is:
 exists K, rev (A :: L) K

can_rev < apply rev_2_is_list to H4.

Subgoal 2.1:

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

Subgoal 2 is:
 exists K, rev (A :: L) K

can_rev < search.

Subgoal 2:

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

can_rev < search.
Proof completed.

Abella <