YES TRS: {s1(s1(s0(s0(x)))) -> s0(s0(s0(s1(s1(s1(x))))))} DP: Strict: {s1#(s1(s0(s0(x)))) -> s1#(x), s1#(s1(s0(s0(x)))) -> s1#(s1(x)), s1#(s1(s0(s0(x)))) -> s1#(s1(s1(x)))} Weak: {s1(s1(s0(s0(x)))) -> s0(s0(s0(s1(s1(s1(x))))))} EDG: {(s1#(s1(s0(s0(x)))) -> s1#(x), s1#(s1(s0(s0(x)))) -> s1#(s1(s1(x)))) (s1#(s1(s0(s0(x)))) -> s1#(x), s1#(s1(s0(s0(x)))) -> s1#(s1(x))) (s1#(s1(s0(s0(x)))) -> s1#(x), s1#(s1(s0(s0(x)))) -> s1#(x)) (s1#(s1(s0(s0(x)))) -> s1#(s1(x)), s1#(s1(s0(s0(x)))) -> s1#(x)) (s1#(s1(s0(s0(x)))) -> s1#(s1(x)), s1#(s1(s0(s0(x)))) -> s1#(s1(x))) (s1#(s1(s0(s0(x)))) -> s1#(s1(x)), s1#(s1(s0(s0(x)))) -> s1#(s1(s1(x)))) (s1#(s1(s0(s0(x)))) -> s1#(s1(s1(x))), s1#(s1(s0(s0(x)))) -> s1#(x)) (s1#(s1(s0(s0(x)))) -> s1#(s1(s1(x))), s1#(s1(s0(s0(x)))) -> s1#(s1(x))) (s1#(s1(s0(s0(x)))) -> s1#(s1(s1(x))), s1#(s1(s0(s0(x)))) -> s1#(s1(s1(x))))} SCCS: Scc: {s1#(s1(s0(s0(x)))) -> s1#(x), s1#(s1(s0(s0(x)))) -> s1#(s1(x)), s1#(s1(s0(s0(x)))) -> s1#(s1(s1(x)))} SCC: Strict: {s1#(s1(s0(s0(x)))) -> s1#(x), s1#(s1(s0(s0(x)))) -> s1#(s1(x)), s1#(s1(s0(s0(x)))) -> s1#(s1(s1(x)))} Weak: {s1(s1(s0(s0(x)))) -> s0(s0(s0(s1(s1(s1(x))))))} UR: {s1(s1(s0(s0(x)))) -> s0(s0(s0(s1(s1(s1(x))))))} BOUND: Bound: match(-raise)-DP-bounded by 2 Automaton: { a_0() -> 2* s1#_2(83) -> 84* s1#_1(85) -> 86* s1#_1(48) -> 49* s1#_1(34) -> 35* s1#_1(26) -> 27* s1#_1(12) -> 13* s1#_0(50) -> 51* s1#_0(36) -> 37* s1#_0(28) -> 29* s1#_0(14) -> 15* s1#_0(4) -> 1* s1_2(82) -> 83* s1_2(81) -> 82* s1_1(97) -> 98* s1_1(96) -> 97* s1_1(87) -> 88* s1_1(76) -> 77* s1_1(59) -> 60* s1_1(54) -> 55* s1_1(47) -> 48* s1_1(46) -> 47* s1_1(33) -> 34* s1_1(32) -> 33* s1_1(25) -> 26* s1_1(24) -> 25* s1_1(11) -> 12* s1_1(10) -> 11* s1_0(91) -> 92* s1_0(90) -> 91* s1_0(89) -> 90* s1_0(71) -> 72* s1_0(70) -> 71* s1_0(65) -> 66* s1_0(64) -> 65* s1_0(52) -> 53* s1_0(41) -> 42* s1_0(40) -> 41* s1_0(38) -> 39* s1_0(30) -> 31* s1_0(19) -> 20* s1_0(18) -> 19* s1_0(16) -> 17* s1_0(5) -> 6* s1_0(3) -> 4* s1_0(2) -> 3* s0_1(100) -> 101* s0_1(99) -> 100* s0_1(98) -> 99* s0_1(79) -> 80* s0_1(78) -> 79* s0_1(77) -> 78* s0_1(62) -> 63* s0_1(61) -> 62* s0_1(60) -> 61* s0_1(57) -> 58* s0_1(56) -> 57* s0_1(55) -> 56* s0_0(94) -> 95* s0_0(93) -> 94* s0_0(92) -> 93* s0_0(74) -> 75* s0_0(73) -> 74* s0_0(72) -> 73* s0_0(68) -> 69* s0_0(67) -> 68* s0_0(66) -> 67* s0_0(44) -> 45* s0_0(43) -> 44* s0_0(42) -> 43* s0_0(22) -> 23* s0_0(21) -> 22* s0_0(20) -> 21* s0_0(8) -> 9* s0_0(7) -> 8* s0_0(6) -> 7* 101 -> 55* 95 -> 66* 88 -> 96 | 85 86 -> 35* 84 -> 35* 80 -> 33* 78 -> 87 | 85 | 81 75 -> 39* 73 -> 89* 69 -> 41* 63 -> 12* 58 -> 26* 53 -> 70 | 50 51 -> 37* 49 -> 37* 48 -> 76* 45 -> 19* 43 -> 52 | 50 | 46 39 -> 64 | 36 37 -> 29* 35 -> 29* 34 -> 54* 31 -> 40 | 28 29 -> 15* 27 -> 15* 26 -> 59* 23 -> 6* 22 -> 30 | 28 | 24 20 -> 38 | 36 | 32 17 -> 18 | 14 15 -> 1* 13 -> 1* 9 -> 4 | 3 7 -> 16 | 14 | 10 4 -> 5*} Strict: {s1#(s1(s0(s0(x)))) -> s1#(x), s1#(s1(s0(s0(x)))) -> s1#(s1(x))} EDG: {(s1#(s1(s0(s0(x)))) -> s1#(s1(x)), s1#(s1(s0(s0(x)))) -> s1#(s1(x))) (s1#(s1(s0(s0(x)))) -> s1#(s1(x)), s1#(s1(s0(s0(x)))) -> s1#(x)) (s1#(s1(s0(s0(x)))) -> s1#(x), s1#(s1(s0(s0(x)))) -> s1#(x)) (s1#(s1(s0(s0(x)))) -> s1#(x), s1#(s1(s0(s0(x)))) -> s1#(s1(x)))} SCCS: Scc: {s1#(s1(s0(s0(x)))) -> s1#(x), s1#(s1(s0(s0(x)))) -> s1#(s1(x))} SCC: Strict: {s1#(s1(s0(s0(x)))) -> s1#(x), s1#(s1(s0(s0(x)))) -> s1#(s1(x))} Weak: {s1(s1(s0(s0(x)))) -> s0(s0(s0(s1(s1(s1(x))))))} UR: {s1(s1(s0(s0(x)))) -> s0(s0(s0(s1(s1(s1(x))))))} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { b_0() -> 2* s1#_0(4) -> 5* s1#_0(2) -> 1* s1_0(42) -> 43* s1_0(41) -> 42* s1_0(40) -> 41* s1_0(35) -> 36* s1_0(34) -> 35* s1_0(33) -> 34* s1_0(28) -> 29* s1_0(27) -> 28* s1_0(26) -> 27* s1_0(21) -> 22* s1_0(20) -> 21* s1_0(19) -> 20* s1_0(14) -> 15* s1_0(13) -> 14* s1_0(12) -> 13* s1_0(7) -> 8* s1_0(6) -> 7* s1_0(3) -> 4* s0_0(45) -> 46* s0_0(44) -> 45* s0_0(43) -> 44* s0_0(38) -> 39* s0_0(37) -> 38* s0_0(36) -> 37* s0_0(31) -> 32* s0_0(30) -> 31* s0_0(29) -> 30* s0_0(24) -> 25* s0_0(23) -> 24* s0_0(22) -> 23* s0_0(17) -> 18* s0_0(16) -> 17* s0_0(15) -> 16* s0_0(10) -> 11* s0_0(9) -> 10* s0_0(8) -> 9* 46 -> 29* 39 -> 27* 37 -> 40* 32 -> 21* 25 -> 14* 23 -> 33* 18 -> 8* 17 -> 19* 15 -> 26* 11 -> 7 | 4 9 -> 12* 5 -> 1* 4 -> 6* 2 -> 3* 1 -> 5*} Strict: {s1#(s1(s0(s0(x)))) -> s1#(s1(x))} EDG: {(s1#(s1(s0(s0(x)))) -> s1#(s1(x)), s1#(s1(s0(s0(x)))) -> s1#(s1(x)))} SCCS: Scc: {s1#(s1(s0(s0(x)))) -> s1#(s1(x))} SCC: Strict: {s1#(s1(s0(s0(x)))) -> s1#(s1(x))} Weak: {s1(s1(s0(s0(x)))) -> s0(s0(s0(s1(s1(s1(x))))))} UR: {s1(s1(s0(s0(x)))) -> s0(s0(s0(s1(s1(s1(x))))))} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { c_0() -> 2* s1#_0(3) -> 1* s1_0(40) -> 41* s1_0(39) -> 40* s1_0(38) -> 39* s1_0(33) -> 34* s1_0(32) -> 33* s1_0(31) -> 32* s1_0(26) -> 27* s1_0(25) -> 26* s1_0(24) -> 25* s1_0(19) -> 20* s1_0(18) -> 19* s1_0(17) -> 18* s1_0(12) -> 13* s1_0(11) -> 12* s1_0(10) -> 11* s1_0(5) -> 6* s1_0(4) -> 5* s1_0(2) -> 3* s0_0(43) -> 44* s0_0(42) -> 43* s0_0(41) -> 42* s0_0(36) -> 37* s0_0(35) -> 36* s0_0(34) -> 35* s0_0(29) -> 30* s0_0(28) -> 29* s0_0(27) -> 28* s0_0(22) -> 23* s0_0(21) -> 22* s0_0(20) -> 21* s0_0(15) -> 16* s0_0(14) -> 15* s0_0(13) -> 14* s0_0(8) -> 9* s0_0(7) -> 8* s0_0(6) -> 7* 44 -> 27* 37 -> 25* 35 -> 38* 30 -> 19* 23 -> 12* 21 -> 31* 16 -> 6* 15 -> 17* 13 -> 24* 9 -> 5 | 3 7 -> 10* 3 -> 4*} Strict: {} Qed