/home/nowonder/forschung/aprove/TPDB05/TRS/various/21.trs

The program

(VAR x)
(RULES
+(p1(),p1()) -> p2()
+(p1(),+(p2(),p2())) -> p5()
+(p5(),p5()) -> p10()
+(+(x,y),z) -> +(x,+(y,z))
+(p1(),+(p1(),x)) -> +(p2(),x)
+(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
+(p2(),p1()) -> +(p1(),p2())
+(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
+(p2(),+(p2(),p2())) -> +(p1(),p5())
+(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
+(p5(),p1()) -> +(p1(),p5())
+(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
+(p5(),p2()) -> +(p2(),p5())
+(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
+(p5(),+(p5(),x)) -> +(p10(),x)
+(p10(),p1()) -> +(p1(),p10())
+(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
+(p10(),p2()) -> +(p2(),p10())
+(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
+(p10(),p5()) -> +(p5(),p10())
+(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
)
(COMMENT Example 2 in Section 8 of \cite{DKM90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend