YES(?,O(n^1)) TRS: { f f X -> f a b f X, f a g X -> b X, b X -> a X} DUP: We consider a non-duplicating system. Trs: { f f X -> f a b f X, f a g X -> b X, b X -> a X} BOUND: Bound: match(-raise)-bounded by 4 Automaton: { b_3(44) -> 45* b_2(37) -> 38* b_2(25) -> 26* b_1(12) -> 13* b_1(9) -> 10* b_1(7) -> 8* b_0(2) -> 1* b_0(1) -> 1* a_4(48) -> 49* a_3(45) -> 46* a_3(39) -> 40* a_3(29) -> 30* a_2(26) -> 27* a_2(22) -> 23* a_2(20) -> 21* a_2(18) -> 19* a_1(13) -> 14* a_1(5) -> 6* a_1(3) -> 4* a_0(2) -> 1* a_0(1) -> 1* g_0(2) -> 2* g_0(1) -> 2* f_3(46) -> 47* f_3(43) -> 44* f_2(41) -> 42* f_2(35) -> 36* f_2(33) -> 34* f_2(27) -> 28* f_2(24) -> 25* f_1(31) -> 32* f_1(16) -> 17* f_1(14) -> 15* f_1(11) -> 12* f_0(2) -> 1* f_0(1) -> 1* 49 -> 45* 47 -> 34* 44 -> 48* 42 -> 37* 40 -> 38* 38 -> 26* 37 -> 39* 36 -> 25* 34 -> 25* 32 -> 12* 31 -> 41* 30 -> 26* 28 -> 37 | 34 | 12 27 -> 43 | 31 25 -> 29* 23 -> 13* 21 -> 10* 19 -> 8* 17 -> 12* 16 -> 35* 15 -> 12 | 1 14 -> 24* 12 -> 34 | 22 | 1 11 -> 33* 10 -> 34 | 12 | 1 9 -> 20* 8 -> 34 | 12 | 1 7 -> 18* 6 -> 1* 4 -> 1* 2 -> 16 | 9 | 5 1 -> 11 | 7 | 3 } Strict: {} Qed