Welcome to Abella 2.0.5-dev.
Abella < Kind nat type.

Abella < Type z nat.

Abella < Type s nat -> nat.

Abella < CoDefine colist : olist -> prop by 
colist nil;
colist (X :: L) := colist L.

Abella < CoDefine eqi : olist -> olist -> prop by 
eqi nil nil;
eqi (X :: L) (X :: R) := eqi L R.

Abella < Define tk : nat -> olist -> olist -> prop by 
tk z L nil;
tk N nil nil;
tk (s N) (X :: L) (X :: R) := tk N L R.

Abella < Define eqf : olist -> olist -> prop by 
eqf L R := (forall N S, tk N L S -> tk N R S) /\ (forall N S, tk N R S -> tk N L S).

Abella < Theorem eqi_take : 
forall L R S N, eqi L R -> tk N L S -> tk N R S.


============================
 forall L R S N, eqi L R -> tk N L S -> tk N R S

eqi_take < induction on 2.

IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
============================
 forall L R S N, eqi L R -> tk N L S @ -> tk N R S

eqi_take < intros.

Variables: L R S N
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H1 : eqi L R
H2 : tk N L S @
============================
 tk N R S

eqi_take < case H2.
Subgoal 1:

Variables: L R
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H1 : eqi L R
============================
 tk z R nil

Subgoal 2 is:
 tk N R nil

Subgoal 3 is:
 tk (s N1) R (X :: R1)

eqi_take < search.
Subgoal 2:

Variables: R N
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H1 : eqi nil R
============================
 tk N R nil

Subgoal 3 is:
 tk (s N1) R (X :: R1)

eqi_take < case H1.
Subgoal 2:

Variables: N
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
============================
 tk N nil nil

Subgoal 3 is:
 tk (s N1) R (X :: R1)

eqi_take < search.
Subgoal 3:

Variables: R R1 X L1 N1
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H1 : eqi (X :: L1) R
H3 : tk N1 L1 R1 *
============================
 tk (s N1) R (X :: R1)

eqi_take < case H1.
Subgoal 3:

Variables: R1 X L1 N1 R2
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H3 : tk N1 L1 R1 *
H4 : eqi L1 R2
============================
 tk (s N1) (X :: R2) (X :: R1)

eqi_take < apply IH to H4 H3.
Subgoal 3:

Variables: R1 X L1 N1 R2
IH : forall L R S N, eqi L R -> tk N L S * -> tk N R S
H3 : tk N1 L1 R1 *
H4 : eqi L1 R2
H5 : tk N1 R2 R1
============================
 tk (s N1) (X :: R2) (X :: R1)

eqi_take < search.
Proof completed.
Abella < Theorem eqi_sym : 
forall L R, eqi L R -> eqi R L.


============================
 forall L R, eqi L R -> eqi R L

eqi_sym < coinduction.

CH : forall L R, eqi L R -> eqi R L +
============================
 forall L R, eqi L R -> eqi R L #

eqi_sym < intros.

Variables: L R
CH : forall L R, eqi L R -> eqi R L +
H1 : eqi L R
============================
 eqi R L #

eqi_sym < case H1.
Subgoal 1:

CH : forall L R, eqi L R -> eqi R L +
============================
 eqi nil nil #

Subgoal 2 is:
 eqi (X :: R1) (X :: L1) #

eqi_sym < search.
Subgoal 2:

Variables: R1 X L1
CH : forall L R, eqi L R -> eqi R L +
H2 : eqi L1 R1
============================
 eqi (X :: R1) (X :: L1) #

eqi_sym < apply CH to H2.
Subgoal 2:

Variables: R1 X L1
CH : forall L R, eqi L R -> eqi R L +
H2 : eqi L1 R1
H3 : eqi R1 L1 +
============================
 eqi (X :: R1) (X :: L1) #

eqi_sym < search.
Proof completed.
Abella < Theorem eqi_eqf : 
forall L R, eqi L R -> eqf L R.


============================
 forall L R, eqi L R -> eqf L R

eqi_eqf < intros.

Variables: L R
H1 : eqi L R
============================
 eqf L R

eqi_eqf < unfold.
Subgoal 1:

Variables: L R
H1 : eqi L R
============================
 forall N S, tk N L S -> tk N R S

Subgoal 2 is:
 forall N S, tk N R S -> tk N L S

eqi_eqf < intros.
Subgoal 1:

