> ReachBy n R B s > > n = number of steps > R = transition relation > B = initial states > > But what is s? s is the state you are querying for whether it is reachable in n steps from B via R. The function you give above *expresses* a set of states, but does so by being a function (states->bool) which is true if s is in that set. I hope? -- Crispin