; @origtpdbfilename ./TRS/AProVE/AAECC-ring.trs
; @xtcfilename "./TRS_Standard/AProVE_04/AAECC-ring.xml"
(format TRS)
(fun fstsplit 2)
(fun |0| 0)
(fun nil 0)
(fun s 1)
(fun cons 2)
(fun sndsplit 2)
(fun empty 1)
(fun true 0)
(fun false 0)
(fun leq 2)
(fun length 1)
(fun app 2)
(fun map_f 2)
(fun f 2)
(fun head 1)
(fun tail 1)
(fun ring 6)
(fun if_1 7)
(fun if_2 7)
(fun if_3 7)
(fun if_4 7)
(fun two 0)
(fun if_5 7)
(fun if_6 7)
(fun if_7 7)
(fun if_8 7)
(fun three 0)
(fun if_9 7)
(rule (fstsplit |0| x) nil)
(rule (fstsplit (s n) nil) nil)
(rule (fstsplit (s n) (cons h t)) (cons h (fstsplit n t)))
(rule (sndsplit |0| x) x)
(rule (sndsplit (s n) nil) nil)
(rule (sndsplit (s n) (cons h t)) (sndsplit n t))
(rule (empty nil) true)
(rule (empty (cons h t)) false)
(rule (leq |0| m) true)
(rule (leq (s n) |0|) false)
(rule (leq (s n) (s m)) (leq n m))
(rule (length nil) |0|)
(rule (length (cons h t)) (s (length t)))
(rule (app nil x) x)
(rule (app (cons h t) x) (cons h (app t x)))
(rule (map_f pid nil) nil)
(rule (map_f pid (cons h t)) (app (f pid h) (map_f pid t)))
(rule (head (cons h t)) h)
(rule (tail (cons h t)) t)
(rule (ring st_1 in_2 st_2 in_3 st_3 m) (if_1 st_1 in_2 st_2 in_3 st_3 m (empty (fstsplit m st_1))))
(rule (if_1 st_1 in_2 st_2 in_3 st_3 m false) (ring (sndsplit m st_1) (cons (fstsplit m st_1) in_2) st_2 in_3 st_3 m))
(rule (ring st_1 in_2 st_2 in_3 st_3 m) (if_2 st_1 in_2 st_2 in_3 st_3 m (leq m (length st_2))))
(rule (if_2 st_1 in_2 st_2 in_3 st_3 m true) (if_3 st_1 in_2 st_2 in_3 st_3 m (empty (fstsplit m st_2))))
(rule (if_3 st_1 in_2 st_2 in_3 st_3 m false) (ring st_1 in_2 (sndsplit m st_2) (cons (fstsplit m st_2) in_3) st_3 m))
(rule (if_2 st_1 in_2 st_2 in_3 st_3 m false) (if_4 st_1 in_2 st_2 in_3 st_3 m (empty (fstsplit m (app (map_f two (head in_2)) st_2)))))
(rule (if_4 st_1 in_2 st_2 in_3 st_3 m false) (ring st_1 (tail in_2) (sndsplit m (app (map_f two (head in_2)) st_2)) (cons (fstsplit m (app (map_f two (head in_2)) st_2)) in_3) st_3 m))
(rule (ring st_1 in_2 st_2 in_3 st_3 m) (if_5 st_1 in_2 st_2 in_3 st_3 m (empty (map_f two (head in_2)))))
(rule (if_5 st_1 in_2 st_2 in_3 st_3 m true) (ring st_1 (tail in_2) st_2 in_3 st_3 m))
(rule (ring st_1 in_2 st_2 in_3 st_3 m) (if_6 st_1 in_2 st_2 in_3 st_3 m (leq m (length st_3))))
(rule (if_6 st_1 in_2 st_2 in_3 st_3 m true) (if_7 st_1 in_2 st_2 in_3 st_3 m (empty (fstsplit m st_3))))
(rule (if_7 st_1 in_2 st_2 in_3 st_3 m false) (ring st_1 in_2 st_2 in_3 (sndsplit m st_3) m))
(rule (if_6 st_1 in_2 st_2 in_3 st_3 m false) (if_8 st_1 in_2 st_2 in_3 st_3 m (empty (fstsplit m (app (map_f three (head in_3)) st_3)))))
(rule (if_8 st_1 in_2 st_2 in_3 st_3 m false) (ring st_1 in_2 st_2 (tail in_3) (sndsplit m (app (map_f three (head in_3)) st_3)) m))
(rule (ring st_1 in_2 st_2 in_3 st_3 m) (if_9 st_1 in_2 st_2 in_3 st_3 m (empty (map_f three (head in_3)))))
(rule (if_9 st_1 in_2 st_2 in_3 st_3 m true) (ring st_1 in_2 st_2 (tail in_3) st_3 m))