YES TRS: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} DP: Strict: {g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(x, g(y, g(x, y))) -> g#(y, b()), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(e(), g(e(), x)) -> g#(c(), x), g#(d(), g(d(), x)) -> g#(e(), x), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(c(), g(c(), x)) -> g#(d(), x), f#(g(x, y)) -> g#(y, g(f(f(x)), a())), f#(g(x, y)) -> g#(f(f(x)), a()), f#(g(x, y)) -> f#(x), f#(g(x, y)) -> f#(f(x))} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} EDG: {(g#(e(), g(e(), x)) -> g#(c(), x), g#(c(), g(c(), x)) -> g#(d(), x)) (g#(e(), g(e(), x)) -> g#(c(), x), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))) (g#(e(), g(e(), x)) -> g#(c(), x), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(e(), g(e(), x)) -> g#(c(), x), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(e(), g(e(), x)) -> g#(c(), x), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(c(), g(c(), x)) -> g#(d(), x), g#(d(), g(d(), x)) -> g#(c(), g(e(), x))) (g#(c(), g(c(), x)) -> g#(d(), x), g#(d(), g(d(), x)) -> g#(e(), x)) (g#(c(), g(c(), x)) -> g#(d(), x), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(c(), g(c(), x)) -> g#(d(), x), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(c(), g(c(), x)) -> g#(d(), x), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(c(), g(c(), x)) -> g#(d(), x)) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(d(), g(d(), x)) -> g#(c(), g(e(), x))) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(d(), g(d(), x)) -> g#(e(), x)) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(e(), g(e(), x)) -> g#(c(), x)) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(e(), g(e(), x)) -> g#(d(), g(c(), x))) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(c(), g(e(), x))) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(e(), x)) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(e(), g(e(), x)) -> g#(c(), x)) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(e(), g(e(), x)) -> g#(d(), g(c(), x))) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (f#(g(x, y)) -> f#(f(x)), f#(g(x, y)) -> g#(y, g(f(f(x)), a()))) (f#(g(x, y)) -> f#(f(x)), f#(g(x, y)) -> g#(f(f(x)), a())) (f#(g(x, y)) -> f#(f(x)), f#(g(x, y)) -> f#(x)) (f#(g(x, y)) -> f#(f(x)), f#(g(x, y)) -> f#(f(x))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(d(), x)) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(e(), g(e(), x)) -> g#(d(), g(c(), x))) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(e(), g(e(), x)) -> g#(c(), x)) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(d(), g(d(), x)) -> g#(e(), x)) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(d(), g(d(), x)) -> g#(c(), g(e(), x))) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(c(), g(c(), x)) -> g#(d(), x)) (f#(g(x, y)) -> f#(x), f#(g(x, y)) -> g#(y, g(f(f(x)), a()))) (f#(g(x, y)) -> f#(x), f#(g(x, y)) -> g#(f(f(x)), a())) (f#(g(x, y)) -> f#(x), f#(g(x, y)) -> f#(x)) (f#(g(x, y)) -> f#(x), f#(g(x, y)) -> f#(f(x))) (g#(d(), g(d(), x)) -> g#(e(), x), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(d(), g(d(), x)) -> g#(e(), x), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(d(), g(d(), x)) -> g#(e(), x), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(d(), g(d(), x)) -> g#(e(), x), g#(e(), g(e(), x)) -> g#(d(), g(c(), x))) (g#(d(), g(d(), x)) -> g#(e(), x), g#(e(), g(e(), x)) -> g#(c(), x)) (g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))))} SCCS: Scc: {f#(g(x, y)) -> f#(x), f#(g(x, y)) -> f#(f(x))} Scc: {g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(e(), g(e(), x)) -> g#(c(), x), g#(d(), g(d(), x)) -> g#(e(), x), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(c(), g(c(), x)) -> g#(d(), x)} SCC: Strict: {f#(g(x, y)) -> f#(x), f#(g(x, y)) -> f#(f(x))} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} BOUND: Bound: match(-raise)-bounded by 1 Automaton: { h_0() -> 2* b_1() -> 41* | 37 | 17 b_0() -> 17* a_1() -> 42* | 35 | 5 a_0() -> 5* f#_1(52) -> 26* f#_1(50) -> 26* f#_1(40) -> 26* f#_1(2) -> 26* f#_0(52) -> 26* f#_0(50) -> 26* f#_0(49) -> 26* f#_0(40) -> 26* f#_0(27) -> 26* f#_0(3) -> 26* f#_0(2) -> 26* f_1(52) -> 52* | 50 | 49 | 40 | 4 | 3 | 2 f_1(50) -> 52* | 50 | 49 | 40 | 4 | 3 | 2 f_1(40) -> 52* | 50 | 49 | 40 | 4 | 3 | 2 f_1(2) -> 40* | 3 | 2 f_0(52) -> 49* | 4 | 3 f_0(50) -> 49* | 4 | 3 f_0(49) -> 4* f_0(40) -> 49* | 4 | 3 f_0(27) -> 4* f_0(3) -> 4* f_0(2) -> 3* c_1() -> 43* | 32 | 12 c_0() -> 12* d_1() -> 44* | 30 | 9 d_0() -> 9* e_1() -> 45* | 29 | 8 e_0() -> 8* g_1(53, 53) -> 4* g_1(53, 36) -> 4* g_1(52, 42) -> 53* | 36 | 6 g_1(52, 35) -> 36* g_1(50, 42) -> 53* | 36 | 6 g_1(50, 35) -> 36* g_1(45, 46) -> 19* g_1(45, 41) -> 48* | 34 | 18 g_1(45, 31) -> 19* g_1(45, 17) -> 48* | 34 | 18 g_1(44, 51) -> 19* g_1(44, 41) -> 46* | 31 | 22 g_1(44, 33) -> 19* g_1(44, 17) -> 46* | 31 | 22 g_1(43, 48) -> 19* g_1(43, 41) -> 51* | 33 | 18 g_1(43, 34) -> 19* g_1(43, 17) -> 51* | 33 | 18 g_1(42, 54) -> 23* g_1(42, 47) -> 54* | 39 | 19 g_1(42, 39) -> 23* g_1(42, 38) -> 39* g_1(41, 41) -> 47* | 38 | 18 g_1(41, 37) -> 38* g_1(40, 42) -> 36* g_1(40, 35) -> 36* g_1(35, 54) -> 23* g_1(35, 39) -> 23* g_1(32, 48) -> 19* g_1(32, 41) -> 33* g_1(32, 34) -> 19* g_1(32, 17) -> 33* g_1(30, 51) -> 19* g_1(30, 41) -> 31* g_1(30, 33) -> 19* g_1(30, 17) -> 31* g_1(29, 46) -> 19* g_1(29, 41) -> 34* g_1(29, 31) -> 19* g_1(29, 17) -> 34* g_1(17, 41) -> 47* | 38 | 18 g_1(17, 37) -> 38* g_1(6, 53) -> 4* g_1(6, 36) -> 4* g_1(5, 47) -> 54* | 39 | 19 g_1(5, 38) -> 39* g_1(2, 42) -> 36* g_1(2, 35) -> 36* g_0(54, 51) -> 19* g_0(54, 48) -> 19* g_0(54, 47) -> 19* g_0(54, 46) -> 19* g_0(54, 41) -> 22* g_0(54, 22) -> 19* g_0(54, 18) -> 19* g_0(54, 17) -> 22* g_0(53, 53) -> 4* g_0(53, 6) -> 4* g_0(52, 53) -> 27* g_0(52, 51) -> 19* g_0(52, 48) -> 19* g_0(52, 47) -> 19* g_0(52, 46) -> 19* g_0(52, 42) -> 6* g_0(52, 41) -> 18* g_0(52, 22) -> 19* g_0(52, 18) -> 19* g_0(52, 17) -> 18* g_0(52, 6) -> 27* g_0(52, 5) -> 6* g_0(51, 51) -> 19* g_0(51, 48) -> 19* g_0(51, 47) -> 19* g_0(51, 46) -> 19* g_0(51, 41) -> 22* g_0(51, 22) -> 19* g_0(51, 18) -> 19* g_0(51, 17) -> 22* g_0(50, 53) -> 27* g_0(50, 51) -> 19* g_0(50, 48) -> 19* g_0(50, 47) -> 19* g_0(50, 46) -> 19* g_0(50, 42) -> 6* g_0(50, 41) -> 18* g_0(50, 22) -> 19* g_0(50, 18) -> 19* g_0(50, 17) -> 18* g_0(50, 6) -> 27* g_0(50, 5) -> 6* g_0(49, 42) -> 6* g_0(49, 5) -> 6* g_0(48, 51) -> 19* g_0(48, 48) -> 19* g_0(48, 47) -> 19* g_0(48, 46) -> 19* g_0(48, 41) -> 22* g_0(48, 22) -> 19* g_0(48, 18) -> 19* g_0(48, 17) -> 22* g_0(47, 51) -> 19* g_0(47, 48) -> 19* g_0(47, 47) -> 19* g_0(47, 46) -> 19* g_0(47, 41) -> 22* g_0(47, 22) -> 19* g_0(47, 18) -> 19* g_0(47, 17) -> 22* g_0(46, 51) -> 19* g_0(46, 48) -> 19* g_0(46, 47) -> 19* g_0(46, 46) -> 19* g_0(46, 41) -> 22* g_0(46, 22) -> 19* g_0(46, 18) -> 19* g_0(46, 17) -> 22* g_0(45, 52) -> 15* g_0(45, 51) -> 19* g_0(45, 50) -> 15* g_0(45, 48) -> 19* g_0(45, 47) -> 19* g_0(45, 46) -> 19* g_0(45, 41) -> 18* g_0(45, 40) -> 15* g_0(45, 28) -> 24* g_0(45, 23) -> 24* g_0(45, 22) -> 19* g_0(45, 18) -> 19* g_0(45, 17) -> 18* g_0(45, 10) -> 24* g_0(45, 2) -> 15* g_0(44, 52) -> 10* g_0(44, 51) -> 19* g_0(44, 50) -> 10* g_0(44, 48) -> 19* g_0(44, 47) -> 19* g_0(44, 46) -> 19* g_0(44, 41) -> 22* g_0(44, 40) -> 10* g_0(44, 24) -> 25* g_0(44, 23) -> 25* g_0(44, 22) -> 19* g_0(44, 18) -> 19* g_0(44, 17) -> 22* g_0(44, 13) -> 25* g_0(44, 2) -> 10* g_0(43, 52) -> 13* g_0(43, 51) -> 19* g_0(43, 50) -> 13* g_0(43, 48) -> 19* g_0(43, 47) -> 19* g_0(43, 46) -> 19* g_0(43, 41) -> 18* g_0(43, 40) -> 13* g_0(43, 25) -> 28* g_0(43, 23) -> 28* g_0(43, 22) -> 19* g_0(43, 18) -> 19* g_0(43, 17) -> 18* g_0(43, 15) -> 28* g_0(43, 2) -> 13* g_0(42, 54) -> 23* g_0(42, 51) -> 19* g_0(42, 48) -> 19* g_0(42, 47) -> 19* g_0(42, 46) -> 19* g_0(42, 41) -> 18* g_0(42, 22) -> 19* g_0(42, 19) -> 23* g_0(42, 18) -> 19* g_0(42, 17) -> 18* g_0(41, 51) -> 19* g_0(41, 48) -> 19* g_0(41, 47) -> 19* g_0(41, 46) -> 19* g_0(41, 41) -> 18* g_0(41, 22) -> 19* g_0(41, 18) -> 19* g_0(41, 17) -> 18* g_0(40, 53) -> 27* g_0(40, 51) -> 19* g_0(40, 48) -> 19* g_0(40, 47) -> 19* g_0(40, 46) -> 19* g_0(40, 41) -> 18* g_0(40, 22) -> 19* g_0(40, 18) -> 19* g_0(40, 17) -> 18* g_0(40, 6) -> 27* g_0(28, 51) -> 19* g_0(28, 48) -> 19* g_0(28, 47) -> 19* g_0(28, 46) -> 19* g_0(28, 41) -> 22* g_0(28, 22) -> 19* g_0(28, 18) -> 19* g_0(28, 17) -> 22* g_0(25, 51) -> 19* g_0(25, 48) -> 19* g_0(25, 47) -> 19* g_0(25, 46) -> 19* g_0(25, 41) -> 22* g_0(25, 22) -> 19* g_0(25, 18) -> 19* g_0(25, 17) -> 22* g_0(24, 51) -> 19* g_0(24, 48) -> 19* g_0(24, 47) -> 19* g_0(24, 46) -> 19* g_0(24, 41) -> 22* g_0(24, 22) -> 19* g_0(24, 18) -> 19* g_0(24, 17) -> 22* g_0(23, 51) -> 19* g_0(23, 48) -> 19* g_0(23, 47) -> 19* g_0(23, 46) -> 19* g_0(23, 41) -> 22* g_0(23, 22) -> 19* g_0(23, 18) -> 19* g_0(23, 17) -> 22* g_0(22, 51) -> 19* g_0(22, 48) -> 19* g_0(22, 47) -> 19* g_0(22, 46) -> 19* g_0(22, 41) -> 22* g_0(22, 22) -> 19* g_0(22, 18) -> 19* g_0(22, 17) -> 22* g_0(19, 51) -> 19* g_0(19, 48) -> 19* g_0(19, 47) -> 19* g_0(19, 46) -> 19* g_0(19, 41) -> 22* g_0(19, 22) -> 19* g_0(19, 18) -> 19* g_0(19, 17) -> 22* g_0(18, 51) -> 19* g_0(18, 48) -> 19* g_0(18, 47) -> 19* g_0(18, 46) -> 19* g_0(18, 41) -> 22* g_0(18, 22) -> 19* g_0(18, 18) -> 19* g_0(18, 17) -> 22* g_0(17, 51) -> 19* g_0(17, 48) -> 19* g_0(17, 47) -> 19* g_0(17, 46) -> 19* g_0(17, 41) -> 18* g_0(17, 22) -> 19* g_0(17, 18) -> 19* g_0(17, 17) -> 18* g_0(15, 51) -> 19* g_0(15, 48) -> 19* g_0(15, 47) -> 19* g_0(15, 46) -> 19* g_0(15, 41) -> 22* g_0(15, 22) -> 19* g_0(15, 18) -> 19* g_0(15, 17) -> 22* g_0(13, 51) -> 19* g_0(13, 48) -> 19* g_0(13, 47) -> 19* g_0(13, 46) -> 19* g_0(13, 41) -> 22* g_0(13, 22) -> 19* g_0(13, 18) -> 19* g_0(13, 17) -> 22* g_0(12, 52) -> 13* g_0(12, 51) -> 19* g_0(12, 50) -> 13* g_0(12, 48) -> 19* g_0(12, 47) -> 19* g_0(12, 46) -> 19* g_0(12, 41) -> 18* g_0(12, 40) -> 13* g_0(12, 25) -> 28* g_0(12, 23) -> 28* g_0(12, 22) -> 19* g_0(12, 18) -> 19* g_0(12, 17) -> 18* g_0(12, 15) -> 28* g_0(12, 2) -> 13* g_0(10, 51) -> 19* g_0(10, 48) -> 19* g_0(10, 47) -> 19* g_0(10, 46) -> 19* g_0(10, 41) -> 22* g_0(10, 22) -> 19* g_0(10, 18) -> 19* g_0(10, 17) -> 22* g_0(9, 52) -> 10* g_0(9, 51) -> 19* g_0(9, 50) -> 10* g_0(9, 48) -> 19* g_0(9, 47) -> 19* g_0(9, 46) -> 19* g_0(9, 41) -> 22* g_0(9, 40) -> 10* g_0(9, 24) -> 25* g_0(9, 23) -> 25* g_0(9, 22) -> 19* g_0(9, 18) -> 19* g_0(9, 17) -> 22* g_0(9, 13) -> 25* g_0(9, 2) -> 10* g_0(8, 52) -> 15* g_0(8, 51) -> 19* g_0(8, 50) -> 15* g_0(8, 48) -> 19* g_0(8, 47) -> 19* g_0(8, 46) -> 19* g_0(8, 41) -> 18* g_0(8, 40) -> 15* g_0(8, 28) -> 24* g_0(8, 23) -> 24* g_0(8, 22) -> 19* g_0(8, 18) -> 19* g_0(8, 17) -> 18* g_0(8, 10) -> 24* g_0(8, 2) -> 15* g_0(6, 53) -> 4* g_0(6, 6) -> 4* g_0(5, 54) -> 23* g_0(5, 51) -> 19* g_0(5, 48) -> 19* g_0(5, 47) -> 19* g_0(5, 46) -> 19* g_0(5, 41) -> 18* g_0(5, 22) -> 19* g_0(5, 19) -> 23* g_0(5, 18) -> 19* g_0(5, 17) -> 18* g_0(4, 42) -> 6* g_0(4, 5) -> 6* g_0(2, 53) -> 27* g_0(2, 51) -> 19* g_0(2, 48) -> 19* g_0(2, 47) -> 19* g_0(2, 46) -> 19* g_0(2, 41) -> 18* g_0(2, 22) -> 19* g_0(2, 18) -> 19* g_0(2, 17) -> 18* g_0(2, 6) -> 27*} Strict: {} Qed SCC: Strict: {g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(e(), g(e(), x)) -> g#(c(), x), g#(d(), g(d(), x)) -> g#(e(), x), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(c(), g(c(), x)) -> g#(d(), x)} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} POLY: Argument Filtering: pi(b) = [], pi(a) = [], pi(f) = [], pi(c) = [], pi(d) = [], pi(e) = [], pi(g#) = 1, pi(g) = [1] Usable Rules: {} Interpretation: [g](x0) = x0 + 1, [b] = 0 Strict: {g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} EDG: {(g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(c(), g(e(), x))) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(e(), g(e(), x)) -> g#(d(), g(c(), x))) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))) (g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))))} SCCS: Scc: {g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))} Scc: {g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))} SCC: Strict: {g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} BOUND: Bound: match(-raise)-bounded by 1 Automaton: { i_0() -> 2* b_1() -> 43* | 39 | 17 b_0() -> 17* a_1() -> 44* | 37 | 5 a_0() -> 5* f_1(42) -> 52* | 36 | 4 f_1(35) -> 36* f_1(2) -> 42* | 35 | 3 f_0(42) -> 4* f_0(27) -> 4* f_0(3) -> 4* f_0(2) -> 3* c_1() -> 45* | 32 | 12 c_0() -> 12* d_1() -> 46* | 30 | 9 d_0() -> 9* e_1() -> 47* | 29 | 8 e_0() -> 8* g#_0(47, 28) -> 20* g#_0(47, 24) -> 20* g#_0(47, 10) -> 20* g#_0(46, 25) -> 21* g#_0(46, 24) -> 21* g#_0(46, 13) -> 21* g#_0(45, 26) -> 22* g#_0(45, 24) -> 22* g#_0(45, 15) -> 22* g#_0(12, 26) -> 22* g#_0(12, 24) -> 22* g#_0(12, 15) -> 22* g#_0(9, 25) -> 21* g#_0(9, 24) -> 21* g#_0(9, 13) -> 21* g#_0(8, 28) -> 20* g#_0(8, 24) -> 20* g#_0(8, 10) -> 20* g_1(53, 53) -> 4* g_1(53, 38) -> 4* g_1(52, 44) -> 53* | 38 | 6 g_1(52, 37) -> 38* g_1(47, 50) -> 19* g_1(47, 43) -> 49* | 34 | 18 g_1(47, 31) -> 19* g_1(47, 17) -> 49* | 34 | 18 g_1(46, 48) -> 19* g_1(46, 43) -> 50* | 31 | 23 g_1(46, 33) -> 19* g_1(46, 17) -> 50* | 31 | 23 g_1(45, 49) -> 19* g_1(45, 43) -> 48* | 33 | 18 g_1(45, 34) -> 19* g_1(45, 17) -> 48* | 33 | 18 g_1(44, 54) -> 24* g_1(44, 51) -> 54* | 41 | 19 g_1(44, 41) -> 24* g_1(44, 40) -> 41* g_1(43, 43) -> 51* | 40 | 18 g_1(43, 39) -> 40* g_1(37, 54) -> 24* g_1(37, 41) -> 24* g_1(36, 44) -> 38* g_1(36, 37) -> 38* g_1(32, 49) -> 19* g_1(32, 43) -> 33* g_1(32, 34) -> 19* g_1(32, 17) -> 33* g_1(30, 48) -> 19* g_1(30, 43) -> 31* g_1(30, 33) -> 19* g_1(30, 17) -> 31* g_1(29, 50) -> 19* g_1(29, 43) -> 34* g_1(29, 31) -> 19* g_1(29, 17) -> 34* g_1(17, 43) -> 51* | 40 | 18 g_1(17, 39) -> 40* g_1(6, 53) -> 4* g_1(6, 38) -> 4* g_1(5, 51) -> 54* | 41 | 19 g_1(5, 40) -> 41* g_0(54, 51) -> 19* g_0(54, 50) -> 19* g_0(54, 49) -> 19* g_0(54, 48) -> 19* g_0(54, 43) -> 23* g_0(54, 23) -> 19* g_0(54, 18) -> 19* g_0(54, 17) -> 23* g_0(53, 53) -> 4* g_0(53, 6) -> 4* g_0(52, 44) -> 6* g_0(52, 5) -> 6* g_0(51, 51) -> 19* g_0(51, 50) -> 19* g_0(51, 49) -> 19* g_0(51, 48) -> 19* g_0(51, 43) -> 23* g_0(51, 23) -> 19* g_0(51, 18) -> 19* g_0(51, 17) -> 23* g_0(50, 51) -> 19* g_0(50, 50) -> 19* g_0(50, 49) -> 19* g_0(50, 48) -> 19* g_0(50, 43) -> 23* g_0(50, 23) -> 19* g_0(50, 18) -> 19* g_0(50, 17) -> 23* g_0(49, 51) -> 19* g_0(49, 50) -> 19* g_0(49, 49) -> 19* g_0(49, 48) -> 19* g_0(49, 43) -> 23* g_0(49, 23) -> 19* g_0(49, 18) -> 19* g_0(49, 17) -> 23* g_0(48, 51) -> 19* g_0(48, 50) -> 19* g_0(48, 49) -> 19* g_0(48, 48) -> 19* g_0(48, 43) -> 23* g_0(48, 23) -> 19* g_0(48, 18) -> 19* g_0(48, 17) -> 23* g_0(47, 51) -> 19* g_0(47, 50) -> 19* g_0(47, 49) -> 19* g_0(47, 48) -> 19* g_0(47, 43) -> 18* g_0(47, 28) -> 25* g_0(47, 24) -> 25* g_0(47, 23) -> 19* g_0(47, 18) -> 19* g_0(47, 17) -> 18* g_0(47, 10) -> 25* g_0(47, 2) -> 15* g_0(46, 51) -> 19* g_0(46, 50) -> 19* g_0(46, 49) -> 19* g_0(46, 48) -> 19* g_0(46, 43) -> 23* g_0(46, 25) -> 26* g_0(46, 24) -> 26* g_0(46, 23) -> 19* g_0(46, 18) -> 19* g_0(46, 17) -> 23* g_0(46, 13) -> 26* g_0(46, 2) -> 10* g_0(45, 51) -> 19* g_0(45, 50) -> 19* g_0(45, 49) -> 19* g_0(45, 48) -> 19* g_0(45, 43) -> 18* g_0(45, 26) -> 28* g_0(45, 24) -> 28* g_0(45, 23) -> 19* g_0(45, 18) -> 19* g_0(45, 17) -> 18* g_0(45, 15) -> 28* g_0(45, 2) -> 13* g_0(44, 54) -> 24* g_0(44, 51) -> 19* g_0(44, 50) -> 19* g_0(44, 49) -> 19* g_0(44, 48) -> 19* g_0(44, 43) -> 18* g_0(44, 23) -> 19* g_0(44, 19) -> 24* g_0(44, 18) -> 19* g_0(44, 17) -> 18* g_0(43, 51) -> 19* g_0(43, 50) -> 19* g_0(43, 49) -> 19* g_0(43, 48) -> 19* g_0(43, 43) -> 18* g_0(43, 23) -> 19* g_0(43, 18) -> 19* g_0(43, 17) -> 18* g_0(28, 51) -> 19* g_0(28, 50) -> 19* g_0(28, 49) -> 19* g_0(28, 48) -> 19* g_0(28, 43) -> 23* g_0(28, 23) -> 19* g_0(28, 18) -> 19* g_0(28, 17) -> 23* g_0(26, 51) -> 19* g_0(26, 50) -> 19* g_0(26, 49) -> 19* g_0(26, 48) -> 19* g_0(26, 43) -> 23* g_0(26, 23) -> 19* g_0(26, 18) -> 19* g_0(26, 17) -> 23* g_0(25, 51) -> 19* g_0(25, 50) -> 19* g_0(25, 49) -> 19* g_0(25, 48) -> 19* g_0(25, 43) -> 23* g_0(25, 23) -> 19* g_0(25, 18) -> 19* g_0(25, 17) -> 23* g_0(24, 51) -> 19* g_0(24, 50) -> 19* g_0(24, 49) -> 19* g_0(24, 48) -> 19* g_0(24, 43) -> 23* g_0(24, 23) -> 19* g_0(24, 18) -> 19* g_0(24, 17) -> 23* g_0(23, 51) -> 19* g_0(23, 50) -> 19* g_0(23, 49) -> 19* g_0(23, 48) -> 19* g_0(23, 43) -> 23* g_0(23, 23) -> 19* g_0(23, 18) -> 19* g_0(23, 17) -> 23* g_0(19, 51) -> 19* g_0(19, 50) -> 19* g_0(19, 49) -> 19* g_0(19, 48) -> 19* g_0(19, 43) -> 23* g_0(19, 23) -> 19* g_0(19, 18) -> 19* g_0(19, 17) -> 23* g_0(18, 51) -> 19* g_0(18, 50) -> 19* g_0(18, 49) -> 19* g_0(18, 48) -> 19* g_0(18, 43) -> 23* g_0(18, 23) -> 19* g_0(18, 18) -> 19* g_0(18, 17) -> 23* g_0(17, 51) -> 19* g_0(17, 50) -> 19* g_0(17, 49) -> 19* g_0(17, 48) -> 19* g_0(17, 43) -> 18* g_0(17, 23) -> 19* g_0(17, 18) -> 19* g_0(17, 17) -> 18* g_0(15, 51) -> 19* g_0(15, 50) -> 19* g_0(15, 49) -> 19* g_0(15, 48) -> 19* g_0(15, 43) -> 23* g_0(15, 23) -> 19* g_0(15, 18) -> 19* g_0(15, 17) -> 23* g_0(13, 51) -> 19* g_0(13, 50) -> 19* g_0(13, 49) -> 19* g_0(13, 48) -> 19* g_0(13, 43) -> 23* g_0(13, 23) -> 19* g_0(13, 18) -> 19* g_0(13, 17) -> 23* g_0(12, 51) -> 19* g_0(12, 50) -> 19* g_0(12, 49) -> 19* g_0(12, 48) -> 19* g_0(12, 43) -> 18* g_0(12, 26) -> 28* g_0(12, 24) -> 28* g_0(12, 23) -> 19* g_0(12, 18) -> 19* g_0(12, 17) -> 18* g_0(12, 15) -> 28* g_0(12, 2) -> 13* g_0(10, 51) -> 19* g_0(10, 50) -> 19* g_0(10, 49) -> 19* g_0(10, 48) -> 19* g_0(10, 43) -> 23* g_0(10, 23) -> 19* g_0(10, 18) -> 19* g_0(10, 17) -> 23* g_0(9, 51) -> 19* g_0(9, 50) -> 19* g_0(9, 49) -> 19* g_0(9, 48) -> 19* g_0(9, 43) -> 23* g_0(9, 25) -> 26* g_0(9, 24) -> 26* g_0(9, 23) -> 19* g_0(9, 18) -> 19* g_0(9, 17) -> 23* g_0(9, 13) -> 26* g_0(9, 2) -> 10* g_0(8, 51) -> 19* g_0(8, 50) -> 19* g_0(8, 49) -> 19* g_0(8, 48) -> 19* g_0(8, 43) -> 18* g_0(8, 28) -> 25* g_0(8, 24) -> 25* g_0(8, 23) -> 19* g_0(8, 18) -> 19* g_0(8, 17) -> 18* g_0(8, 10) -> 25* g_0(8, 2) -> 15* g_0(6, 53) -> 4* g_0(6, 6) -> 4* g_0(5, 54) -> 24* g_0(5, 51) -> 19* g_0(5, 50) -> 19* g_0(5, 49) -> 19* g_0(5, 48) -> 19* g_0(5, 43) -> 18* g_0(5, 23) -> 19* g_0(5, 19) -> 24* g_0(5, 18) -> 19* g_0(5, 17) -> 18* g_0(4, 44) -> 6* g_0(4, 5) -> 6* g_0(2, 53) -> 27* g_0(2, 51) -> 19* g_0(2, 50) -> 19* g_0(2, 49) -> 19* g_0(2, 48) -> 19* g_0(2, 43) -> 18* g_0(2, 23) -> 19* g_0(2, 18) -> 19* g_0(2, 17) -> 18* g_0(2, 6) -> 27*} Strict: {} Qed SCC: Strict: {g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} BOUND: Bound: match(-raise)-bounded by 1 Automaton: { j_0() -> 2* b_1() -> 41* | 37 | 17 b_0() -> 17* a_1() -> 42* | 35 | 5 a_0() -> 5* f_1(40) -> 49* | 34 | 4 f_1(33) -> 34* f_1(2) -> 40* | 33 | 3 f_0(40) -> 4* f_0(25) -> 4* f_0(3) -> 4* f_0(2) -> 3* c_1() -> 43* | 30 | 12 c_0() -> 12* d_1() -> 44* | 28 | 9 d_0() -> 9* e_1() -> 45* | 27 | 8 e_0() -> 8* g#_1(42, 51) -> 20* g#_1(42, 39) -> 20* g#_1(35, 51) -> 20* g#_1(35, 39) -> 20* g#_0(42, 51) -> 20* g#_0(42, 19) -> 20* g#_0(5, 51) -> 20* g#_0(5, 19) -> 20* g_1(52, 52) -> 4* g_1(52, 36) -> 4* g_1(49, 42) -> 52* | 36 | 6 g_1(49, 35) -> 36* g_1(45, 46) -> 19* g_1(45, 41) -> 48* | 32 | 18 g_1(45, 29) -> 19* g_1(45, 17) -> 48* | 32 | 18 g_1(44, 50) -> 19* g_1(44, 41) -> 46* | 29 | 21 g_1(44, 31) -> 19* g_1(44, 17) -> 46* | 29 | 21 g_1(43, 48) -> 19* g_1(43, 41) -> 50* | 31 | 18 g_1(43, 32) -> 19* g_1(43, 17) -> 50* | 31 | 18 g_1(42, 51) -> 22* g_1(42, 47) -> 51* | 39 | 19 g_1(42, 39) -> 22* g_1(42, 38) -> 39* g_1(41, 41) -> 47* | 38 | 18 g_1(41, 37) -> 38* g_1(35, 51) -> 22* g_1(35, 39) -> 22* g_1(34, 42) -> 36* g_1(34, 35) -> 36* g_1(30, 48) -> 19* g_1(30, 41) -> 31* g_1(30, 32) -> 19* g_1(30, 17) -> 31* g_1(28, 50) -> 19* g_1(28, 41) -> 29* g_1(28, 31) -> 19* g_1(28, 17) -> 29* g_1(27, 46) -> 19* g_1(27, 41) -> 32* g_1(27, 29) -> 19* g_1(27, 17) -> 32* g_1(17, 41) -> 47* | 38 | 18 g_1(17, 37) -> 38* g_1(6, 52) -> 4* g_1(6, 36) -> 4* g_1(5, 47) -> 51* | 39 | 19 g_1(5, 38) -> 39* g_0(52, 52) -> 4* g_0(52, 6) -> 4* g_0(51, 50) -> 19* g_0(51, 48) -> 19* g_0(51, 47) -> 19* g_0(51, 46) -> 19* g_0(51, 41) -> 21* g_0(51, 21) -> 19* g_0(51, 18) -> 19* g_0(51, 17) -> 21* g_0(50, 50) -> 19* g_0(50, 48) -> 19* g_0(50, 47) -> 19* g_0(50, 46) -> 19* g_0(50, 41) -> 21* g_0(50, 21) -> 19* g_0(50, 18) -> 19* g_0(50, 17) -> 21* g_0(49, 42) -> 6* g_0(49, 5) -> 6* g_0(48, 50) -> 19* g_0(48, 48) -> 19* g_0(48, 47) -> 19* g_0(48, 46) -> 19* g_0(48, 41) -> 21* g_0(48, 21) -> 19* g_0(48, 18) -> 19* g_0(48, 17) -> 21* g_0(47, 50) -> 19* g_0(47, 48) -> 19* g_0(47, 47) -> 19* g_0(47, 46) -> 19* g_0(47, 41) -> 21* g_0(47, 21) -> 19* g_0(47, 18) -> 19* g_0(47, 17) -> 21* g_0(46, 50) -> 19* g_0(46, 48) -> 19* g_0(46, 47) -> 19* g_0(46, 46) -> 19* g_0(46, 41) -> 21* g_0(46, 21) -> 19* g_0(46, 18) -> 19* g_0(46, 17) -> 21* g_0(45, 50) -> 19* g_0(45, 48) -> 19* g_0(45, 47) -> 19* g_0(45, 46) -> 19* g_0(45, 41) -> 18* g_0(45, 26) -> 23* g_0(45, 22) -> 23* g_0(45, 21) -> 19* g_0(45, 18) -> 19* g_0(45, 17) -> 18* g_0(45, 10) -> 23* g_0(45, 2) -> 15* g_0(44, 50) -> 19* g_0(44, 48) -> 19* g_0(44, 47) -> 19* g_0(44, 46) -> 19* g_0(44, 41) -> 21* g_0(44, 23) -> 24* g_0(44, 22) -> 24* g_0(44, 21) -> 19* g_0(44, 18) -> 19* g_0(44, 17) -> 21* g_0(44, 13) -> 24* g_0(44, 2) -> 10* g_0(43, 50) -> 19* g_0(43, 48) -> 19* g_0(43, 47) -> 19* g_0(43, 46) -> 19* g_0(43, 41) -> 18* g_0(43, 24) -> 26* g_0(43, 22) -> 26* g_0(43, 21) -> 19* g_0(43, 18) -> 19* g_0(43, 17) -> 18* g_0(43, 15) -> 26* g_0(43, 2) -> 13* g_0(42, 51) -> 22* g_0(42, 50) -> 19* g_0(42, 48) -> 19* g_0(42, 47) -> 19* g_0(42, 46) -> 19* g_0(42, 41) -> 18* g_0(42, 21) -> 19* g_0(42, 19) -> 22* g_0(42, 18) -> 19* g_0(42, 17) -> 18* g_0(41, 50) -> 19* g_0(41, 48) -> 19* g_0(41, 47) -> 19* g_0(41, 46) -> 19* g_0(41, 41) -> 18* g_0(41, 21) -> 19* g_0(41, 18) -> 19* g_0(41, 17) -> 18* g_0(26, 50) -> 19* g_0(26, 48) -> 19* g_0(26, 47) -> 19* g_0(26, 46) -> 19* g_0(26, 41) -> 21* g_0(26, 21) -> 19* g_0(26, 18) -> 19* g_0(26, 17) -> 21* g_0(24, 50) -> 19* g_0(24, 48) -> 19* g_0(24, 47) -> 19* g_0(24, 46) -> 19* g_0(24, 41) -> 21* g_0(24, 21) -> 19* g_0(24, 18) -> 19* g_0(24, 17) -> 21* g_0(23, 50) -> 19* g_0(23, 48) -> 19* g_0(23, 47) -> 19* g_0(23, 46) -> 19* g_0(23, 41) -> 21* g_0(23, 21) -> 19* g_0(23, 18) -> 19* g_0(23, 17) -> 21* g_0(22, 50) -> 19* g_0(22, 48) -> 19* g_0(22, 47) -> 19* g_0(22, 46) -> 19* g_0(22, 41) -> 21* g_0(22, 21) -> 19* g_0(22, 18) -> 19* g_0(22, 17) -> 21* g_0(21, 50) -> 19* g_0(21, 48) -> 19* g_0(21, 47) -> 19* g_0(21, 46) -> 19* g_0(21, 41) -> 21* g_0(21, 21) -> 19* g_0(21, 18) -> 19* g_0(21, 17) -> 21* g_0(19, 50) -> 19* g_0(19, 48) -> 19* g_0(19, 47) -> 19* g_0(19, 46) -> 19* g_0(19, 41) -> 21* g_0(19, 21) -> 19* g_0(19, 18) -> 19* g_0(19, 17) -> 21* g_0(18, 50) -> 19* g_0(18, 48) -> 19* g_0(18, 47) -> 19* g_0(18, 46) -> 19* g_0(18, 41) -> 21* g_0(18, 21) -> 19* g_0(18, 18) -> 19* g_0(18, 17) -> 21* g_0(17, 50) -> 19* g_0(17, 48) -> 19* g_0(17, 47) -> 19* g_0(17, 46) -> 19* g_0(17, 41) -> 18* g_0(17, 21) -> 19* g_0(17, 18) -> 19* g_0(17, 17) -> 18* g_0(15, 50) -> 19* g_0(15, 48) -> 19* g_0(15, 47) -> 19* g_0(15, 46) -> 19* g_0(15, 41) -> 21* g_0(15, 21) -> 19* g_0(15, 18) -> 19* g_0(15, 17) -> 21* g_0(13, 50) -> 19* g_0(13, 48) -> 19* g_0(13, 47) -> 19* g_0(13, 46) -> 19* g_0(13, 41) -> 21* g_0(13, 21) -> 19* g_0(13, 18) -> 19* g_0(13, 17) -> 21* g_0(12, 50) -> 19* g_0(12, 48) -> 19* g_0(12, 47) -> 19* g_0(12, 46) -> 19* g_0(12, 41) -> 18* g_0(12, 24) -> 26* g_0(12, 22) -> 26* g_0(12, 21) -> 19* g_0(12, 18) -> 19* g_0(12, 17) -> 18* g_0(12, 15) -> 26* g_0(12, 2) -> 13* g_0(10, 50) -> 19* g_0(10, 48) -> 19* g_0(10, 47) -> 19* g_0(10, 46) -> 19* g_0(10, 41) -> 21* g_0(10, 21) -> 19* g_0(10, 18) -> 19* g_0(10, 17) -> 21* g_0(9, 50) -> 19* g_0(9, 48) -> 19* g_0(9, 47) -> 19* g_0(9, 46) -> 19* g_0(9, 41) -> 21* g_0(9, 23) -> 24* g_0(9, 22) -> 24* g_0(9, 21) -> 19* g_0(9, 18) -> 19* g_0(9, 17) -> 21* g_0(9, 13) -> 24* g_0(9, 2) -> 10* g_0(8, 50) -> 19* g_0(8, 48) -> 19* g_0(8, 47) -> 19* g_0(8, 46) -> 19* g_0(8, 41) -> 18* g_0(8, 26) -> 23* g_0(8, 22) -> 23* g_0(8, 21) -> 19* g_0(8, 18) -> 19* g_0(8, 17) -> 18* g_0(8, 10) -> 23* g_0(8, 2) -> 15* g_0(6, 52) -> 4* g_0(6, 6) -> 4* g_0(5, 51) -> 22* g_0(5, 50) -> 19* g_0(5, 48) -> 19* g_0(5, 47) -> 19* g_0(5, 46) -> 19* g_0(5, 41) -> 18* g_0(5, 21) -> 19* g_0(5, 19) -> 22* g_0(5, 18) -> 19* g_0(5, 17) -> 18* g_0(4, 42) -> 6* g_0(4, 5) -> 6* g_0(2, 52) -> 25* g_0(2, 50) -> 19* g_0(2, 48) -> 19* g_0(2, 47) -> 19* g_0(2, 46) -> 19* g_0(2, 41) -> 18* g_0(2, 21) -> 19* g_0(2, 18) -> 19* g_0(2, 17) -> 18* g_0(2, 6) -> 25*} Strict: {} Qed