CSI^ho
HRS
For input use the Cops HRS format. See http://coco.nue.riec.tohoku.ac.jp/problems/hrs.txt for details.

Example:

(FUN
  nil : alist
  cons : a -> alist -> alist
  map : (a -> a) -> alist -> alist
)
(VAR
  x : a
  F : a -> a
  h : a
  t : alist
)
(RULES
  map (\x. F x) nil -> nil,
  map (\x. F x) (cons h t) -> cons (F h) (map (\x. F x) t)
)
 (examples: )
input Upload a file (HRS) in the Cops format. See http://coco.nue.riec.tohoku.ac.jp/problems/hrs.txt for details.  
KB Knuth-Bendix Criterion   NONCR Disprove Confluence   AUTO Automatic Mode   COMP Competition Mode  
EXPERT Expert mode; enter your own strategy