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

Abella < Type z nat.

Abella < Type s nat -> nat.

Abella < Define nat : nat -> prop by 
nat z;
nat (s N) := nat N.

Abella < Define even : nat -> prop by 
even z;
even (s (s N)) := even N.

Abella < Define odd : nat -> prop by 
odd (s z);
odd (s (s N)) := odd N.

Abella < Theorem even_or_odd : 
forall N, nat N -> even N \/ odd N.


============================
 forall N, nat N -> even N \/ odd N

even_or_odd < induction on 1.

IH : forall N, nat N * -> even N \/ odd N
============================
 forall N, nat N @ -> even N \/ odd N

even_or_odd < intros.

Variables: N
IH : forall N, nat N * -> even N \/ odd N
H1 : nat N @
============================
 even N \/ odd N

even_or_odd < case H1.
Subgoal 1:

IH : forall N, nat N * -> even N \/ odd N
============================
 even z \/ odd z

Subgoal 2 is:
 even (s N1) \/ odd (s N1)

even_or_odd < search.
Subgoal 2:

Variables: N1
IH : forall N, nat N * -> even N \/ odd N
H2 : nat N1 *
============================
 even (s N1) \/ odd (s N1)

even_or_odd < case H2.
Subgoal 2.1:

IH : forall N, nat N * -> even N \/ odd N
============================
 even (s z) \/ odd (s z)

Subgoal 2.2 is:
 even (s (s N2)) \/ odd (s (s N2))

even_or_odd < search.
Subgoal 2.2:

Variables: N2
IH : forall N, nat N * -> even N \/ odd N
H3 : nat N2 *
============================
 even (s (s N2)) \/ odd (s (s N2))

even_or_odd < apply IH to H3.
Subgoal 2.2:

Variables: N2
IH : forall N, nat N * -> even N \/ odd N
H3 : nat N2 *
H4 : even N2 \/ odd N2
============================
 even (s (s N2)) \/ odd (s (s N2))

even_or_odd < case H4.
Subgoal 2.2.1:

Variables: N2
IH : forall N, nat N * -> even N \/ odd N
H3 : nat N2 *
H5 : even N2
============================
 even (s (s N2)) \/ odd (s (s N2))

Subgoal 2.2.2 is:
 even (s (s N2)) \/ odd (s (s N2))

even_or_odd < search.
Subgoal 2.2.2:

Variables: N2
IH : forall N, nat N * -> even N \/ odd N
H3 : nat N2 *
H5 : odd N2
============================
 even (s (s N2)) \/ odd (s (s N2))

even_or_odd < search.
Proof completed.
Abella < Define even' : nat -> prop,	
odd' : nat -> prop by 
even' z;
odd' (s N) := even' N;
even' (s N) := odd' N.

Abella < Theorem even'_nat : 
forall N, even' N -> nat N.


============================
 forall N, even' N -> nat N

even'_nat < induction on 1.

IH : forall N, even' N * -> nat N
============================
 forall N, even' N @ -> nat N

even'_nat < intros.

Variables: N
IH : forall N, even' N * -> nat N
H1 : even' N @
============================
 nat N

even'_nat < case H1.
Subgoal 1:

IH : forall N, even' N * -> nat N
============================
 nat z

Subgoal 2 is:
 nat (s N1)

even'_nat < search.
Subgoal 2:

Variables: N1
IH : forall N, even' N * -> nat N
H2 : odd' N1 *
============================
 nat (s N1)

even'_nat < case H2.
Subgoal 2:

Variables: N2
IH : forall N, even' N * -> nat N
H3 : even' N2 *
============================
 nat (s (s N2))

even'_nat < apply IH to H3.
Subgoal 2:

Variables: N2
IH : forall N, even' N * -> nat N
H3 : even' N2 *
H4 : nat N2
============================
 nat (s (s N2))

even'_nat < search.
Proof completed.
Abella < Theorem odd'_nat : 
forall N, odd' N -> nat N.


============================
 forall N, odd' N -> nat N

odd'_nat < induction on 1.

IH : forall N, odd' N * -> nat N
============================
 forall N, odd' N @ -> nat N

odd'_nat < intros.

Variables: N
IH : forall N, odd' N * -> nat N
H1 : odd' N @
============================
 nat N

odd'_nat < case H1.

Variables: N1
IH : forall N, odd' N * -> nat N
H2 : even' N1 *
============================
 nat (s N1)

odd'_nat < case H2.
Subgoal 1:

IH : forall N, odd' N * -> nat N
============================
 nat (s z)

Subgoal 2 is:
 nat (s (s N2))

odd'_nat < search.
Subgoal 2:

Variables: N2
IH : forall N, odd' N * -> nat N
H3 : odd' N2 *
============================
 nat (s (s N2))

odd'_nat < apply IH to H3.
Subgoal 2:

Variables: N2
IH : forall N, odd' N * -> nat N
H3 : odd' N2 *
H4 : nat N2
============================
 nat (s (s N2))

odd'_nat < search.
Proof completed.
Abella <