[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

errors



Hello,

	Projection is a basic operator in query languages,
proj and f are a function,
	proj : C(T1)->C(T2) (%  C(T) is TYPE = list[T1])
	f: T1->T2	
	C(X1,....Xn) is list[T1]
	proj(C(X1,X2,....Xn)) = C(f(X1) , f(X2) , ..... , f(Xn))

and i would like to prove the theorem but i have a message error:

Specification in PVS:

projection[T1, T2: TYPE] : THEORY
   BEGIN
	C1: TYPE = list[T1]
	C2: TYPE = list[T2]
	proj: VAR [C1->C2]
	f: VAR [T1->T2]
	l: VAR C1
	x: VAR T1
	proj(l): RECURSIVE [C1->C2] =
		CASES l OF
			null: null,
			cons(x,y): cons(f(car(l)),proj(cdr(l)))
		ENDCASES 
	MEASURE length(l)
 
   END projection

After M-x tc message error is: Free variables not allowed here
the curssor is placed there f(car(l)),proj(cdr(l)

Could you help me?
Thanks