/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/2.02.trs

The program

(VAR x y z)
(RULES
+(+(x,y),z) -> +(x,+(y,z))
+(f(x),f(y)) -> f(+(x,y))
+(f(x),+(f(y),z)) -> +(f(+(x,y)),z)
)

(COMMENT Example 2.2 (Associativity and Endomorphism) in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend