YES
Problem:
log(s(x1)) -> s(log(half(s(x1))))
half(0(x1)) -> 0(s(s(half(x1))))
half(s(0(x1))) -> 0(x1)
half(s(s(x1))) -> s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) -> s(s(half(half(x1))))
p(s(s(s(x1)))) -> s(p(s(s(x1))))
s(s(p(s(x1)))) -> s(s(x1))
0(x1) -> x1
Proof:
Arctic Interpretation Processor:
dimension: 1
interpretation:
[p](x0) = x0,
[0](x0) = 4x0,
[half](x0) = x0,
[log](x0) = x0,
[s](x0) = x0
orientation:
log(s(x1)) = x1 >= x1 = s(log(half(s(x1))))
half(0(x1)) = 4x1 >= 4x1 = 0(s(s(half(x1))))
half(s(0(x1))) = 4x1 >= 4x1 = 0(x1)
half(s(s(x1))) = x1 >= x1 = s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) = x1 >= x1 = s(s(half(half(x1))))
p(s(s(s(x1)))) = x1 >= x1 = s(p(s(s(x1))))
s(s(p(s(x1)))) = x1 >= x1 = s(s(x1))
0(x1) = 4x1 >= x1 = x1
problem:
log(s(x1)) -> s(log(half(s(x1))))
half(0(x1)) -> 0(s(s(half(x1))))
half(s(0(x1))) -> 0(x1)
half(s(s(x1))) -> s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) -> s(s(half(half(x1))))
p(s(s(s(x1)))) -> s(p(s(s(x1))))
s(s(p(s(x1)))) -> s(s(x1))
Arctic Interpretation Processor:
dimension: 2
interpretation:
[0 2 ]
[p](x0) = [-& 0 ]x0,
[1 2]
[0](x0) = [0 3]x0,
[0 2]
[half](x0) = [0 0]x0,
[2 2 ]
[log](x0) = [-& 2 ]x0,
[0 0 ]
[s](x0) = [-& -&]x0
orientation:
[2 2 ] [2 2 ]
log(s(x1)) = [-& -&]x1 >= [-& -&]x1 = s(log(half(s(x1))))
[2 5] [1 3]
half(0(x1)) = [1 3]x1 >= [0 2]x1 = 0(s(s(half(x1))))
[1 3] [1 2]
half(s(0(x1))) = [1 3]x1 >= [0 3]x1 = 0(x1)
[0 0] [0 0 ]
half(s(s(x1))) = [0 0]x1 >= [-& -&]x1 = s(half(p(s(s(x1)))))
[2 2] [2 2 ]
half(half(s(s(s(s(x1)))))) = [0 0]x1 >= [-& -&]x1 = s(s(half(half(x1))))
[0 0 ] [0 0 ]
p(s(s(s(x1)))) = [-& -&]x1 >= [-& -&]x1 = s(p(s(s(x1))))
[0 0 ] [0 0 ]
s(s(p(s(x1)))) = [-& -&]x1 >= [-& -&]x1 = s(s(x1))
problem:
log(s(x1)) -> s(log(half(s(x1))))
half(s(0(x1))) -> 0(x1)
half(s(s(x1))) -> s(half(p(s(s(x1)))))
half(half(s(s(s(s(x1)))))) -> s(s(half(half(x1))))
p(s(s(s(x1)))) -> s(p(s(s(x1))))
s(s(p(s(x1)))) -> s(s(x1))
String Reversal Processor:
s(log(x1)) -> s(half(log(s(x1))))
0(s(half(x1))) -> 0(x1)
s(s(half(x1))) -> s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1))))
s(s(s(p(x1)))) -> s(s(p(s(x1))))
s(p(s(s(x1)))) -> s(s(x1))
Matrix Interpretation Processor: dim=3
interpretation:
[1 0 0]
[p](x0) = [1 0 0]x0
[0 0 0] ,
[1 1 0] [1]
[0](x0) = [0 0 0]x0 + [1]
[1 1 0] [1],
[1 0 0]
[half](x0) = [0 0 0]x0
[0 1 0] ,
[1 0 0] [1]
[log](x0) = [0 0 0]x0 + [0]
[0 0 0] [0],
[1 0 0] [0]
[s](x0) = [0 0 1]x0 + [1]
[0 0 0] [0]
orientation:
[1 0 0] [1] [1 0 0] [1]
s(log(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = s(half(log(s(x1))))
[0 0 0] [0] [0 0 0] [0]
[1 1 0] [2] [1 1 0] [1]
0(s(half(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(x1)
[1 1 0] [2] [1 1 0] [1]
[1 0 0] [0] [1 0 0] [0]
s(s(half(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = s(s(p(half(s(x1)))))
[0 0 0] [0] [0 0 0] [0]
[1 0 0] [0] [1 0 0]
s(s(s(s(half(half(x1)))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = half(half(s(s(x1))))
[0 0 0] [0] [0 0 0]
[1 0 0] [0] [1 0 0] [0]
s(s(s(p(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = s(s(p(s(x1))))
[0 0 0] [0] [0 0 0] [0]
[1 0 0] [0] [1 0 0] [0]
s(p(s(s(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = s(s(x1))
[0 0 0] [0] [0 0 0] [0]
problem:
s(log(x1)) -> s(half(log(s(x1))))
s(s(half(x1))) -> s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1))))
s(s(s(p(x1)))) -> s(s(p(s(x1))))
s(p(s(s(x1)))) -> s(s(x1))
DP Processor:
DPs:
s#(log(x1)) -> s#(x1)
s#(log(x1)) -> s#(half(log(s(x1))))
s#(s(half(x1))) -> s#(x1)
s#(s(half(x1))) -> s#(p(half(s(x1))))
s#(s(half(x1))) -> s#(s(p(half(s(x1)))))
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(p(s(x1)))
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
TRS:
s(log(x1)) -> s(half(log(s(x1))))
s(s(half(x1))) -> s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1))))
s(s(s(p(x1)))) -> s(s(p(s(x1))))
s(p(s(s(x1)))) -> s(s(x1))
EDG Processor:
DPs:
s#(log(x1)) -> s#(x1)
s#(log(x1)) -> s#(half(log(s(x1))))
s#(s(half(x1))) -> s#(x1)
s#(s(half(x1))) -> s#(p(half(s(x1))))
s#(s(half(x1))) -> s#(s(p(half(s(x1)))))
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(p(s(x1)))
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
TRS:
s(log(x1)) -> s(half(log(s(x1))))
s(s(half(x1))) -> s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1))))
s(s(s(p(x1)))) -> s(s(p(s(x1))))
s(p(s(s(x1)))) -> s(s(x1))
graph:
s#(log(x1)) -> s#(x1) -> s#(log(x1)) -> s#(x1)
s#(log(x1)) -> s#(x1) -> s#(log(x1)) -> s#(half(log(s(x1))))
s#(log(x1)) -> s#(x1) -> s#(s(half(x1))) -> s#(x1)
s#(log(x1)) -> s#(x1) -> s#(s(half(x1))) -> s#(p(half(s(x1))))
s#(log(x1)) -> s#(x1) -> s#(s(half(x1))) -> s#(s(p(half(s(x1)))))
s#(log(x1)) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(log(x1)) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(log(x1)) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1)
s#(log(x1)) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(p(s(x1)))
s#(log(x1)) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(half(x1))) -> s#(x1) -> s#(log(x1)) -> s#(x1)
s#(s(half(x1))) -> s#(x1) -> s#(log(x1)) -> s#(half(log(s(x1))))
s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1)
s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(p(half(s(x1))))
s#(s(half(x1))) -> s#(x1) ->
s#(s(half(x1))) -> s#(s(p(half(s(x1)))))
s#(s(half(x1))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(half(x1))) -> s#(x1) ->
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(half(x1))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1)
s#(s(half(x1))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(p(s(x1)))
s#(s(half(x1))) -> s#(x1) ->
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(half(x1))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(half(x1))) -> s#(p(half(s(x1))))
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(half(x1))) -> s#(s(p(half(s(x1)))))
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(s(p(x1)))) -> s#(p(s(x1)))
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(s(p(x1)))) -> s#(x1) -> s#(log(x1)) -> s#(x1)
s#(s(s(p(x1)))) -> s#(x1) -> s#(log(x1)) -> s#(half(log(s(x1))))
s#(s(s(p(x1)))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(x1) -> s#(s(half(x1))) -> s#(p(half(s(x1))))
s#(s(s(p(x1)))) -> s#(x1) ->
s#(s(half(x1))) -> s#(s(p(half(s(x1)))))
s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(x1) ->
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(p(s(x1)))
s#(s(s(p(x1)))) -> s#(x1) ->
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(half(x1))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(half(x1))) -> s#(p(half(s(x1))))
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(half(x1))) -> s#(s(p(half(s(x1)))))
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(s(p(x1)))) -> s#(p(s(x1)))
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(log(x1)) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(log(x1)) -> s#(half(log(s(x1))))
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(s(half(x1))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(s(half(x1))) -> s#(p(half(s(x1))))
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(s(half(x1))) -> s#(s(p(half(s(x1)))))
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(s(s(p(x1)))) -> s#(p(s(x1)))
s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
SCC Processor:
#sccs: 1
#rules: 6
#arcs: 56/100
DPs:
s#(log(x1)) -> s#(x1)
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(half(x1))) -> s#(x1)
TRS:
s(log(x1)) -> s(half(log(s(x1))))
s(s(half(x1))) -> s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1))))
s(s(s(p(x1)))) -> s(s(p(s(x1))))
s(p(s(s(x1)))) -> s(s(x1))
Arctic Interpretation Processor:
dimension: 1
interpretation:
[s#](x0) = 12x0,
[p](x0) = x0,
[half](x0) = x0,
[log](x0) = 8x0 + 4,
[s](x0) = x0
orientation:
s#(log(x1)) = 20x1 + 16 >= 12x1 = s#(x1)
s#(s(s(p(x1)))) = 12x1 >= 12x1 = s#(s(p(s(x1))))
s#(s(s(p(x1)))) = 12x1 >= 12x1 = s#(x1)
s#(s(s(s(half(half(x1)))))) = 12x1 >= 12x1 = s#(s(x1))
s#(s(s(s(half(half(x1)))))) = 12x1 >= 12x1 = s#(x1)
s#(s(half(x1))) = 12x1 >= 12x1 = s#(x1)
s(log(x1)) = 8x1 + 4 >= 8x1 + 4 = s(half(log(s(x1))))
s(s(half(x1))) = x1 >= x1 = s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) = x1 >= x1 = half(half(s(s(x1))))
s(s(s(p(x1)))) = x1 >= x1 = s(s(p(s(x1))))
s(p(s(s(x1)))) = x1 >= x1 = s(s(x1))
problem:
DPs:
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(half(x1))) -> s#(x1)
TRS:
s(log(x1)) -> s(half(log(s(x1))))
s(s(half(x1))) -> s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1))))
s(s(s(p(x1)))) -> s(s(p(s(x1))))
s(p(s(s(x1)))) -> s(s(x1))
EDG Processor:
DPs:
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(half(x1))) -> s#(x1)
TRS:
s(log(x1)) -> s(half(log(s(x1))))
s(s(half(x1))) -> s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1))))
s(s(s(p(x1)))) -> s(s(p(s(x1))))
s(p(s(s(x1)))) -> s(s(x1))
graph:
s#(s(half(x1))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(half(x1))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1)
s#(s(half(x1))) -> s#(x1) ->
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(half(x1))) -> s#(x1) ->
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) ->
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(half(x1))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(x1) ->
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(p(x1)))) -> s#(x1) ->
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(s(p(x1)))) -> s#(x1) ->
s#(s(half(x1))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) ->
s#(s(half(x1))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(s(s(p(x1)))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(s(s(s(half(half(x1)))))) -> s#(s(x1))
s#(s(s(s(half(half(x1)))))) -> s#(x1) ->
s#(s(s(s(half(half(x1)))))) -> s#(x1)
s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1)
Arctic Interpretation Processor:
dimension: 1
interpretation:
[s#](x0) = 5x0 + 0,
[p](x0) = -1x0 + 4,
[half](x0) = x0 + 4,
[log](x0) = 4,
[s](x0) = 1x0 + 0
orientation:
s#(s(s(p(x1)))) = 6x1 + 11 >= 6x1 + 10 = s#(s(p(s(x1))))
s#(s(s(p(x1)))) = 6x1 + 11 >= 5x1 + 0 = s#(x1)
s#(s(s(s(half(half(x1)))))) = 8x1 + 12 >= 6x1 + 5 = s#(s(x1))
s#(s(s(s(half(half(x1)))))) = 8x1 + 12 >= 5x1 + 0 = s#(x1)
s#(s(half(x1))) = 6x1 + 10 >= 5x1 + 0 = s#(x1)
s(log(x1)) = 5 >= 5 = s(half(log(s(x1))))
s(s(half(x1))) = 2x1 + 6 >= 2x1 + 6 = s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) = 4x1 + 8 >= 2x1 + 4 = half(half(s(s(x1))))
s(s(s(p(x1)))) = 2x1 + 7 >= 2x1 + 6 = s(s(p(s(x1))))
s(p(s(s(x1)))) = 2x1 + 5 >= 2x1 + 1 = s(s(x1))
problem:
DPs:
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
TRS:
s(log(x1)) -> s(half(log(s(x1))))
s(s(half(x1))) -> s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1))))
s(s(s(p(x1)))) -> s(s(p(s(x1))))
s(p(s(s(x1)))) -> s(s(x1))
EDG Processor:
DPs:
s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
TRS:
s(log(x1)) -> s(half(log(s(x1))))
s(s(half(x1))) -> s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1))))
s(s(s(p(x1)))) -> s(s(p(s(x1))))
s(p(s(s(x1)))) -> s(s(x1))
graph:
s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1))))
Matrix Interpretation Processor: dim=3
interpretation:
[s#](x0) = [0 0 1]x0 + [1],
[0 0 1]
[p](x0) = [1 0 0]x0
[0 1 0] ,
[0]
[half](x0) = [0]
[0],
[0 0 0]
[log](x0) = [1 1 1]x0
[0 0 0] ,
[0 1 0] [1]
[s](x0) = [0 0 0]x0 + [0]
[1 0 1] [0]
orientation:
s#(s(s(p(x1)))) = [1 1 1]x1 + [2] >= [1 0 1]x1 + [1] = s#(s(p(s(x1))))
[1 1 1] [1] [1]
s(log(x1)) = [0 0 0]x1 + [0] >= [0] = s(half(log(s(x1))))
[0 0 0] [0] [0]
[1] [1]
s(s(half(x1))) = [0] >= [0] = s(s(p(half(s(x1)))))
[1] [1]
[1] [0]
s(s(s(s(half(half(x1)))))) = [0] >= [0] = half(half(s(s(x1))))
[3] [0]
[0 0 0] [1] [0 0 0] [1]
s(s(s(p(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = s(s(p(s(x1))))
[1 1 1] [2] [1 1 1] [2]
[0 0 0] [2] [0 0 0] [1]
s(p(s(s(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = s(s(x1))
[1 1 1] [1] [1 1 1] [1]
problem:
DPs:
TRS:
s(log(x1)) -> s(half(log(s(x1))))
s(s(half(x1))) -> s(s(p(half(s(x1)))))
s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1))))
s(s(s(p(x1)))) -> s(s(p(s(x1))))
s(p(s(s(x1)))) -> s(s(x1))
Qed