MAYBE
Problem:
f(x,a(b(c(y)))) -> f(b(c(a(b(x)))),y)
f(a(x),y) -> f(x,a(y))
f(b(x),y) -> f(x,b(y))
f(c(x),y) -> f(x,c(y))
Proof:
Complexity Transformation Processor:
strict:
f(x,a(b(c(y)))) -> f(b(c(a(b(x)))),y)
f(a(x),y) -> f(x,a(y))
f(b(x),y) -> f(x,b(y))
f(c(x),y) -> f(x,c(y))
weak:
Bounds Processor:
bound: 3
enrichment: match
automaton:
final states: {4}
transitions:
f3(30,66) -> 4*
f3(31,59) -> 4*
f3(21,59) -> 4*
f3(1,59) -> 4*
f3(28,55) -> 4*
f3(3,59) -> 4*
f3(22,59) -> 4*
f3(2,59) -> 4*
f3(29,51) -> 4*
f1(3,11) -> 4*
f1(22,1) -> 4*
f1(22,3) -> 4*
f1(22,11) -> 4*
f1(2,11) -> 4*
f1(21,11) -> 4*
f1(1,11) -> 4*
f1(21,19) -> 4*
f1(22,2) -> 4*
b3(55) -> 59*
b3(59) -> 66*
b1(22) -> 19*
b1(2) -> 19*
b1(59) -> 11*
b1(21) -> 22*
b1(11) -> 11*
b1(1) -> 19*
b1(53) -> 11*
b1(3) -> 19*
c3(49) -> 51*
c3(66) -> 51*
c3(58) -> 51*
c3(28) -> 51*
c1(20) -> 21*
c1(2) -> 11*
c1(59) -> 11*
c1(11) -> 11*
c1(1) -> 11*
c1(53) -> 11*
c1(3) -> 11*
a3(51) -> 55*
a1(59) -> 11*
a1(19) -> 20*
a1(11) -> 11*
a1(53) -> 11*
f2(30,58) -> 4*
f2(31,53) -> 4*
f2(1,53) -> 4*
f2(3,53) -> 4*
f2(31,2) -> 4*
f2(19,46) -> 4*
f2(20,27) -> 4*
f2(30,49) -> 4*
f2(21,58) -> 4*
f2(22,53) -> 4*
f2(2,53) -> 4*
f2(31,1) -> 4*
f2(31,3) -> 4*
f2(30,28) -> 4*
f2(31,11) -> 4*
f0(3,1) -> 4*
f0(3,3) -> 4*
f0(1,2) -> 4*
f0(2,1) -> 4*
f0(2,3) -> 4*
f0(3,2) -> 4*
f0(1,1) -> 4*
f0(1,3) -> 4*
f0(2,2) -> 4*
b2(30) -> 31*
b2(22) -> 28*
b2(2) -> 28*
b2(59) -> 58*
b2(46) -> 53*
b2(31) -> 28*
b2(21) -> 28*
b2(11) -> 49*
b2(1) -> 28*
b2(53) -> 58*
b2(3) -> 28*
a0(2) -> 1*
a0(1) -> 1*
a0(3) -> 1*
c2(59) -> 27*
c2(29) -> 30*
c2(19) -> 27*
c2(11) -> 27*
c2(58) -> 27*
b0(2) -> 2*
b0(1) -> 2*
b0(3) -> 2*
a2(27) -> 46*
a2(28) -> 29*
c0(2) -> 3*
c0(1) -> 3*
c0(3) -> 3*
problem:
strict:
f(x,a(b(c(y)))) -> f(b(c(a(b(x)))),y)
f(a(x),y) -> f(x,a(y))
f(b(x),y) -> f(x,b(y))
weak:
f(c(x),y) -> f(x,c(y))
Bounds Processor:
bound: 3
enrichment: match
automaton:
final states: {4}
transitions:
f3(55,68) -> 4*
f3(57,36) -> 4*
f3(56,63) -> 4*
f3(6,63) -> 4*
f3(1,63) -> 4*
f3(26,69) -> 4*
f3(27,68) -> 4*
f3(28,63) -> 4*
f3(8,63) -> 4*
f3(3,63) -> 4*
f3(54,62) -> 4*
f3(55,61) -> 4*
f3(5,63) -> 4*
f3(56,60) -> 4*
f3(57,41) -> 4*
f3(57,63) -> 4*
f3(7,63) -> 4*
f3(2,63) -> 4*
f3(29,63) -> 4*
f3(54,69) -> 4*
f3(29,69) -> 4*
f1(1,39) -> 4*
f1(8,1) -> 4*
f1(8,3) -> 4*
f1(2,36) -> 4*
f1(8,21) -> 4*
f1(2,40) -> 4*
f1(3,21) -> 4*
f1(3,39) -> 4*
f1(5,21) -> 4*
f1(7,5) -> 4*
f1(1,36) -> 4*
f1(7,21) -> 4*
f1(1,40) -> 4*
f1(8,2) -> 4*
f1(2,21) -> 4*
f1(2,39) -> 4*
f1(3,36) -> 4*
f1(3,40) -> 4*
f1(5,20) -> 4*
f1(6,19) -> 4*
f1(6,21) -> 4*
f1(1,21) -> 4*
b3(5) -> 54*
b3(62) -> 63*
b3(57) -> 54*
b3(7) -> 54*
b3(2) -> 54*
b3(69) -> 63*
b3(29) -> 54*
b3(56) -> 57*
b3(41) -> 60*
b3(36) -> 60*
b3(6) -> 54*
b3(1) -> 54*
b3(63) -> 63*
b3(28) -> 54*
b3(8) -> 54*
b3(3) -> 54*
b1(20) -> 21*
b1(7) -> 8*
b1(2) -> 5*
b1(39) -> 21*
b1(36) -> 21*
b1(21) -> 21*
b1(1) -> 5*
b1(8) -> 5*
b1(3) -> 5*
c3(60) -> 61*
c3(55) -> 56*
c3(63) -> 68*
c1(40) -> 21*
c1(5) -> 19*
c1(39) -> 21*
c1(21) -> 21*
c1(6) -> 7*
a3(54) -> 55*
a3(61) -> 62*
a3(68) -> 69*
a1(40) -> 21*
a1(5) -> 6*
a1(19) -> 20*
a1(41) -> 21*
a1(36) -> 21*
a1(21) -> 21*
a1(63) -> 21*
f2(26,41) -> 4*
f2(6,39) -> 4*
f2(6,41) -> 4*
f2(1,41) -> 4*
f2(7,36) -> 4*
f2(2,36) -> 4*
f2(28,41) -> 4*
f2(8,41) -> 4*
f2(3,41) -> 4*
f2(29,36) -> 4*
f2(29,40) -> 4*
f2(5,41) -> 4*
f2(6,36) -> 4*
f2(26,40) -> 4*
f2(1,36) -> 4*
f2(27,39) -> 4*
f2(27,41) -> 4*
f2(7,41) -> 4*
f2(2,41) -> 4*
f2(28,36) -> 4*
f2(8,36) -> 4*
f2(29,21) -> 4*
f2(3,36) -> 4*
f2(29,39) -> 4*
f2(29,41) -> 4*
f2(5,36) -> 4*
f2(5,40) -> 4*
f0(3,1) -> 4*
f0(3,3) -> 4*
f0(1,2) -> 4*
f0(2,1) -> 4*
f0(2,3) -> 4*
f0(3,2) -> 4*
f0(1,1) -> 4*
f0(1,3) -> 4*
f0(2,2) -> 4*
b2(40) -> 41*
b2(5) -> 26*
b2(57) -> 26*
b2(7) -> 26*
b2(2) -> 26*
b2(39) -> 36*
b2(29) -> 26*
b2(41) -> 36*
b2(36) -> 36*
b2(21) -> 36*
b2(6) -> 26*
b2(1) -> 26*
b2(28) -> 29*
b2(8) -> 26*
b2(3) -> 26*
a0(2) -> 1*
a0(1) -> 1*
a0(3) -> 1*
c2(27) -> 28*
c2(41) -> 41*
c2(36) -> 39*
c2(63) -> 36*
b0(2) -> 2*
b0(1) -> 2*
b0(3) -> 2*
a2(39) -> 40*
a2(29) -> 27*
a2(41) -> 41*
a2(36) -> 36*
a2(26) -> 27*
a2(63) -> 36*
c0(2) -> 3*
c0(1) -> 3*
c0(3) -> 3*
problem:
strict:
f(a(x),y) -> f(x,a(y))
f(b(x),y) -> f(x,b(y))
weak:
f(x,a(b(c(y)))) -> f(b(c(a(b(x)))),y)
f(c(x),y) -> f(x,c(y))
Bounds Processor:
bound: 4
enrichment: match
automaton:
final states: {4}
transitions:
b3(27) -> 33*
b3(17) -> 29*
b3(12) -> 29*
b3(9) -> 29*
b3(31) -> 32*
b3(26) -> 27*
b3(16) -> 34*
b3(43) -> 27*
c3(30) -> 31*
c3(34) -> 41*
c3(33) -> 35*
a3(35) -> 26*
a3(25) -> 26*
a3(29) -> 30*
a3(16) -> 26*
f4(29,42) -> 4*
f4(17,43) -> 4*
f4(12,43) -> 4*
f4(9,43) -> 4*
a4(35) -> 42*
a4(41) -> 42*
f0(3,1) -> 4*
f0(3,3) -> 4*
f0(1,2) -> 4*
f0(2,1) -> 4*
f0(2,3) -> 4*
f0(3,2) -> 4*
f0(1,1) -> 4*
f0(1,3) -> 4*
f0(2,2) -> 4*
a0(2) -> 1*
a0(1) -> 1*
a0(3) -> 1*
b0(2) -> 2*
b0(1) -> 2*
b0(3) -> 2*
b4(42) -> 43*
c0(2) -> 3*
c0(1) -> 3*
c0(3) -> 3*
f1(3,5) -> 4*
f1(10,5) -> 4*
f1(12,1) -> 4*
f1(12,3) -> 4*
f1(12,5) -> 4*
f1(2,5) -> 4*
f1(10,14) -> 4*
f1(11,5) -> 4*
f1(1,5) -> 4*
f1(11,9) -> 4*
f1(12,2) -> 4*
b1(20) -> 9*
b1(10) -> 9*
b1(5) -> 5*
b1(12) -> 9*
b1(2) -> 9*
b1(16) -> 5*
b1(11) -> 12*
b1(1) -> 9*
b1(3) -> 9*
c1(10) -> 11*
c1(5) -> 5*
c1(9) -> 14*
c1(16) -> 5*
a1(5) -> 5*
a1(27) -> 5*
a1(12) -> 10*
a1(2) -> 5*
a1(9) -> 10*
a1(16) -> 5*
a1(1) -> 5*
a1(3) -> 5*
f2(12,16) -> 4*
f2(2,16) -> 4*
f2(18,25) -> 4*
f2(19,16) -> 4*
f2(20,5) -> 4*
f2(11,16) -> 4*
f2(1,16) -> 4*
f2(12,15) -> 4*
f2(18,16) -> 4*
f2(3,16) -> 4*
f2(9,15) -> 4*
f2(19,23) -> 4*
f2(20,16) -> 4*
f2(10,16) -> 4*
b2(20) -> 17*
b2(15) -> 16*
b2(10) -> 17*
b2(5) -> 23*
b2(27) -> 16*
b2(12) -> 17*
b2(2) -> 17*
b2(19) -> 20*
b2(9) -> 17*
b2(16) -> 16*
b2(11) -> 17*
b2(1) -> 17*
b2(43) -> 16*
b2(3) -> 17*
c2(27) -> 16*
c2(16) -> 16*
c2(23) -> 25*
c2(18) -> 19*
a2(5) -> 15*
a2(27) -> 15*
a2(17) -> 18*
a2(14) -> 15*
a2(16) -> 15*
f3(32,16) -> 4*
f3(17,26) -> 4*
f3(3,27) -> 4*
f3(18,35) -> 4*
f3(20,27) -> 4*
f3(10,27) -> 4*
f3(30,35) -> 4*
f3(30,41) -> 4*
f3(31,34) -> 4*
f3(32,27) -> 4*
f3(12,27) -> 4*
f3(2,27) -> 4*
f3(9,27) -> 4*
f3(19,33) -> 4*
f3(11,27) -> 4*
f3(31,33) -> 4*
f3(1,27) -> 4*
problem:
strict:
f(b(x),y) -> f(x,b(y))
weak:
f(a(x),y) -> f(x,a(y))
f(x,a(b(c(y)))) -> f(b(c(a(b(x)))),y)
f(c(x),y) -> f(x,c(y))
Open