Lines Matching refs:PATH
73 (PATH (x,[]) s = T) /\
74 (PATH (x,y::ys) s = PATH (y,ys) s /\ ?z d. (x,y,z,d) IN s \/ (x,z,y,d) IN s)`;
77 reachable r s i = (r = i) \/ ?p. PATH (r,p++[i]) s`;
605 ``!p r b i j m. PATH (r,p) (basic_abs(CUT (b,i) m)) /\ i <= j ==>
606 PATH (r,p) (basic_abs(CUT (b,j) m))``,
622 ``!ys x y z m. PATH(x,ys++[y])m /\ PATH(y,[z])m ==> PATH(x,ys++[y]++[z])m``,
745 \\ `PATH (h,[i]) (basic_abs (CUT (b,i + 1) ((i =+ DATA (x',y',d))m'')))` by
917 PATH (r,p ++ [g a]) s ==> PATH (f r,MAP f p ++ [a]) (apply g s)``,
934 \\ Q.UNDISCH_TAC `PATH (r',p ++ [a]) (apply g s)`
941 RANGE(i,j)r /\ ~RANGE(i,j)x /\ PATH (r,p ++ [x]) (abs m) /\ ~(x = 0) /\ (m 0 = EMP) ==>
942 ?s d. PATH(s,[d]) (abs m) /\ RANGE(i,j)s /\ ~RANGE(i,j)d /\ ~(d = 0)``,
985 PATH (b,p) (abs (CUT (i,j) m)) ==> PATH (b,p) (abs m)``,