Solution: defining the odd numbers

This page is part of the introduction to proving metatheorems with STELF.

Exercise 2 from the part 1 exercises: Define the odd numbers with a judgement analogous to the even judgement defined above.

Starting with the preliminaries:

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%term plus-z plus z N2 N2 %.
%term plus-s %pi (plus (s N1) N2 (s N3)) %<- (plus N1 N2 N3) %.
%sort even {_ nat} %.
%term even-z even z %.
%term even-s %pi (even (s (s N))) %<- (even N) %.

The definition of odd looks much like the definition of even.

%sort odd {_ nat} %.
%term odd-1 odd (s z) %.
%term odd-s %pi (odd N) %-> (odd (s (s N))) %.