let
r f x y = (fst (f x) =
'r'
)
&&
(y--> dNS (fst x) (snd x))
&&
(segV x y)
&&
(rr f x y)