spec 
::= 
( decl ) spec  e 
decl 
::= 
VAR idlist  THEORY listofthdecl 
RULES listofrules 


 STRATEGY strategydecl  id anylist 
anylist 
::= 
e  id anylist  string anylist 


 ( anylist ) anylist  , anylist 
idlist 
::= 
e  id idlist 
listofthdecl 
::= 
e  ( thdecl ) listofthdecl 
thdecl 
::= 
id idlist  EQUATIONS eqlist 
eqlist 
::= 
e  equation eqlist 
equation 
::= 
term == term 
listofrules 
::= 
e  rule listofrules 
rule 
::= 
term > term  term > term 
condlist 
condlist 
::= 
cond  cond , condlist 
cond 
::= 
term > term  term >< term 
term 
::= 
id  id ( )  id ( termlist ) 
termlist 
::= 
term  term , termlist 
strategydecl 
::= 
INNERMOST  CONTEXTSENSITIVE
csstratlist 
csstratlist 
::= 
e  ( id intlist )
csstratlist 
intlist 
::= 
e  int intlist 