Term Rewriting System R:
[x, y, z]
bsort(nil) -> nil
bsort(.(x, y)) -> last(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
bubble(nil) -> nil
bubble(.(x, nil)) -> .(x, nil)
bubble(.(x, .(y, z))) -> if(<=(x, y), .(y, bubble(.(x, z))), .(x, bubble(.(y, z))))
last(nil) -> 0
last(.(x, nil)) -> x
last(.(x, .(y, z))) -> last(.(y, z))
butlast(nil) -> nil
butlast(.(x, nil)) -> nil
butlast(.(x, .(y, z))) -> .(x, butlast(.(y, z)))

Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

BSORT(.(x, y)) -> LAST(.(bubble(.(x, y)), bsort(butlast(bubble(.(x, y))))))
BSORT(.(x, y)) -> BUBBLE(.(x, y))
BSORT(.(x, y)) -> BSORT(butlast(bubble(.(x, y))))
BSORT(.(x, y)) -> BUTLAST(bubble(.(x, y)))
BUBBLE(.(x, .(y, z))) -> BUBBLE(.(x, z))
BUBBLE(.(x, .(y, z))) -> BUBBLE(.(y, z))
LAST(.(x, .(y, z))) -> LAST(.(y, z))
BUTLAST(.(x, .(y, z))) -> BUTLAST(.(y, z))

Furthermore, R contains four SCCs.


   R
DPs
       →DP Problem 1
Remaining Obligation(s)
       →DP Problem 2
Remaining Obligation(s)
       →DP Problem 3
Remaining Obligation(s)
       →DP Problem 4
Remaining Obligation(s)




The following remains to be proven:


   R
DPs
       →DP Problem 1
Remaining Obligation(s)
       →DP Problem 2
Remaining Obligation(s)
       →DP Problem 3
Remaining Obligation(s)
       →DP Problem 4
Remaining Obligation(s)




The following remains to be proven:


   R
DPs
       →DP Problem 1
Remaining Obligation(s)
       →DP Problem 2
Remaining Obligation(s)
       →DP Problem 3
Remaining Obligation(s)
       →DP Problem 4
Remaining Obligation(s)




The following remains to be proven:


   R
DPs
       →DP Problem 1
Remaining Obligation(s)
       →DP Problem 2
Remaining Obligation(s)
       →DP Problem 3
Remaining Obligation(s)
       →DP Problem 4
Remaining Obligation(s)




The following remains to be proven:

Termination of R could not be shown.
Duration:
0:09 minutes