; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann04.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann04.xml"
(format TRS)
(fun eq 2)
(fun |0| 0)
(fun true 0)
(fun s 1)
(fun false 0)
(fun or 2)
(fun union 2)
(fun empty 0)
(fun edge 3)
(fun isEmpty 1)
(fun from 1)
(fun to 1)
(fun rest 1)
(fun reach 4)
(fun if1 8)
(fun if2 7)
(fun if3 6)
(fun if4 5)
(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 (union empty h) h)
(rule (union (edge x y i) h) (edge x y (union i h)))
(rule (isEmpty empty) true)
(rule (isEmpty (edge x y i)) false)
(rule (from (edge x y i)) x)
(rule (to (edge x y i)) y)
(rule (rest (edge x y i)) i)
(rule (rest empty) empty)
(rule (reach x y i h) (if1 (eq x y) (isEmpty i) (eq x (from i)) (eq y (to i)) x y i h))
(rule (if1 true b1 b2 b3 x y i h) true)
(rule (if1 false b1 b2 b3 x y i h) (if2 b1 b2 b3 x y i h))
(rule (if2 true b2 b3 x y i h) false)
(rule (if2 false b2 b3 x y i h) (if3 b2 b3 x y i h))
(rule (if3 false b3 x y i h) (reach x y (rest i) (edge (from i) (to i) h)))
(rule (if3 true b3 x y i h) (if4 b3 x y i h))
(rule (if4 true x y i h) true)
(rule (if4 false x y i h) (or (reach x y (rest i) h) (reach (to i) y (union (rest i) h) empty)))