MAYBE
Problem:
minus(minus(x)) -> x
minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y))))
minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))
Proof:
DP Processor:
DPs:
minus#(+(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(minus(minus(x)))
f#(minus(x)) -> f#(x)
f#(minus(x)) -> minus#(f(x))
f#(minus(x)) -> minus#(minus(f(x)))
f#(minus(x)) -> minus#(minus(minus(f(x))))
TRS:
minus(minus(x)) -> x
minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y))))
minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))
ADG Processor:
DPs:
minus#(+(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(minus(minus(x)))
f#(minus(x)) -> f#(x)
f#(minus(x)) -> minus#(f(x))
f#(minus(x)) -> minus#(minus(f(x)))
f#(minus(x)) -> minus#(minus(minus(f(x))))
TRS:
minus(minus(x)) -> x
minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y))))
minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))
graph:
f#(minus(x)) -> f#(x) -> f#(minus(x)) -> f#(x)
f#(minus(x)) -> f#(x) -> f#(minus(x)) -> minus#(f(x))
f#(minus(x)) -> f#(x) -> f#(minus(x)) -> minus#(minus(f(x)))
f#(minus(x)) -> f#(x) -> f#(minus(x)) -> minus#(minus(minus(f(x))))
f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(y)
f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(y))
f#(minus(x)) -> minus#(f(x)) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(x)
f#(minus(x)) -> minus#(f(x)) -> minus#(+(x,y)) -> minus#(minus(x))
f#(minus(x)) -> minus#(f(x)) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(y)
f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(y))
f#(minus(x)) -> minus#(f(x)) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(x)
f#(minus(x)) -> minus#(f(x)) -> minus#(*(x,y)) -> minus#(minus(x))
f#(minus(x)) -> minus#(f(x)) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(+(x,y)) -> minus#(y)
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(+(x,y)) -> minus#(minus(y))
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(+(x,y)) -> minus#(x)
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(+(x,y)) -> minus#(minus(x))
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(*(x,y)) -> minus#(y)
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(*(x,y)) -> minus#(minus(y))
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(*(x,y)) -> minus#(x)
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(*(x,y)) -> minus#(minus(x))
f#(minus(x)) -> minus#(minus(f(x))) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(+(x,y)) -> minus#(y)
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(+(x,y)) -> minus#(minus(y))
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(+(x,y)) -> minus#(x)
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(+(x,y)) -> minus#(minus(x))
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(*(x,y)) -> minus#(y)
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(*(x,y)) -> minus#(minus(y))
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(*(x,y)) -> minus#(x)
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(*(x,y)) -> minus#(minus(x))
f#(minus(x)) -> minus#(minus(minus(f(x)))) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(y) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(y) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(y) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(y) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(x) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(x) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(x) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(x) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(minus(minus(y))) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(minus(minus(x))) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(minus(y)) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(minus(x)) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(y) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(y) -> minus#(+(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(y) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(y) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(y) -> minus#(*(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(y) ->
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(x) ->
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(x) -> minus#(+(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(x) ->
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(x) ->
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(x) -> minus#(*(x,y)) -> minus#(minus(minus(x)))
Restore Modifier:
DPs:
minus#(+(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(y)
minus#(*(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(minus(minus(x)))
f#(minus(x)) -> f#(x)
f#(minus(x)) -> minus#(f(x))
f#(minus(x)) -> minus#(minus(f(x)))
f#(minus(x)) -> minus#(minus(minus(f(x))))
TRS:
minus(minus(x)) -> x
minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y))))
minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))
SCC Processor:
#sccs: 2
#rules: 13
#arcs: 184/256
DPs:
f#(minus(x)) -> f#(x)
TRS:
minus(minus(x)) -> x
minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y))))
minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))
Open
DPs:
minus#(*(x,y)) -> minus#(minus(minus(x)))
minus#(*(x,y)) -> minus#(minus(x))
minus#(*(x,y)) -> minus#(x)
minus#(*(x,y)) -> minus#(minus(minus(y)))
minus#(*(x,y)) -> minus#(minus(y))
minus#(*(x,y)) -> minus#(y)
minus#(+(x,y)) -> minus#(minus(minus(x)))
minus#(+(x,y)) -> minus#(minus(x))
minus#(+(x,y)) -> minus#(x)
minus#(+(x,y)) -> minus#(minus(minus(y)))
minus#(+(x,y)) -> minus#(minus(y))
minus#(+(x,y)) -> minus#(y)
TRS:
minus(minus(x)) -> x
minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y))))
minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))
Open