sum : THEORY
BEGIN

a : [nat->real]

plus(x:nat,y:nat): nat = x+y

sum(n:nat) : RECURSIVE real = 
IF n=0 THEN a(0) ELSE a(n) + sum(n) ENDIF 
MEASURE 2*n

sum(a:[nat->real],n:nat) : RECURSIVE real = 
IF n=0 THEN a(0) ELSE a(n) + sum(a,n-1) ENDIF 
MEASURE n

id(x:nat):nat = x

gauss1 : PROPOSITION sum(id,3) = 6

unser_p(n:nat):boolean = sum(id,n) = n*(n+1)/2

 gauss : PROPOSITION 
	FORALL(n:nat):sum(id,n) = n*(n+1)/2



fib(n:nat) : RECURSIVE nat = 
 IF n=0 OR n=1 THEN 1 ELSE fib(n-1) + fib(n-2) ENDIF 
MEASURE n

c(n:nat): RECURSIVE int = IF n=0 THEN 1 ELSE -c(n-1) ENDIF MEASURE n

cassini : THEOREM FORALL (n:nat): 
      fib(n+2)*fib(n) - fib(n+1) * fib(n+1) = c(n)

END sum