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 <
```