% Taken from Vlad Rusu, Verifying a Sliding Window Protocol using PVS. FORTE 2001: 251-268.
runs[State      : TYPE, 
     initial    : PRED[State], 
     transition : PRED[[State, State]]] : THEORY

BEGIN

  % Runs are infinite sequences of transition-related states,  
  % starting in an initial state

  run_fragment: pred[sequence[State]] =  
    {r : sequence[State] | FORALL (n : nat): transition(r(n),r(n+1))}

  run : pred[(run_fragment)] =  {r : (run_fragment) | initial(r(0))}

  r: VAR (run)
  p :VAR pred[[State]]  
  % The first parameter is the current state
  % The second parameter is the initial state

  invariant(p) : bool = FORALL (r : (run), n:nat ): p(r(n))

  invariant_rule : THEOREM
    (FORALL (r : (run)) : p(r(0)) AND 
      FORALL (n : nat) : p(r(n)) IMPLIES p(r(n+1)))
     IMPLIES invariant(p)

END runs