YES Term Rewriting System R: [N, M, V] 1 -> s--osb-os-osb-Nat-csb-os-csb(0) 2 -> s--osb-os-osb-Nat-csb-os-csb(1) 3 -> s--osb-os-osb-Nat-csb-os-csb(2) 4 -> s--osb-os-osb-Nat-csb-os-csb(3) 5 -> s--osb-os-osb-Nat-csb-os-csb(4) 6 -> s--osb-os-osb-Nat-csb-os-csb(5) 7 -> s--osb-os-osb-Nat-csb-os-csb(6) 8 -> s--osb-os-osb-Nat-csb-os-csb(7) 9 -> s--osb-os-osb-Nat-csb-os-csb(8) -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> 0 -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, 0) -> 0 -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> N -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), M) -> s--osb-os-osb-Nat-csb-os-csb(-+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> true -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, N) -> true -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), 0) -> false -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) ->--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) -> not-osb-os-osb-Bool-csb-os-csb(-<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) is'Bool-osb-os-osb-Bool-csb-os-csb(V) -> tt is'Nat-osb-os-osb-Nat-csb-os-csb(V) -> tt is'NzNat-osb-os-osb-Nat-csb-os-csb(V) -> tt is'Thruth-osb-os-osb-Thruth-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-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> N sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, 0) -> N sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) Termination of R to be shown. R ->Dependency Pair Analysis R contains the following Dependency Pairs: 3' -> 2' 2' -> 1' -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), M) -> -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M) 4' -> 3' 8' -> 7' 7' -> 6' ->--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M) -> NOT-OSB-OS-OSB-BOOL-CSB-OS-CSB(-<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) ->--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M) -> -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M) -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M) SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M) 9' -> 8' 6' -> 5' 5' -> 4' -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M) Furthermore, R contains four SCCs. R ->DPs ->DP Problem 1 ->Size-Change Principle ->DP Problem 2 ->SCP ->DP Problem 3 ->SCP ->DP Problem 4 ->SCP Dependency Pair: -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), M) -> -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M) Rules: not-osb-os-osb-Bool-csb-os-csb(false) -> true not-osb-os-osb-Bool-csb-os-csb(true) -> false 3 -> s--osb-os-osb-Nat-csb-os-csb(2) 2 -> s--osb-os-osb-Nat-csb-os-csb(1) is'Nat-osb-os-osb-Nat-csb-os-csb(V) -> tt -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), M) -> s--osb-os-osb-Nat-csb-os-csb(-+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> N 4 -> s--osb-os-osb-Nat-csb-os-csb(3) 1 -> s--osb-os-osb-Nat-csb-os-csb(0) is'Thruth-osb-os-osb-Thruth-csb-os-csb(V) -> tt 8 -> s--osb-os-osb-Nat-csb-os-csb(7) 7 -> s--osb-os-osb-Nat-csb-os-csb(6) ->--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) -> not-osb-os-osb-Bool-csb-os-csb(-<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> true -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), 0) -> false -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, N) -> true -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> N sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, 0) -> N 9 -> s--osb-os-osb-Nat-csb-os-csb(8) 6 -> s--osb-os-osb-Nat-csb-os-csb(5) 5 -> s--osb-os-osb-Nat-csb-os-csb(4) is'NzNat-osb-os-osb-Nat-csb-os-csb(V) -> tt -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> 0 -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, 0) -> 0 -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) is'Bool-osb-os-osb-Bool-csb-os-csb(V) -> tt We number the DPs as follows: - -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), M) -> -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)and get the following Size-Change Graph(s): [3: -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), M) -> -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)] -> [3: -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), M) -> -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)]: [1>1, 2=2] which lead(s) to this/these maximal multigraph(s): [3: -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), M) -> -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)] -> [3: -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), M) -> -+--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)]: [1>1, 2=2] DoP: empty set Oriented Rules: none We used the order Homeomorphic Embedding Order with Non-Strict Precedence. trivial with Argument Filtering System: ([s--osb-os-osb-Nat-csb-os-csb(xo1) -> s--osb-os-osb-Nat-csb-os-csb(xo1)]) We obtain no new DP problems. R ->DPs ->DP Problem 1 ->SCP ->DP Problem 2 ->Size-Change Principle ->DP Problem 3 ->SCP ->DP Problem 4 ->SCP Dependency Pair: -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M) Rules: not-osb-os-osb-Bool-csb-os-csb(false) -> true not-osb-os-osb-Bool-csb-os-csb(true) -> false 3 -> s--osb-os-osb-Nat-csb-os-csb(2) 2 -> s--osb-os-osb-Nat-csb-os-csb(1) is'Nat-osb-os-osb-Nat-csb-os-csb(V) -> tt -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), M) -> s--osb-os-osb-Nat-csb-os-csb(-+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> N 4 -> s--osb-os-osb-Nat-csb-os-csb(3) 1 -> s--osb-os-osb-Nat-csb-os-csb(0) is'Thruth-osb-os-osb-Thruth-csb-os-csb(V) -> tt 8 -> s--osb-os-osb-Nat-csb-os-csb(7) 7 -> s--osb-os-osb-Nat-csb-os-csb(6) ->--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) -> not-osb-os-osb-Bool-csb-os-csb(-<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> true -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), 0) -> false -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, N) -> true -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> N sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, 0) -> N 9 -> s--osb-os-osb-Nat-csb-os-csb(8) 6 -> s--osb-os-osb-Nat-csb-os-csb(5) 5 -> s--osb-os-osb-Nat-csb-os-csb(4) is'NzNat-osb-os-osb-Nat-csb-os-csb(V) -> tt -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> 0 -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, 0) -> 0 -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) is'Bool-osb-os-osb-Bool-csb-os-csb(V) -> tt We number the DPs as follows: - -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)and get the following Size-Change Graph(s): [9: -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)] -> [9: -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)]: [1>1, 2>2] which lead(s) to this/these maximal multigraph(s): [9: -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)] -> [9: -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)]: [1>1, 2>2] DoP: empty set Oriented Rules: none We used the order Homeomorphic Embedding Order with Non-Strict Precedence. trivial with Argument Filtering System: ([s--osb-os-osb-Nat-csb-os-csb(xo1) -> s--osb-os-osb-Nat-csb-os-csb(xo1)]) We obtain no new DP problems. R ->DPs ->DP Problem 1 ->SCP ->DP Problem 2 ->SCP ->DP Problem 3 ->Size-Change Principle ->DP Problem 4 ->SCP Dependency Pair: SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M) Rules: not-osb-os-osb-Bool-csb-os-csb(false) -> true not-osb-os-osb-Bool-csb-os-csb(true) -> false 3 -> s--osb-os-osb-Nat-csb-os-csb(2) 2 -> s--osb-os-osb-Nat-csb-os-csb(1) is'Nat-osb-os-osb-Nat-csb-os-csb(V) -> tt -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), M) -> s--osb-os-osb-Nat-csb-os-csb(-+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> N 4 -> s--osb-os-osb-Nat-csb-os-csb(3) 1 -> s--osb-os-osb-Nat-csb-os-csb(0) is'Thruth-osb-os-osb-Thruth-csb-os-csb(V) -> tt 8 -> s--osb-os-osb-Nat-csb-os-csb(7) 7 -> s--osb-os-osb-Nat-csb-os-csb(6) ->--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) -> not-osb-os-osb-Bool-csb-os-csb(-<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> true -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), 0) -> false -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, N) -> true -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> N sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, 0) -> N 9 -> s--osb-os-osb-Nat-csb-os-csb(8) 6 -> s--osb-os-osb-Nat-csb-os-csb(5) 5 -> s--osb-os-osb-Nat-csb-os-csb(4) is'NzNat-osb-os-osb-Nat-csb-os-csb(V) -> tt -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> 0 -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, 0) -> 0 -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) is'Bool-osb-os-osb-Bool-csb-os-csb(V) -> tt We number the DPs as follows: - SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)and get the following Size-Change Graph(s): [10: SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)] -> [10: SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)]: [1>1, 2>2] which lead(s) to this/these maximal multigraph(s): [10: SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)] -> [10: SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> SD-OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)]: [1>1, 2>2] DoP: empty set Oriented Rules: none We used the order Homeomorphic Embedding Order with Non-Strict Precedence. trivial with Argument Filtering System: ([s--osb-os-osb-Nat-csb-os-csb(xo1) -> s--osb-os-osb-Nat-csb-os-csb(xo1)]) We obtain no new DP problems. R ->DPs ->DP Problem 1 ->SCP ->DP Problem 2 ->SCP ->DP Problem 3 ->SCP ->DP Problem 4 ->Size-Change Principle Dependency Pair: -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M) Rules: not-osb-os-osb-Bool-csb-os-csb(false) -> true not-osb-os-osb-Bool-csb-os-csb(true) -> false 3 -> s--osb-os-osb-Nat-csb-os-csb(2) 2 -> s--osb-os-osb-Nat-csb-os-csb(1) is'Nat-osb-os-osb-Nat-csb-os-csb(V) -> tt -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), M) -> s--osb-os-osb-Nat-csb-os-csb(-+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> N 4 -> s--osb-os-osb-Nat-csb-os-csb(3) 1 -> s--osb-os-osb-Nat-csb-os-csb(0) is'Thruth-osb-os-osb-Thruth-csb-os-csb(V) -> tt 8 -> s--osb-os-osb-Nat-csb-os-csb(7) 7 -> s--osb-os-osb-Nat-csb-os-csb(6) ->--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) -> not-osb-os-osb-Bool-csb-os-csb(-<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> true -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), 0) -> false -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, N) -> true -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> -<=--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(s--osb-os-osb-Nat-csb-os-csb(N), s--osb-os-osb-Nat-csb-os-csb(M)) -> sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M) sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> N sd-osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, 0) -> N 9 -> s--osb-os-osb-Nat-csb-os-csb(8) 6 -> s--osb-os-osb-Nat-csb-os-csb(5) 5 -> s--osb-os-osb-Nat-csb-os-csb(4) is'NzNat-osb-os-osb-Nat-csb-os-csb(V) -> tt -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(0, N) -> 0 -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, 0) -> 0 -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -+--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, -*--osb-os-osb-Nat-csb-os-csb-osb-os-osb-Nat-csb-os-csb(N, M)) is'Bool-osb-os-osb-Bool-csb-os-csb(V) -> tt We number the DPs as follows: - -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)and get the following Size-Change Graph(s): [15: -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)] -> [15: -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)]: [1=1, 2>2] which lead(s) to this/these maximal multigraph(s): [15: -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)] -> [15: -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, s--osb-os-osb-Nat-csb-os-csb(M)) -> -*--OSB-OS-OSB-NAT-CSB-OS-CSB-OSB-OS-OSB-NAT-CSB-OS-CSB(N, M)]: [1=1, 2>2] DoP: empty set Oriented Rules: none We used the order Homeomorphic Embedding Order with Non-Strict Precedence. trivial with Argument Filtering System: ([s--osb-os-osb-Nat-csb-os-csb(xo1) -> s--osb-os-osb-Nat-csb-os-csb(xo1)]) We obtain no new DP problems. Termination of R successfully shown. Duration: 0:00 minutes