(CONDITIONTYPE ORIENTED) (VAR x) (RULES f(x) -> e | d == l h(x, x) -> A ) (COMMENT \cite{NSS12}, R_10 of Example 4.11 doi: 10.2168/LMCS-8(3:4)2012 )