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

The program

(VAR )
(RULES
f(g(i(a,b,b'),c),d) ->
    if(e,f(.(b,c),d'),f(.(b',c),d'))
f(g(h(a,b),c),d) ->
    if(e,f(.(b,g(h(a,b),c)),d),f(c,d'))
)
(COMMENT Example 4.47 in \cite{SK90})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend