3. The behavior does not end in a state sn if there exists a state sn+1 such that the sequence s1 → ... → sn+1 also satisfies condition 2.
What does it means for a state such as sn+1 to "exist"?
States are assignments of values to variables, so existence of a state satisfying some condition means being able to find suitable values for the variables. Concretely, formula Next is (equivalent to)
\/ b=0 /\ b'=1 /\ box' = ... \/ b=1 /\ b'=0 /\ box' = ...
Therefore, starting from any state s_n where b equals 0 or 1, one can find some state s_{n+1} such that the pair (s_n, s_{n+1}) satisfies Next.
Stephan
|