Variables: L R N S
H1 : eqi L R
H2 : tk N L S
============================
 tk N R S

Subgoal 2 is:
 forall N S, tk N R S -> tk N L S

eqi_eqf < apply eqi_take to H1 H2.
Subgoal 1:

Variables: L R N S
H1 : eqi L R
H2 : tk N L S
H3 : tk N R S
============================
 tk N R S

Subgoal 2 is:
 forall N S, tk N R S -> tk N L S

eqi_eqf < search.
Subgoal 2:

Variables: L R
H1 : eqi L R
============================
 forall N S, tk N R S -> tk N L S

eqi_eqf < intros.
Subgoal 2:

Variables: L R N S
H1 : eqi L R
H2 : tk N R S
============================
 tk N L S

eqi_eqf < apply eqi_sym to H1.
Subgoal 2:

Variables: L R N S
H1 : eqi L R
H2 : tk N R S
H3 : eqi R L
============================
 tk N L S

eqi_eqf < apply eqi_take to H3 H2.
Subgoal 2:

Variables: L R N S
H1 : eqi L R
H2 : tk N R S
H3 : eqi R L
H4 : tk N L S
============================
 tk N L S

eqi_eqf < search.
Proof completed.
Abella < Theorem eqf_nil : 
forall L, eqf nil L -> L = nil.


============================
 forall L, eqf nil L -> L = nil

eqf_nil < intros.

Variables: L
H1 : eqf nil L
============================
 L = nil

eqf_nil < case H1.

Variables: L
H2 : forall N S, tk N nil S -> tk N L S
H3 : forall N S, tk N L S -> tk N nil S
============================
 L = nil

eqf_nil < apply H2 to _ with N = s z.

Variables: L
H2 : forall N S, tk N nil S -> tk N L S
H3 : forall N S, tk N L S -> tk N nil S
H4 : tk (s z) L nil
============================
 L = nil

eqf_nil < case H4.

H2 : forall N S, tk N nil S -> tk N nil S
H3 : forall N S, tk N nil S -> tk N nil S
============================
 nil = nil

eqf_nil < search.
Proof completed.
Abella < Theorem eqf_cons : 
forall X L R, eqf (X :: L) R -> (exists S, R = X :: S).


============================
 forall X L R, eqf (X :: L) R -> (exists S, R = X :: S)

eqf_cons < intros.

Variables: X L R
H1 : eqf (X :: L) R
============================
 exists S, R = X :: S

eqf_cons < case H1.

Variables: X L R
H2 : forall N S, tk N (X :: L) S -> tk N R S
H3 : forall N S, tk N R S -> tk N (X :: L) S
============================
 exists S, R = X :: S

eqf_cons < apply H2 to _ with N = s z.

Variables: X L R
H2 : forall N S, tk N (X :: L) S -> tk N R S
H3 : forall N S, tk N R S -> tk N (X :: L) S
H4 : tk (s z) R (X :: nil)
============================
 exists S, R = X :: S

eqf_cons < case H4.

Variables: X L L1
H2 : forall N S, tk N (X :: L) S -> tk N (X :: L1) S
H3 : forall N S, tk N (X :: L1) S -> tk N (X :: L) S
H5 : tk z L1 nil
============================
 exists S, X :: L1 = X :: S

eqf_cons < search.
Proof completed.
Abella < Theorem eqf_sym : 
forall L R, eqf L R -> eqf R L.


============================
 forall L R, eqf L R -> eqf R L

eqf_sym < intros.

Variables: L R
H1 : eqf L R
============================
 eqf R L

eqf_sym < case H1.

Variables: L R
H2 : forall N S, tk N L S -> tk N R S
H3 : forall N S, tk N R S -> tk N L S
============================
 eqf R L

eqf_sym < search.
Proof completed.
Abella < Theorem eqf_downward : 
forall X L R, eqf (X :: L) (X :: R) -> eqf L R.


============================
 forall X L R, eqf (X :: L) (X :: R) -> eqf L R

eqf_downward < intros.

Variables: X L R
H1 : eqf (X :: L) (X :: R)
============================
 eqf L R

eqf_downward < case H1.

Variables: X L R
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
============================
 eqf L R

eqf_downward < unfold.
Subgoal 1:

Variables: X L R
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
============================
 forall N S, tk N L S -> tk N R S

Subgoal 2 is:
 forall N S, tk N R S -> tk N L S

eqf_downward < intros.
Subgoal 1:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N L S
============================
 tk N R S

