PVSHOL  % [ parameters ]
		: THEORY

  BEGIN

 state:TYPE = {a,b,c,d,e}
  
  i:state =a

  x, y, z:VAR state

  f(x):state = TABLE |[x=a | x=b | x=c | x=d |x=e ]|
                     | a   | b   | b   | b   | a  ||
               ENDTABLE

%  Final:TYPE = { x | x=a OR x=e}
%  F: [ state -> bool ] = Final?
   F(x):bool = x=a OR x=e


  R(x,y):bool = LET T= TRUE, F=FALSE in 
     TABLE x, y
          |[ a | b | c | d | e ]|
       | a | F | T | T | F | F ||
       | b | F | F | F | T | F ||
       | c | F | F | F | T | F ||
       | d | F | F | F | F | T ||
       | e | F | F | F | F | F ||
     ENDTABLE

  u,v:VAR state
  P: VAR PRED[[state,state]]
  

  Reachable(u,v):bool = 
	FORALL P:( FORALL x,y,z: 
 		P(x,x) & 
		(P(x,y)& P(y,z) => P(x,z)) &
		(R(x,y)=>P(x,y)))
	=> P(u,v)

  Test:THEOREM Reachable(a,d) 

  myP:PRED[[state,state]] = (lambda (x,y:state): x=y OR x=a or ((x=b OR x=c) & (y=d OR y=e))
 OR x=d & y=e)

  Test2:THEOREM NOT Reachable(e,a) 
  

  END PVSHOL