E.1.3 NAT

spec

NAT =

free

{

sorts

Nat;
Zero,Pos < Nat

ops

zero : Zero;
suc__ : Nat  ->   Pos }

then

op

pre__ : Pos  ->   Nat

var

x : Nat

  ·  

pre(suc x)=x

then local

pred

odd__ : Nat

var

x : Nat

  ·  

¬  odd zero

  ·  

odd(suc x)  <=>  ¬  odd x

within

sort

Odd = { n:Nat   ·   odd n }