Format

The format for context-sensitive conditional term rewrite systems is the straightforward extension of the CTRS and CSTRS formats:

   CSCTRS ::= ( format CSCTRS cond-type ) fun* rule*
cond-type ::= oriented | join | semi-equational
      fun ::= ( fun identifier number (:replacement-map ( number* ))? )
     rule ::= ( rule term term cond* )
     cond ::= ( = term term )

The restriction on rules and replacement maps are the same as in the CTRS and CSTRS formats.

Example

; @author Miguel Vitores
; @author Salvador Lucas
; @cops 1646
; COPS 1140 with canonical replacement map
(format CSCTRS oriented)
(fun a 0)
(fun b 0)
(fun f 2 :replacement-map (2))
(fun g 2 :replacement-map ())
(fun h 1 :replacement-map ())
(fun k 1 :replacement-map ())
(rule a b)
(rule (f y a) (g x x) (= (h z) x) (= y (k z)))
(rule (k x) a)
(rule (k x) b)
(rule (k x) (h x))