Lines Matching refs:PATH
79 ``(PATH M s (FINITE l) =
85 (PATH M s (INFINITE f) =
422 ``w IN PATH M s = PATH M s w``,
428 ``w IN COMPUTATION M = ?s. s IN M.S0 /\ PATH M s w``,
967 (PATH M s (FINITE l) =
1091 (* (PATH M (HD l) (FINITE l) = *)
1108 (PATH M (f 0) (INFINITE f) =
1133 (PATH M (ELEM w 0) w =
1247 ``PATH M s p ==> (ELEM p 0 = s)``,
1255 ?p :: PATH M s. ?i :: (LESS(LENGTH p)). O_SEM M f (ELEM p i)``,
1267 !p :: PATH M s. !i :: (LESS(LENGTH p)). O_SEM M f (ELEM p i)``,
1486 THEN `PATH
1572 ``TOTAL_AUTOMATON A /\ p IN PATH (M || A) (s,t) ==> (MAP_PATH FST p) IN PATH M s ``,
1816 ``PATH (M || A) (s,t) p /\ AUTOMATON A
1818 PATH
1870 THEN `(MAP_PATH FST p) IN PATH M s'` by PROVE_TAC[PROD_FST]
1979 ``s IN M.S0 /\ t IN A.Q0 /\ PATH M s v /\ MODEL M /\ AUTOMATON A /\
1980 PATH (COMPUTATION_TO_MODEL (MAP_PATH M.L v) || A) (0,t) p /\
1983 PATH (M || A) (s,t) (MAP_PATH (\(n,q). (ELEM v n,q)) p)``,
2051 ``s IN M.S0 /\ t IN A.Q0 /\ PATH M s v /\ MODEL M /\ TOTAL_AUTOMATON A /\
2052 PATH (COMPUTATION_TO_MODEL (MAP_PATH M.L v) || A) (0,t) p
2054 PATH (M || A) (s,t) (MAP_PATH (\(n,q). (ELEM v n,q)) p)``,