E.1.3 Nat

spec

Nat =

free

{

sorts

Nat;
Zero,Pos < Nat

ops

zero : Zero;
succ__ : Nat -> Pos }

then

 

op

pre__ : Pos -> Nat

var

x : Nat

·

pre(succ x)=x

then local

 

pred

odd__ : Nat

var

x : Nat

·

¬ odd zero

·

odd(succ x) <=> ¬ odd x

within

sort

Odd = {n:Nat . odd n}