; @origtpdbfilename ./TRS/higher-order/AotoYam/012.trs
; @xtcfilename "./TRS_Standard/AotoYamada_05/012.xml"
(format TRS)
(fun app 2)
(fun and 0)
(fun true 0)
(fun false 0)
(fun or 0)
(fun forall 0)
(fun nil 0)
(fun cons 0)
(fun forsome 0)
(rule (app (app and true) true) true)
(rule (app (app and x) false) false)
(rule (app (app and false) y) false)
(rule (app (app or true) y) true)
(rule (app (app or x) true) true)
(rule (app (app or false) false) false)
(rule (app (app forall p) nil) true)
(rule (app (app forall p) (app (app cons x) xs)) (app (app and (app p x)) (app (app forall p) xs)))
(rule (app (app forsome p) nil) false)
(rule (app (app forsome p) (app (app cons x) xs)) (app (app or (app p x)) (app (app forsome p) xs)))