; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann37.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann37.xml"
(format TRS)
(fun eq 2)
(fun |0| 0)
(fun true 0)
(fun s 1)
(fun false 0)
(fun or 2)
(fun and 2)
(fun size 1)
(fun empty 0)
(fun edge 3)
(fun le 2)
(fun reachable 3)
(fun reach 5)
(fun if1 6)
(fun if2 6)
(rule (eq |0| |0|) true)
(rule (eq |0| (s x)) false)
(rule (eq (s x) |0|) false)
(rule (eq (s x) (s y)) (eq x y))
(rule (or true y) true)
(rule (or false y) y)
(rule (and true y) y)
(rule (and false y) false)
(rule (size empty) |0|)
(rule (size (edge x y i)) (s (size i)))
(rule (le |0| y) true)
(rule (le (s x) |0|) false)
(rule (le (s x) (s y)) (le x y))
(rule (reachable x y i) (reach x y |0| i i))
(rule (reach x y c i j) (if1 (eq x y) x y c i j))
(rule (if1 true x y c i j) true)
(rule (if1 false x y c i j) (if2 (le c (size j)) x y c i j))
(rule (if2 false x y c i j) false)
(rule (if2 true x y c empty j) false)
(rule (if2 true x y c (edge u v i) j) (or (if2 true x y c i j) (and (eq x u) (reach v y (s c) j j))))