YES Problem: f(f(X)) -> f(g(f(g(f(X))))) f(g(f(X))) -> f(g(X)) Proof: DP Processor: DPs: f#(f(X)) -> f#(g(f(X))) f#(f(X)) -> f#(g(f(g(f(X))))) f#(g(f(X))) -> f#(g(X)) TRS: f(f(X)) -> f(g(f(g(f(X))))) f(g(f(X))) -> f(g(X)) EDG Processor: DPs: f#(f(X)) -> f#(g(f(X))) f#(f(X)) -> f#(g(f(g(f(X))))) f#(g(f(X))) -> f#(g(X)) TRS: f(f(X)) -> f(g(f(g(f(X))))) f(g(f(X))) -> f(g(X)) graph: f#(g(f(X))) -> f#(g(X)) -> f#(g(f(X))) -> f#(g(X)) f#(f(X)) -> f#(g(f(g(f(X))))) -> f#(g(f(X))) -> f#(g(X)) f#(f(X)) -> f#(g(f(X))) -> f#(g(f(X))) -> f#(g(X)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 3/9 DPs: f#(g(f(X))) -> f#(g(X)) TRS: f(f(X)) -> f(g(f(g(f(X))))) f(g(f(X))) -> f(g(X)) Bounds Processor: bound: 3 enrichment: match automaton: final states: {3} transitions: f3(117) -> 118* f3(112) -> 113* f3(129) -> 130* f1(30) -> 31* f1(20) -> 21* f1(32) -> 33* f1(22) -> 23* f1(24) -> 25* g3(162) -> 163* g3(114) -> 115* g3(166) -> 167* g3(156) -> 157* g3(131) -> 132* g3(116) -> 117* g3(111) -> 112* g3(158) -> 159* g3(128) -> 129* g3(160) -> 161* g1(92) -> 93* g1(94) -> 95* g1(39) -> 40* g1(41) -> 42* g1(21) -> 22* g1(6) -> 7* g1(148) -> 149* g1(23) -> 24* g1(18) -> 19* f{#,1}(7) -> 8* f{#,1}(174) -> 175* f{#,1}(168) -> 169* f{#,1}(150) -> 151* f2(75) -> 76* f2(60) -> 61* f2(82) -> 83* f2(67) -> 68* f2(62) -> 63* f2(58) -> 59* f2(80) -> 81* f{#,0}(2) -> 3* f{#,0}(1) -> 3* g2(45) -> 46* g2(77) -> 78* g2(154) -> 155* g2(124) -> 125* g2(109) -> 110* g2(79) -> 80* g2(74) -> 75* g2(59) -> 60* g2(136) -> 137* g2(101) -> 102* g2(61) -> 62* g2(103) -> 104* g2(48) -> 49* g0(2) -> 1* g0(1) -> 1* f{#,2}(182) -> 183* f{#,2}(152) -> 153* f{#,2}(176) -> 177* f{#,2}(46) -> 47* f0(2) -> 2* f0(1) -> 2* 1 -> 30,18 2 -> 20,6 7 -> 32* 8 -> 3* 19 -> 7* 20 -> 77* 22 -> 79* 24 -> 67,45,41 25 -> 21,2 30 -> 74* 31 -> 21* 32 -> 58,48,39 33 -> 31,21,2 40 -> 7* 42 -> 7* 46 -> 82* 47 -> 8,3 49 -> 46* 58 -> 114* 60 -> 116* 62 -> 158,124 63 -> 68,59,25,2,20,6,77,21 67 -> 111* 68 -> 59* 75 -> 162,136 76 -> 33,31,109,23 78 -> 75* 80 -> 128,101,94 81 -> 68,59,25,2 82 -> 131,103,92 83 -> 76,59,23,33,2 93 -> 7* 95 -> 7* 102 -> 46* 104 -> 46* 110 -> 62* 112 -> 166* 113 -> 61* 115 -> 112* 117 -> 156,154,148 118 -> 76,61,33,23,31,109,63 125 -> 152,150,75 129 -> 160* 130 -> 61,63,76,23 132 -> 129* 137 -> 176,174,62 149 -> 7* 151 -> 3* 153 -> 8,3 155 -> 46* 157 -> 129* 159 -> 129* 161 -> 182,168,117 163 -> 117* 167 -> 117* 169 -> 3* 175 -> 3* 177 -> 8,3 183 -> 8,3 problem: DPs: TRS: f(f(X)) -> f(g(f(g(f(X))))) f(g(f(X))) -> f(g(X)) Qed