Subgoal 2 is:
 forall N S, tk N R S -> tk N L S

eqf_downward < assert tk (s N) (X :: L) (X :: S).
Subgoal 1:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N L S
H5 : tk (s N) (X :: L) (X :: S)
============================
 tk N R S

Subgoal 2 is:
 forall N S, tk N R S -> tk N L S

eqf_downward < apply H2 to H5.
Subgoal 1:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N L S
H5 : tk (s N) (X :: L) (X :: S)
H6 : tk (s N) (X :: R) (X :: S)
============================
 tk N R S

Subgoal 2 is:
 forall N S, tk N R S -> tk N L S

eqf_downward < case H6.
Subgoal 1:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N L S
H5 : tk (s N) (X :: L) (X :: S)
H7 : tk N R S
============================
 tk N R S

Subgoal 2 is:
 forall N S, tk N R S -> tk N L S

eqf_downward < search.
Subgoal 2:

Variables: X L R
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
============================
 forall N S, tk N R S -> tk N L S

eqf_downward < intros.
Subgoal 2:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N R S
============================
 tk N L S

eqf_downward < assert tk (s N) (X :: R) (X :: S).
Subgoal 2:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N R S
H5 : tk (s N) (X :: R) (X :: S)
============================
 tk N L S

eqf_downward < apply H3 to H5.
Subgoal 2:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N R S
H5 : tk (s N) (X :: R) (X :: S)
H6 : tk (s N) (X :: L) (X :: S)
============================
 tk N L S

eqf_downward < case H6.
Subgoal 2:

Variables: X L R N S
H2 : forall N S, tk N (X :: L) S -> tk N (X :: R) S
H3 : forall N S, tk N (X :: R) S -> tk N (X :: L) S
H4 : tk N R S
H5 : tk (s N) (X :: R) (X :: S)
H7 : tk N L S
============================
 tk N L S

eqf_downward < search.
Proof completed.
Abella < Theorem eqf_eqi : 
forall L R, colist L -> eqf L R -> eqi L R.


============================
 forall L R, colist L -> eqf L R -> eqi L R

eqf_eqi < coinduction.

CH : forall L R, colist L -> eqf L R -> eqi L R +
============================
 forall L R, colist L -> eqf L R -> eqi L R #

eqf_eqi < intros.

Variables: L R
CH : forall L R, colist L -> eqf L R -> eqi L R +
H1 : colist L
H2 : eqf L R
============================
 eqi L R #

eqf_eqi < case H1.
Subgoal 1:

Variables: R
CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf nil R
============================
 eqi nil R #

Subgoal 2 is:
 eqi (X :: L1) R #

eqf_eqi < apply eqf_nil to H2.
Subgoal 1:

CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf nil nil
============================
 eqi nil nil #

Subgoal 2 is:
 eqi (X :: L1) R #

eqf_eqi < search.
Subgoal 2:

Variables: R L1 X
CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf (X :: L1) R
H3 : colist L1
============================
 eqi (X :: L1) R #

eqf_eqi < apply eqf_cons to H2.
Subgoal 2:

Variables: L1 X S
CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf (X :: L1) (X :: S)
H3 : colist L1
============================
 eqi (X :: L1) (X :: S) #

eqf_eqi < apply eqf_downward to H2.
Subgoal 2:

Variables: L1 X S
CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf (X :: L1) (X :: S)
H3 : colist L1
H4 : eqf L1 S
============================
 eqi (X :: L1) (X :: S) #

eqf_eqi < apply CH to H3 H4.
Subgoal 2:

Variables: L1 X S
CH : forall L R, colist L -> eqf L R -> eqi L R +
H2 : eqf (X :: L1) (X :: S)
H3 : colist L1
H4 : eqf L1 S
H5 : eqi L1 S +
============================
 eqi (X :: L1) (X :: S) #

eqf_eqi < search.
Proof completed.
Abella < CoDefine coapp : olist -> olist -> olist -> prop by 
coapp (X :: A) B (X :: C) := coapp A B C;
coapp nil (X :: B) (X :: C) := coapp nil B C;
coapp nil nil nil.

Abella < Theorem coapp_assoc : 
forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC -> coapp B C BC ->
  coapp A BC ABC.


============================
 forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC -> coapp B C BC ->
   coapp A BC ABC

coapp_assoc < coinduction.

CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
============================
 forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC -> coapp B C BC ->
   coapp A BC ABC #

