C Illustrations

---

Table 5: BasicNat

 LaTeX source:

BasicNat.tex

Formatted:

sorts

Zero, Pos < Nat

ops

0 : Zero;
suc__ : Nat -> Pos;
1 : Pos = suc 0;

__+__ :	Nat×Nat -> Nat,
	assoc,comm,unit 0;

vars

i,j:Nat

.

i+0=0

.

i+suc j=suc(i+j)

ops

pre__ : Nat ->? Nat;
pre__ : Pos -> Nat

vars

m,n : Nat

axioms

 
¬ def pre(0);
pre suc n=n;
def pre(n) <=> n e Pos;
n e Pos => suc pre n=n;

pre m+pre n=pre pre(m+n)

if def pre m /\ def pre n;

pre(m+n) =
pre(m)+n	when m e Pos else
m+pre(n)	when n e Pos else
0 %%	when m=0 /\ n=0

op

double(k:Nat):Nat = k+k;

pred

even : Nat

axioms

 
even(0);

even(n) =>	¬ even(n+1) /\
	even(n+1+1)

sort

Even = { x:Nat.even(x) }

axiom

 

forall e:Even. exists ! h:Nat.

e=double(h)

preds

 
__<__ : Nat×Nat;

__ < __(m,n:Nat) <=>

m=n \/ m<n

generated {

sort

Nat

ops

0, 1 : Nat;
__+__ : Nat×Nat -> Nat  }

---

---

Table 6: BasicTypes

 LaTeX source:

BasicTypes.tex

Formatted:

generated type

 
Nat ::= 0 | 1 | __+__(Nat;Nat)

free type

 
Nat ::= 0 | suc(pre:?Nat)

free types

 

Nat	::=	sorts Zero, Pos
Zero	::=	0
Pos	::=	suc(pre:Nat)

free type

List[Elem] ::=

nil | cons( hd:?Elem; tl:?List[Elem])

free type

BinTree[Elem] ::=

sort Elem | node( left,right:? BinTree[Elem])

---