Lines Matching refs:PATH
162 * PATH M s p is true iff p is a path of model M starting from s
166 `PATH M s p = (p 0 = s) /\ !i. M.R(p(i),p(i+1))`;
171 ``!M s p. s IN M.S /\ PATH M s p /\ MODEL M ==> !n. (p n) IN M.S``,
217 `SAT M f = !p. (p 0) IN M.S0 /\ PATH M (p 0) p ==> SEM M p f`;
348 ==> !p. PATH M s p ==> ?p'. PATH M' s' p' /\ !i. M'.S(p' i) /\ B(p i, p' i)``,
377 ==> !p'. PATH M' s' p'
378 ==> ?p. PATH M s p /\ !i. M.S(p i) /\ B(p i, p' i)``,
396 (!p. PATH M s p
397 ==> ?p'. PATH M' s' p' /\ !i. M'.S(p' i) /\ B(p i, p' i))
399 (!p'. PATH M' s' p'
400 ==> ?p. PATH M s p /\ !i. M.S(p i) /\ B(p i, p' i))``,
418 ``!M p. PATH M s p ==> !n. PATH M (p n) (SUFFIX p n)``,
425 ``!M s p. MODEL M /\ M.S s /\ PATH M s p
445 PATH M s p /\ PATH M' s' p' /\ (!i. B(p i, p' i))
487 PATH M s p /\ PATH M' s' p' /\ (!i. B(p i, p' i))
518 THEN `!p'. PATH M' (p 0) p' ==> ?p. PATH M s0 p /\ !i. B (p i,p' i)`
525 THEN `?p'. PATH M' s0' p' /\ !i. B (p i,p' i)` by METIS_TAC[Lemma1]