coapp_assoc < intros.

Variables: A B C AB ABC BC
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H1 : coapp A B AB
H2 : coapp AB C ABC
H3 : coapp B C BC
============================
 coapp A BC ABC #

coapp_assoc < case H1.
Subgoal 1:

Variables: B C ABC BC C1 X A1
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H2 : coapp (X :: C1) C ABC
H3 : coapp B C BC
H4 : coapp A1 B C1
============================
 coapp (X :: A1) BC ABC #

Subgoal 2 is:
 coapp nil BC ABC #

Subgoal 3 is:
 coapp nil BC ABC #

coapp_assoc < case H2.
Subgoal 1:

Variables: B C BC C1 X A1 C2
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H3 : coapp B C BC
H4 : coapp A1 B C1
H5 : coapp C1 C C2
============================
 coapp (X :: A1) BC (X :: C2) #

Subgoal 2 is:
 coapp nil BC ABC #

Subgoal 3 is:
 coapp nil BC ABC #

coapp_assoc < apply CH to H4 H5 H3.
Subgoal 1:

Variables: B C BC C1 X A1 C2
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H3 : coapp B C BC
H4 : coapp A1 B C1
H5 : coapp C1 C C2
H6 : coapp A1 BC C2 +
============================
 coapp (X :: A1) BC (X :: C2) #

Subgoal 2 is:
 coapp nil BC ABC #

Subgoal 3 is:
 coapp nil BC ABC #

coapp_assoc < search.
Subgoal 2:

Variables: C ABC BC C1 X B1
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H2 : coapp (X :: C1) C ABC
H3 : coapp (X :: B1) C BC
H4 : coapp nil B1 C1
============================
 coapp nil BC ABC #

Subgoal 3 is:
 coapp nil BC ABC #

coapp_assoc < case H2.
Subgoal 2:

Variables: C BC C1 X B1 C2
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H3 : coapp (X :: B1) C BC
H4 : coapp nil B1 C1
H5 : coapp C1 C C2
============================
 coapp nil BC (X :: C2) #

Subgoal 3 is:
 coapp nil BC ABC #

coapp_assoc < case H3.
Subgoal 2:

Variables: C C1 X B1 C2 C3
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H4 : coapp nil B1 C1
H5 : coapp C1 C C2
H6 : coapp B1 C C3
============================
 coapp nil (X :: C3) (X :: C2) #

Subgoal 3 is:
 coapp nil BC ABC #

coapp_assoc < apply CH to H4 H5 H6.
Subgoal 2:

Variables: C C1 X B1 C2 C3
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H4 : coapp nil B1 C1
H5 : coapp C1 C C2
H6 : coapp B1 C C3
H7 : coapp nil C3 C2 +
============================
 coapp nil (X :: C3) (X :: C2) #

Subgoal 3 is:
 coapp nil BC ABC #

coapp_assoc < search.
Subgoal 3:

Variables: C ABC BC
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H2 : coapp nil C ABC
H3 : coapp nil C BC
============================
 coapp nil BC ABC #

coapp_assoc < case H2.
Subgoal 3.1:

Variables: BC C1 X B1
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H3 : coapp nil (X :: B1) BC
H4 : coapp nil B1 C1
============================
 coapp nil BC (X :: C1) #

Subgoal 3.2 is:
 coapp nil BC nil #

coapp_assoc < case H3.
Subgoal 3.1:

Variables: C1 X B1 C2
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H4 : coapp nil B1 C1
H5 : coapp nil B1 C2
============================
 coapp nil (X :: C2) (X :: C1) #

Subgoal 3.2 is:
 coapp nil BC nil #

coapp_assoc < apply CH to _ H4 H5.
Subgoal 3.1:

Variables: C1 X B1 C2
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H4 : coapp nil B1 C1
H5 : coapp nil B1 C2
H6 : coapp nil C2 C1 +
============================
 coapp nil (X :: C2) (X :: C1) #

Subgoal 3.2 is:
 coapp nil BC nil #

coapp_assoc < search.
Subgoal 3.2:

Variables: BC
CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
H3 : coapp nil nil BC
============================
 coapp nil BC nil #

coapp_assoc < case H3.
Subgoal 3.2:

CH : forall A B C AB ABC BC, coapp A B AB -> coapp AB C ABC ->
       coapp B C BC -> coapp A BC ABC +
============================
 coapp nil nil nil #

coapp_assoc < search.
Proof completed.
Abella <