YES Termination Proof using AProVETerm Rewriting System R:
[I, N, I1, M, z, y, x]
1 -> s-osb-Nat-comma-Morituri-csb(0)
initial-osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(1, I) -> ---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(dagger-osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(I, I), 1)
initial-osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(s-osb-Nat-comma-Morituri-csb(N), I) -> ---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(initial-osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(N, I), s-osb-Nat-comma-Morituri-csb(N))
ocb---ccb-osb-Nat-comma-Morituri-csb(---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(dagger-osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(1, I), ---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(I1, M))) -> ocb---ccb-osb-Nat-comma-Morituri-csb(---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(dagger-osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(I, I), M))
ocb---ccb-osb-Nat-comma-Morituri-csb(---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(dagger-osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(N, I), I1)) -> ocb---ccb-osb-Nat-comma-Morituri-csb(I1)
ocb---ccb-osb-Nat-comma-Morituri-csb(---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(dagger-osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(s-osb-Nat-comma-Morituri-csb(N), I), ---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(I1, M))) -> ocb---ccb-osb-Nat-comma-Morituri-csb(---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(dagger-osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(N, I), ---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(M, I1)))
---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(x, y), z) == ---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(x, ---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb(y, z))

Termination of R to be shown. 



   R
     ↳Direct Termination



Direct Termination proof successful with the following AC-Compatible Recursive Path Order with Status:
Precedence:
1 > s-osb-Nat-comma-Morituri-csb
1 > 0
initial-osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb > ---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb > dagger-osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb

Status:
---osb-Nat-comma-Morituri-csb-osb-Nat-comma-Morituri-csb: flat

Removing all rules.


   R
     ↳Direct
       →TRS2
         ↳Dependency Pair Analysis



R contains no Dependency Pairs and therefore no SCCs.

Termination of R successfully shown.
Duration:
0:00 minutes