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 }