Lines Matching refs:PATH
143 ``!xs x s t. PATH (x,xs) s /\ s SUBSET t ==> PATH (x,xs) t``,
348 \\ Q.UNDISCH_TAC `PATH (r',p ++ [x]) (apply b (ch_set h))`
382 \\ Q.UNDISCH_TAC `PATH (r',p ++ [x]) (basic_abs m)`
414 (PATH (y,p) ((x,y',z,d) INSERT s) = PATH (y,p) s)``,
417 \\ Q.UNDISCH_TAC `PATH (y,p) ((x,y',z,d) INSERT s)`
999 ``!xs x y ys. PATH (x,xs ++ y::ys) s = PATH(x,xs++[y]) s /\ PATH(y,ys) s``,
1003 ``!p r. MEM r (v1::v2::vs) /\ PATH (r,p++[a]) ((fresh h,v1,v2,d) INSERT (ch_set h)) ==>
1005 (PATH (r',p++[a]) ((fresh h,v1,v2,d) INSERT (ch_set h)) \/ (a = v1) \/ (a = v2)) /\
1029 ``!p k r. ~MEM k (r::p) ==> (PATH (r,p ++ [a]) ((k,x,y,z) INSERT s) = PATH (r,p ++ [a]) s)``,
1033 ``!p k r x y z. ~MEM k (r::p) /\ PATH (r,p ++ [a]) ((k,x,y,z) INSERT s) ==> PATH (r,p ++ [a]) s``,