YES Term Rewriting System R: [N, M, V] AC [---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb] 1 -> s--osb-os-osb-Blackboard-csb-os-csb(0) 2 -> s--osb-os-osb-Blackboard-csb-os-csb(1) 3 -> s--osb-os-osb-Blackboard-csb-os-csb(2) 4 -> s--osb-os-osb-Blackboard-csb-os-csb(3) 5 -> s--osb-os-osb-Blackboard-csb-os-csb(4) 6 -> s--osb-os-osb-Blackboard-csb-os-csb(5) 7 -> s--osb-os-osb-Blackboard-csb-os-csb(6) 8 -> s--osb-os-osb-Blackboard-csb-os-csb(7) 9 -> s--osb-os-osb-Blackboard-csb-os-csb(8) initial -> ---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(1, ---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(2, ---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(3, ---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(4, ---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(5, ---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(6, ---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(7, ---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(8, 9)))))))) -*--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(0, N) -> 0 -*--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(N, 0) -> 0 -*--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(N, s--osb-os-osb-Blackboard-csb-os-csb(M)) -> -+--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(N, -*--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(N, M)) -+--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(0, N) -> N -+--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(s--osb-os-osb-Blackboard-csb-os-csb(N), M) -> s--osb-os-osb-Blackboard-csb-os-csb(-+--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(N, M)) ---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(M, N) -> -+--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(-+--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(-*--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(M, N), M), N) -<=--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(0, N) -> true -<=--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(N, N) -> true -<=--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(s--osb-os-osb-Blackboard-csb-os-csb(N), 0) -> false -<=--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(s--osb-os-osb-Blackboard-csb-os-csb(N), s--osb-os-osb-Blackboard-csb-os-csb(M)) -> -<=--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(N, M) ->--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(N, M) -> not-osb-os-osb-Bool-csb-os-csb(-<=--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(N, M)) is'Blackboard-osb-os-osb-Blackboard-csb-os-csb(V) -> tt is'Bool-osb-os-osb-Bool-csb-os-csb(V) -> tt is'Nat-osb-os-osb-Blackboard-csb-os-csb(V) -> tt is'NzNat-osb-os-osb-Blackboard-csb-os-csb(V) -> tt not-osb-os-osb-Bool-csb-os-csb(false) -> true not-osb-os-osb-Bool-csb-os-csb(true) -> false sd-osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(0, N) -> N sd-osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(N, 0) -> N sd-osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(s--osb-os-osb-Blackboard-csb-os-csb(N), s--osb-os-osb-Blackboard-csb-os-csb(M)) -> sd-osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb(N, M) Termination of R to be shown. R ->Direct Termination Direct Termination proof successful with the following AC-Compatible Recursive Path Order with Status: Precedence: initial > 9 > 8 > 7 > 6 > 5 > 4 > 3 > 2 > 1 > s--osb-os-osb-Blackboard-csb-os-csb initial > 9 > 8 > 7 > 6 > 5 > 4 > 3 > 2 > 1 > 0 > false initial > ---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb > -*--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb > -+--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb > s--osb-os-osb-Blackboard-csb-os-csb ->--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb > -<=--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb > true ->--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb > not-osb-os-osb-Bool-csb-os-csb > true ->--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb > not-osb-os-osb-Bool-csb-os-csb > false is'Blackboard-osb-os-osb-Blackboard-csb-os-csb > tt is'Bool-osb-os-osb-Bool-csb-os-csb > tt is'Nat-osb-os-osb-Blackboard-csb-os-csb > tt is'NzNat-osb-os-osb-Blackboard-csb-os-csb > tt Status: 1: no status s--osb-os-osb-Blackboard-csb-os-csb: no status 0: no status 2: no status 3: no status 4: no status 5: no status 6: no status 7: no status 8: no status 9: no status initial: no status ---osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb: flat status -*--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb: no status -+--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb: no status -<=--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb: no status true: no status false: no status ->--osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb: no status not-osb-os-osb-Bool-csb-os-csb: no status is'Blackboard-osb-os-osb-Blackboard-csb-os-csb: no status tt: no status is'Bool-osb-os-osb-Bool-csb-os-csb: no status is'Nat-osb-os-osb-Blackboard-csb-os-csb: no status is'NzNat-osb-os-osb-Blackboard-csb-os-csb: no status sd-osb-os-osb-Blackboard-csb-os-csb-osb-os-osb-Blackboard-csb-os-csb: no status 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