MAYBE
Problem:
r1(a(x1)) -> a(a(a(r1(x1))))
r2(a(x1)) -> a(a(a(r2(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
r1(b(x1)) -> l1(b(x1))
r2(b(x1)) -> l2(a(b(x1)))
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
a(a(x1)) -> x1
Proof:
Complexity Transformation Processor:
strict:
r1(a(x1)) -> a(a(a(r1(x1))))
r2(a(x1)) -> a(a(a(r2(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
r1(b(x1)) -> l1(b(x1))
r2(b(x1)) -> l2(a(b(x1)))
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
a(a(x1)) -> x1
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[b](x0) = x0,
[l2](x0) = x0 + 1,
[l1](x0) = x0,
[r2](x0) = x0,
[r1](x0) = x0,
[a](x0) = x0
orientation:
r1(a(x1)) = x1 >= x1 = a(a(a(r1(x1))))
r2(a(x1)) = x1 >= x1 = a(a(a(r2(x1))))
a(l1(x1)) = x1 >= x1 = l1(a(a(a(x1))))
a(a(l2(x1))) = x1 + 1 >= x1 + 1 = l2(a(a(x1)))
r1(b(x1)) = x1 >= x1 = l1(b(x1))
r2(b(x1)) = x1 >= x1 + 1 = l2(a(b(x1)))
b(l1(x1)) = x1 >= x1 = b(r2(x1))
b(l2(x1)) = x1 + 1 >= x1 = b(r1(x1))
a(a(x1)) = x1 >= x1 = x1
problem:
strict:
r1(a(x1)) -> a(a(a(r1(x1))))
r2(a(x1)) -> a(a(a(r2(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
r1(b(x1)) -> l1(b(x1))
r2(b(x1)) -> l2(a(b(x1)))
b(l1(x1)) -> b(r2(x1))
a(a(x1)) -> x1
weak:
b(l2(x1)) -> b(r1(x1))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[b](x0) = x0,
[l2](x0) = x0,
[l1](x0) = x0 + 1,
[r2](x0) = x0,
[r1](x0) = x0,
[a](x0) = x0
orientation:
r1(a(x1)) = x1 >= x1 = a(a(a(r1(x1))))
r2(a(x1)) = x1 >= x1 = a(a(a(r2(x1))))
a(l1(x1)) = x1 + 1 >= x1 + 1 = l1(a(a(a(x1))))
a(a(l2(x1))) = x1 >= x1 = l2(a(a(x1)))
r1(b(x1)) = x1 >= x1 + 1 = l1(b(x1))
r2(b(x1)) = x1 >= x1 = l2(a(b(x1)))
b(l1(x1)) = x1 + 1 >= x1 = b(r2(x1))
a(a(x1)) = x1 >= x1 = x1
b(l2(x1)) = x1 >= x1 = b(r1(x1))
problem:
strict:
r1(a(x1)) -> a(a(a(r1(x1))))
r2(a(x1)) -> a(a(a(r2(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
r1(b(x1)) -> l1(b(x1))
r2(b(x1)) -> l2(a(b(x1)))
a(a(x1)) -> x1
weak:
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[b](x0) = x0,
[l2](x0) = x0,
[l1](x0) = x0,
[r2](x0) = x0,
[r1](x0) = x0,
[a](x0) = x0 + 1
orientation:
r1(a(x1)) = x1 + 1 >= x1 + 3 = a(a(a(r1(x1))))
r2(a(x1)) = x1 + 1 >= x1 + 3 = a(a(a(r2(x1))))
a(l1(x1)) = x1 + 1 >= x1 + 3 = l1(a(a(a(x1))))
a(a(l2(x1))) = x1 + 2 >= x1 + 2 = l2(a(a(x1)))
r1(b(x1)) = x1 >= x1 = l1(b(x1))
r2(b(x1)) = x1 >= x1 + 1 = l2(a(b(x1)))
a(a(x1)) = x1 + 2 >= x1 = x1
b(l1(x1)) = x1 >= x1 = b(r2(x1))
b(l2(x1)) = x1 >= x1 = b(r1(x1))
problem:
strict:
r1(a(x1)) -> a(a(a(r1(x1))))
r2(a(x1)) -> a(a(a(r2(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
r1(b(x1)) -> l1(b(x1))
r2(b(x1)) -> l2(a(b(x1)))
weak:
a(a(x1)) -> x1
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[b](x0) = x0,
[l2](x0) = x0,
[l1](x0) = x0 + 1,
[r2](x0) = x0 + 1,
[r1](x0) = x0,
[a](x0) = x0
orientation:
r1(a(x1)) = x1 >= x1 = a(a(a(r1(x1))))
r2(a(x1)) = x1 + 1 >= x1 + 1 = a(a(a(r2(x1))))
a(l1(x1)) = x1 + 1 >= x1 + 1 = l1(a(a(a(x1))))
a(a(l2(x1))) = x1 >= x1 = l2(a(a(x1)))
r1(b(x1)) = x1 >= x1 + 1 = l1(b(x1))
r2(b(x1)) = x1 + 1 >= x1 = l2(a(b(x1)))
a(a(x1)) = x1 >= x1 = x1
b(l1(x1)) = x1 + 1 >= x1 + 1 = b(r2(x1))
b(l2(x1)) = x1 >= x1 = b(r1(x1))
problem:
strict:
r1(a(x1)) -> a(a(a(r1(x1))))
r2(a(x1)) -> a(a(a(r2(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
r1(b(x1)) -> l1(b(x1))
weak:
r2(b(x1)) -> l2(a(b(x1)))
a(a(x1)) -> x1
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
r10(2) -> 3*
r10(1) -> 3*
a0(50) -> 51*
a0(25) -> 26*
a0(2) -> 5*
a0(144) -> 145*
a0(49) -> 50*
a0(24) -> 25*
a0(1) -> 5*
a0(118) -> 119*
a0(48) -> 49*
r20(2) -> 4*
r20(1) -> 4*
l10(2) -> 1*
l10(51) -> 52*
l10(26) -> 27*
l10(1) -> 1*
l20(2) -> 2*
l20(79) -> 80*
l20(1) -> 2*
b0(2) -> 6*
b0(46) -> 47*
b0(1) -> 6*
b0(28) -> 29*
1 -> 25*
2 -> 25*
3 -> 46*
4 -> 28*
5 -> 24*
24 -> 145,26
25 -> 49,79
26 -> 48*
27 -> 145,119,5
29 -> 6*
47 -> 6*
48 -> 50*
49 -> 51*
50 -> 119*
51 -> 118*
52 -> 49,25
79 -> 144*
80 -> 49,25
118 -> 25,49
119 -> 24*
144 -> 25,49
145 -> 24*
problem:
strict:
r1(a(x1)) -> a(a(a(r1(x1))))
r2(a(x1)) -> a(a(a(r2(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
weak:
r1(b(x1)) -> l1(b(x1))
r2(b(x1)) -> l2(a(b(x1)))
a(a(x1)) -> x1
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
r10(2) -> 3*
r10(1) -> 3*
a0(50) -> 51*
a0(132) -> 133*
a0(92) -> 93*
a0(52) -> 53*
a0(7) -> 8*
a0(2) -> 5*
a0(51) -> 52*
a0(1) -> 5*
a0(8) -> 9*
r20(2) -> 4*
r20(1) -> 4*
l10(2) -> 1*
l10(9) -> 10*
l10(1) -> 1*
l10(53) -> 54*
l20(55) -> 56*
l20(2) -> 2*
l20(1) -> 2*
b0(32) -> 33*
b0(2) -> 6*
b0(34) -> 35*
b0(1) -> 6*
1 -> 51,8
2 -> 51,8
3 -> 34*
4 -> 32*
5 -> 7*
7 -> 133,9
8 -> 51,55
9 -> 50*
10 -> 93,133,5
33 -> 6*
35 -> 6*
50 -> 93,52
51 -> 53*
52 -> 93*
53 -> 92*
54 -> 51,8
55 -> 132*
56 -> 51,8
92 -> 8,53
93 -> 7*
132 -> 8,53
133 -> 7*
problem:
strict:
r2(a(x1)) -> a(a(a(r2(x1))))
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
weak:
r1(a(x1)) -> a(a(a(r1(x1))))
r1(b(x1)) -> l1(b(x1))
r2(b(x1)) -> l2(a(b(x1)))
a(a(x1)) -> x1
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {6,5,4,3}
transitions:
r10(2) -> 5*
r10(1) -> 5*
a0(77) -> 78*
a0(37) -> 38*
a0(7) -> 8*
a0(2) -> 4*
a0(39) -> 40*
a0(111) -> 112*
a0(1) -> 4*
a0(38) -> 39*
a0(8) -> 9*
r20(2) -> 3*
r20(1) -> 3*
l10(40) -> 41*
l10(2) -> 1*
l10(9) -> 10*
l10(1) -> 1*
l20(42) -> 43*
l20(2) -> 2*
l20(1) -> 2*
b0(2) -> 6*
b0(26) -> 27*
b0(1) -> 6*
b0(28) -> 29*
1 -> 38,8
2 -> 38,8
3 -> 26*
4 -> 7*
5 -> 28*
7 -> 112,9
8 -> 38,42
9 -> 37*
10 -> 78,112,4
27 -> 6*
29 -> 6*
37 -> 78,39
38 -> 40*
39 -> 78*
40 -> 77*
41 -> 38,8
42 -> 111*
43 -> 38,8
77 -> 8,38
78 -> 7*
111 -> 38*
112 -> 7*
problem:
strict:
a(l1(x1)) -> l1(a(a(a(x1))))
a(a(l2(x1))) -> l2(a(a(x1)))
weak:
r2(a(x1)) -> a(a(a(r2(x1))))
r1(a(x1)) -> a(a(a(r1(x1))))
r1(b(x1)) -> l1(b(x1))
r2(b(x1)) -> l2(a(b(x1)))
a(a(x1)) -> x1
b(l1(x1)) -> b(r2(x1))
b(l2(x1)) -> b(r1(x1))
Open