User:Polygon/Page for analyses

A page for analyses of individual machines.

1RB1RD1LC_2LB1RB1LC_1RZ1LA1LD_2RB2RA2RD (bbch)

1. One of the seven potential BB(4,3) champions discovered by Pavel Kropitz in May 2024. Analysed in September 2025. This TM runs the shortest of Pavel's potential champions, achieving a score of about $10\uparrow \uparrow 9.873987$.

Analysis

	0	1	2
A	1RB	1RD	1LC
B	2LB	1RB	1LC
C	1RZ	1LA	1LD
D	2RB	2RA	2RD

S is any tape configuration
1. S D> 2^a S --> S 2^a D> S [+a steps]
2. S B> 1^a S --> S 1^a B> S [+a steps]
3. S 1 B> 0 S --> S <A 1^2 S [+4 steps]
4. S D> (11)^a S --> S (21)^a D> S [+2a steps]
   S A> (11)^a S --> S (12)^a A> S [+2a steps]
5. S (21)^a <C S --> S <C (11)^a S [+2a steps]
   S (12)^a <A S --> S <A (11)^a S [+2a steps]
6. S (12)^a A> 0^2 S --> S <A (11)^a+1 S [+2a +5 steps]

7. S (12)^a 2 (12)^b A> 0^2 S --> S (12)^a-1 2 (12)^b+2 A> S [+4b +7 steps]
by:
S (12)^a 2 (12)^b A> 0^2 S
--> S (12)^a 2 <A (11)^b+1 S
--> S (12)^a <C 1 (11)^b+1 S
--> S (12)^a-1 1 <D (11)^b+2 S
--> S (12)^a-1 2 A> (11)^b+2 S
--> S (12)^a-1 2 (12)^b+2 A> S

8. S (12)^a 2 (12)^b A> 0^inf --> S 2 (12)^b+2a A> 0^inf [+4a^2 +8a +4ba steps]
Obtained by repeating rule 7.

9. S (12)^a <D (11)^b 0^inf --> S (12)^a-1 <D (11)^2b+3 0^inf [+4b^2 +22b +22 steps]
by:
S (12)^a <D (11)^b 0^inf
--> S (12)^a D> (11)^b 0^inf
--> S (12)^a (21)^b D> 0^inf
--> S (12)^a (21)^b 2 B> 0^inf
--> S (12)^a (21)^b 2 <B 2 0^inf
--> S (12)^a (21)^b <C 1 2 0^inf
--> S (12)^a <C (11)^b 1 2 0^inf
--> S (12)^a-1 1 <D (11)^b+1 2 0^inf
--> S (12)^a-1 2 A> (11)^b+1 2 0^inf
--> S (12)^a-1 2 (12)^b+1 A> 2 0^inf
--> S (12)^a-1 2 (12)^b+1 <C 1 0^inf
--> S (12)^a-1 2 (12)^b 1 <D 11 0^inf
--> S (12)^a-1 2 (12)^b 2 A> (11)^1 0^inf
--> S (12)^a-1 2 (12)^b 2 (12)^1 A> 0^inf
--> S (12)^a-1 2 2 (12)^2b+1 A> 0^inf
--> S (12)^a-1 2^2 <A (11)^2b+2 0^inf
--> S (12)^a-1 2 <C 1 (11)^2b+2 0^inf
--> S (12)^a-1 <D (11)^2b+3 0^inf

10. S (12)^a <D (11)^b 0^inf --> S <D (11)^((2^(a))*b+(2^(a))*3-3) 0^inf
Obtained by repeating rule 9.

11. S (11)^a <D (11)^b 0^inf --> S (11)^a-2 (12)^b+3 <D (11)^3 0^inf [+10b +50 steps]
by:
S (11)^a <D (11)^b 0^inf
--> S (11)^a-1 1 2 A> (11)^b 0^inf
--> S (11)^a-1 (12)^b+1 A> 0^inf
--> S (11)^a-1 <A (11)^b+2 0^inf
--> S (11)^a-1 D> (11)^b+2 0^inf
--> S (11)^a-1 (21)^b+2 D> 0^inf
--> S (11)^a-1 (21)^b+2 2 B> 0^inf
--> S (11)^a-1 (21)^b+2 2 <B 2 0^inf
--> S (11)^a-1 (21)^b+2 <C (12)^1 0^inf
--> S (11)^a-1 <C (11)^b+2 1 2 0^inf
--> S (11)^a-2 1 <A (11)^b+3 2 0^inf
--> S (11)^a-2 1 D> (11)^b+3 2 0^inf
--> S (11)^a-2 1 (21)^b+3 D> 2 0^inf
--> S (11)^a-2 1 (21)^b+3 2 D> 0^inf
--> S (11)^a-2 1 (21)^b+3 2^2 B> 0^inf
--> S (11)^a-2 1 (21)^b+3 2^2 <B 2 0^inf
--> S (11)^a-2 1 (21)^b+3 2 <C (12)^1 0^inf
--> S (11)^a-2 1 (21)^b+3 <D 1 1 2 0^inf
Note that 1 (21)^k = (12)^k 1
= S (11)^a-2 (12)^b+3 1 <D (11)^1 2 0^inf
--> S (11)^a-2 (12)^b+3 2 A> (11)^1 2 0^inf
--> S (11)^a-2 (12)^b+3 2 (12)^1 A> 2 0^inf
--> S (11)^a-2 (12)^b+3 2 (12)^1 <C 1 0^inf
--> S (11)^a-2 (12)^b+3 2 1<D (11)^1 0^inf
--> S (11)^a-2 (12)^b+3 2^2 A> (11)^1 0^inf
--> S (11)^a-2 (12)^b+3 2^2 (12)^1 A> 0^inf
--> S (11)^a-2 (12)^b+3 2^2 <A (11)^2 0^inf
--> S (11)^a-2 (12)^b+3 2 <C 1 (11)^2 0^inf
--> S (11)^a-2 (12)^b+3 <D (11)^3 0^inf

12. S 1^a <A (11)^b 0^inf --> 1^a-1 <A (11)^b+1 2 0^inf [+4b +5 steps]
by:
S 1^a <A (11)^b 0^inf
--> S 1^a D> (11)^b 0^inf
--> S 1^a (21)^b D> 0^inf
--> S 1^a (21)^b 2 B> 0^inf
--> S 1^a (21)^b 2 <B 2 0^inf
--> S 1^a (21)^b <C 1 2 0^inf
--> S 1^a <C (11)^b 1 2 0^inf
--> 1^a-1 <A (11)^b+1 2 0^inf

Functions

Let A(a,b,c) = S (11)^a (12)^b <D (11)^c 0^inf

• Rule 9: A(a, b, c) --> A(a, b - 1, 2c + 3)
• Rule 10: A(a, b, c) --> $A(a,0,2^b\times c+2^b\times 3-3)$ which becomes $A(a,0,2^{b+1}\times 3-3)$ if c = 3.
• Rule 11: A(a, 0, c) --> A(a - 2, c + 3, 3)

Further: let $f(n)=2^{n+1}\times 3$

• If c = 3: A(a, b, 3) --> A(a, 0, f(b) - 3) --> A(a - 2, f(b), 3)

• A(a, 0, c) --> $A(a-2,c+3,3)-->A(a-2,0,f(c+3)-3)$

• A(2k + d, b, 3) --> $A(d,f^k(b),3)$

Trajectory

S=0: 0^inf A> 0^inf
S=1: 0^inf 1 B> 0^inf
S=5: 0^inf <A (11)^1 0^inf
S=6: 0^inf 1 B> (11)^1 0^inf
S=8: 0^inf 1 (11)^1 B> 0^inf
S=9: 0^inf 1 (11)^1 <B 2 0^inf
S=10: 0^inf 1 (11)^1 B> 2 0^inf
S=11: 0^inf 1 (11)^1 <C 1 0^inf
S=12: 0^inf (11)^1 <A (11)^1 0^inf
S=21: 0^inf 1 <A (11)^2 2 0^inf by rule 12
S=22: 0^inf 1 D> (11)^2 2 0^inf
S=26: 0^inf 1 (21)^2 D> 2 0^inf
S=27: 0^inf 1 (21)^2 2 D> 0^inf
S=28: 0^inf 1 (21)^2 2^2 B> 0^inf
S=29: 0^inf 1 (21)^2 2^2 <B 2 0^inf
S=30: 0^inf 1 (21)^2 2 <C 1 2 0^inf
S=31: 0^inf 1 (21)^2 <D (11)^1 2 0^inf
S=32: 0^inf 1 (21)^1 2^2 A> (11)^1 2 0^inf
S=34: 0^inf 1 (21)^1 2^2 (12)^1 A> 2 0^inf
S=35: 0^inf 1 (21)^1 2^2 (12)^1 <C 1 0^inf
S=36: 0^inf 1 (21)^1 2^2 1 <D (11)^1 0^inf
S=37: 0^inf 1 (21)^1 2^3 A> (11)^1 0^inf
S=39: 0^inf (12)^2 2^2 (12)^1 A> 0^inf
S=46: 0^inf (12)^2 2^2 <A (11)^2 0^inf
S=47: 0^inf (12)^2 2 <C 1 (11)^2 0^inf
S=48: 0^inf (12)^2 <D (11)^3 0^inf
S=172: 0^inf (12)^1 <D (11)^9 0^inf by rule 9
S=716: 0^inf <D (11)^21 0^inf by rule 9
S=717: 0^inf 2 B> (11)^21 0^inf
S=759: 0^inf 2 (11)^21 B> 0^inf
S=760: 0^inf 2 (11)^21 <B 2 0^inf
S=761: 0^inf 2 (11)^21 B> 2 0^inf
S=762: 0^inf 2 (11)^21 <C 1 0^inf
S=763: 0^inf 2 (11)^20 1 <A (11)^1 0^inf
S=772: 0^inf 2 (11)^20 <A (11)^2 2 0^inf
S=773: 0^inf 2 (11)^20 D> (11)^2 2 0^inf
S=777: 0^inf 2 (11)^20 (21)^2 D> 2 0^inf
S=778: 0^inf 2 (11)^20 (21)^2 2 D> 0^inf
S=779: 0^inf 2 1 (11)^19 1 (21)^2 2^2 B> 0^inf
S=780: 0^inf 2 1 (11)^19 (12)^3 2 <B 2 0^inf
S=781: 0^inf 2 1 (11)^19 (12)^3 <C 1 2 0^inf
S=782: 0^inf 2 1 (11)^19 (12)^2 1 <D (11)^1 2 0^inf
S=783: 0^inf 2 1 (11)^19 (12)^2 2 A> (11)^1 2 0^inf
S=785: 0^inf 2 1 (11)^19 (12)^2 2 (12)^1 A> 2 0^inf
S=786: 0^inf 2 1 (11)^19 (12)^2 2 (12)^1 <C 1 0^inf
S=787: 0^inf 2 1 (11)^19 (12)^2 2 1 <D (11)^1 0^inf
S=788: 0^inf 2 1 (11)^19 (12)^2 2^2 A> (11)^1 0^inf
S=790: 0^inf 2 1 (11)^19 (12)^2 2^2 (12)^1 A> 0^inf
S=797: 0^inf 2 1 (11)^19 (12)^2 2^2 <A (11)^2 0^inf
S=798: 0^inf 2 1 (11)^19 (12)^2 2 <C 1 (11)^2 0^inf
S=799: 0^inf 2 1 (11)^19 (12)^2 <D (11)^3 0^inf
= A(19, 2, 3)

A(19, 2, 3) --> $A(1,f^9(2),3)-->A(1,0,f^{10}(2)-3)$

Let m = $f^{10}(2)-3$

--> 0^inf 2 1 (11)^1 <D (11)^m 0^inf

Final trajectory:
0^inf 2 1 (11)^1 <D (11)^m 0^inf
--> 0^inf 2 1 1 2 A> (11)^m 0^inf
--> 0^inf 2 1 (12)^m+1 A> 0^inf
--> 0^inf 2 1 <A (11)^m+2 0^inf
--> 0^inf 2 1 D> (11)^m+2 0^inf
--> 0^inf (21)^m+3 D> 0^inf
--> 0^inf (21)^m+3 2 B> 0^inf
--> 0^inf (21)^m+3 2 <B 2 0^inf
--> 0^inf (21)^m+3 <C (12)^1 0^inf
--> 0^inf <C (11)^m+3 (12)^1 0^inf
--> 0^inf 1 Z> (11)^m+3 (12)^1 0^inf
Score = 2m + 9

Approximate Score

Score calculated in HyperCalc:

(10^)^8 30,302,671.815163

Or in tetration: 10^^9.873987 (truncated)

1RB1RD1LC_2LB1RB1LC_1RZ1LA1LD_0RB2RA2RD (bbch)

2. One of the seven potential BB(4,3) champions discovered by Pavel Kropitz in May 2024.

Analysis

	0	1	2
A	1RB	1RD	1LC
B	2LB	1RB	1LC
C	1RZ	1LA	1LD
D	0RB	2RA	2RD

S is any tape configuration
1. S D> 2^a S --> S 2^a D> S [+a steps]
2. S B> 1^a S --> S 1^a B> S [+a steps]
3. S A> 0^2 S --> S <A 1^2 S [+5 steps]
4. S D> (11)^a S --> S (21)^a D> S [+2a steps]
   S A> (11)^a S --> S (12)^a A> S [+2a steps]
5. S (21)^a <C S --> S <C (11)^a S [+2a steps]
   S (12)^a <A S --> S <A (11)^a S [+2a steps]
6. S (12)^a A> 0^2 S --> S <A (11)^a+1 S [+2a +5 steps]
by:
S (12)^a A> 0^2 S
--> S (12)^a <A (11)^1 S
--> S <A (11)^a+1 S

7. S A> (11)^1 2^b S --> S 2 A> (11)^1 2^b-1 S [+5 steps]
by:
S A> (11)^1 2^b S
--> S (12)^1 A> 2^b S
--> S (12)^1 <C 1 2^b-1 S
--> S 1 <D (11)^1 2^b-1 S
--> S 2 A> (11)^1 2^b-1 S
8. S A> (11)^1 2^b S --> S 2^b A> (11)^1 S [+5b steps]
by repetition of rule 7

9. S D> 0^2 S --> S <B 2^2 S [+3 steps]

10. S 2 <D (11)^a 0^2 S --> S <D (11)^a+1 2 S [+4a +7 steps]
by:
S 2 <D (11)^a 0^2 S
--> S 2 D> (11)^a 0^2 S
--> S 2 (21)^a D> 0^2 S
--> S 2 (21)^a <B 2^2 S
--> S 2 (21)^a B> 2^2 S
--> S 2 (21)^a <C 1 2 S
--> S 2 <C (11)^a 1 2 S
--> S <D (11)^a+1 2 S

11. S 2 <D (11)^a 2 0^2 S --> S <D (11)^a+1 2^2 S [+4a +7 steps]
by:
S 2 <D (11)^a 2 0^2 S
--> S 2 D> (11)^a 2 0^2 S
--> S 2 (21)^a D> 2 0^2 S
--> S 2 (21)^a 2 D> 0^2 S
--> S 2 (21)^a 2 <B 2^2 S
--> S 2 (21)^a <C 1 2^2 S
--> S 2 <C (11)^a 1 2^2 S
--> S <D (11)^a+1 2^2 S

12. S  1^a <A (11)^b 0^2 S --> S 1^a-1 <A (11)^b+1 2 S [+4b +7 steps]
by:
S 1^a <A (11)^b 0^2 S
--> S 1^a D> (11)^b 0^2 S
--> S 1^a (21)^b D> 0^2 S
--> S 1^a (21)^b <B 2^2 S
--> S 1^a (21)^b B> 2^2 S
--> S 1^a (21)^b <C 1 2 S
--> S 1^a <C (11)^b 1 2 S
--> S 1^a-1 <A (11)^b+1 2 S

13. S 1^a <A (11)^b 2 0^2 S --> S 1^a-1 <A (11)^b+1 2^2 S [+4b +7 steps]
by:
S 1^a <A (11)^b 2 0^2 S
--> S 1^a D> (11)^b 2 0^2 S
--> S 1^a (21)^b D> 2 0^2 S
--> S 1^a (21)^b 2 D> 0^2 S
--> S 1^a (21)^b 2 <B 2^2 S
--> S 1^a (21)^b <C 1 2^2 S
--> S 1^a <C (11)^b 1 2^2 S
--> S 1^a-1 <A (11)^b+1 2^2 S

14. S (12)^a 1 <D (11)^b 0^2 S --> S (12)^a-1 1 <D (11)^b+2 [+4b +8 steps]
by:
S (12)^a 1 <D (11)^b 0^2 S
--> S (12)^a 2 A> (11)^b 0^2 S
--> S (12)^a 2 (12)^b A> 0^2 S
--> S (12)^a 2 <A (11)^b+1 S
--> S (12)^a <C 1 (11)^b+1 S
--> S (12)^a-1 1 <D (11)^b+2 S

15. S (12)^a 1 <D (11)^b 0^inf --> S 1 <D (11)^b+2a 0^inf [+4a^2 +4ba + 4a steps]
by repetition of rule 14

16. S (12)^a 2 1 <D (11)^b 0^inf --> S (12)^a-1 2 (12)^b+2 1 <D (11)^1 0^inf [+10b +28 steps]
by:
S (12)^a 2 1 <D (11)^b 0^inf
--> S (12)^a 2^2 A> (11)^b 0^inf
--> S (12)^a 2^2 (12)^b A> 0^inf
--> S (12)^a 2^2 <A (11)^b+1 0^inf
--> S (12)^a 2 <C 1 (11)^b+1 0^inf
--> S (12)^a <D (11)^b+2 0^inf
--> S (12)^a-1 1 <D (11)^b+3 2 0^inf by rule 10
--> S (12)^a-1 2 A> (11)^b+3 2 0^inf
--> S (12)^a-1 2 (12)^b+3 A> 2 0^inf
--> S (12)^a-1 2 (12)^b+3 <C 1 0^inf
--> S (12)^a-1 2 (12)^b+2 1 <D (11)^1 0^inf

17. S (12)^a 2 1 <D (11)^b 0^inf --> S (12)^a-1 2 1 <D (11)^2b+5 0^inf
by:
S (12)^a 2 1 <D (11)^b 0^inf
--> S (12)^a-1 2 (12)^b+2 1 <D (11)^1 0^inf by rule 16
--> S (12)^a-1 2 1 <D (11)^2b+5 0^inf by rule 15

18. S (12)^a 2 1 <D (11)^b 0^inf --> S 2 1 <D (11)^(2^a)*b+(2^a)*5-5 0^inf
by repetition of rule 17

---
19. S (12)^a 2 1 <D (11)^b 2 0^inf --> S (12)^a 2^2 1 <D (11)^2b-1 0^inf
by:
S (12)^a 2 1 <D (11)^b 2 0^inf
--> S (12)^a 2^2 A> (11)^b 2 0^inf
--> S (12)^a 2^2 (12)^b A> 2 0^inf
--> S (12)^a 2^2 (12)^b <C 1 0^inf
--> S (12)^a 2^2 (12)^b-1 1 <D (11)^1 0^inf
--> S (12)^a 2^2 1 <D (11)^2b-1 0^inf by rule 15

20. S (12)^a 1 <D (11)^b 2 0^inf --> S (12)^a 2 1 <D (11)^2b-1 0^inf
by:
S (12)^a 1 <D (11)^b 2 0^inf
--> S (12)^a 2 A> (11)^b 2 0^inf
--> S (12)^a 2 (12)^b A> 2 0^inf
--> S (12)^a 2 (12)^b <C 1 0^inf
--> S (12)^a 2 (12)^b-1 1 <D (11)^1 0^inf
--> S (12)^a 2 1 <D (11)^2b-1 0^inf by rule 15

21. S (12)^a 2^2 1 <D (11)^b 0^inf --> S (12)^a-1 2^2 1 <D (11)^2^(b+4)*3-5 0^inf
by:
S (12)^a 2^2 1 <D (11)^b 0^inf
--> S (12)^a 2^3 A> (11)^b 0^inf
--> S (12)^a 2^3 (12)^b A> 0^inf
--> S (12)^a 2^3 <A (11)^b+1 0^inf
--> S (12)^a 2^2 <C 1 (11)^b+1 0^inf
--> S (12)^a 2 <D (11)^b+2 0^inf
--> S (12)^a <D (11)^b+3 2 0^inf by rule 10
--> S (12)^a-1 1 <D (11)^b+4 2^2 0^inf by rule 11
--> S (12)^a-1 2 A> (11)^b+4 2^2 0^inf
--> S (12)^a-1 2 (12)^b+4 A> 2^2 0^inf
--> S (12)^a-1 2 (12)^b+4 <C 1 2 0^inf
--> S (12)^a-1 2 (12)^b+3 1 <D (11)^1 2 0^inf
--> S (12)^a-1 2 (12)^b+3 2 1 <D (11)^1 0^inf by rule 20
--> S (12)^a-1 2^2 1 <D (11)^(2^(b+3)*1)+(2^(b+3)*5)-5 0^inf by rule 18
= S (12)^a-1 2^2 1 <D (11)^(2^(b+4)*3-5) 0^inf

22. S 1 <D (11)^b 2^2 0^inf --> S 2 (12)^b-1 2 1 <D (11)^1 0^inf
by:
S 1 <D (11)^b 2^2 0^inf
--> S 2 A> (11)^b 2^2 0^inf
--> S 2 (12)^b A> 2^2 0^inf
--> S 2 (12)^b <C 1 2 0^inf
--> S 2 (12)^b-1 1 <D (11)^1 2 0^inf
--> S 2 (12)^b-1 2 1 <D (11)^1 0^inf by rule 20

23. S (11)^a 2^2 1 <D (11)^b 0^inf --> S (11)^a-3 (12)^2b+11 2^2 1 <D (11)^1 0^inf
by:
S (11)^a 2^2 1 <D (11)^b 0^inf
--> S (11)^a 2^3 A> (11)^b 0^inf
--> S (11)^a 2^3 (12)^b A> 0^inf
--> S (11)^a 2^3 <A (11)^b+1 0^inf
--> S (11)^a 2^2 <C 1 (11)^b+1 0^inf
--> S (11)^a 2 <D (11)^b+2 0^inf
--> S (11)^a <D (11)^b+3 2 0^inf by rule 10
--> S (11)^a-1 1 2 A> (11)^b+3 2 0^inf
--> S (11)^a-1 (12)^b+4 A> 2 0^inf
--> S (11)^a-1 (12)^b+4 <C 1 0^inf
--> S (11)^a-1 (12)^b+3 1 <D (11)^1 0^inf
--> S (11)^a-1 1 <D (11)^2b+7 0^inf by rule 15
--> S (11)^a-1 2 A> (11)^2b+7 0^inf
--> S (11)^a-1 2 (12)^2b+7 A> 0^inf
--> S (11)^a-1 2 <A (11)^2b+8 0^inf
--> S (11)^a-1 <C 1 (11)^2b+8 0^inf
--> S (11)^a-2 1 <A (11)^2b+9 0^inf
--> S (11)^a-2 <A (11)^2b+10 2 0^inf by rule 12
--> S (11)^a-3 1 <A (11)^2b+11 2^2 0^inf by rule 13
--> S (11)^a-3 1 D> (11)^2b+11 2^2 0^inf
--> S (11)^a-3 1 (21)^2b+11 D> 2^2 0^inf
--> S (11)^a-3 1 (21)^2b+11 2^2 D> 0^inf
--> S (11)^a-3 1 (21)^2b+11 2^2 <B 2^2 0^inf
--> S (11)^a-3 1 (21)^2b+11 2 <C 1 2^2 0^inf
--> S (11)^a-3 1 (21)^2b+11 <D (11)^1 2^2 0^inf
= S (11)^a-3 (12)^2b+11 1 <D (11)^1 2^2 0^inf
--> S (11)^a-3 (12)^2b+11 2 (12)^0 2 1 <D (11)^1 0^inf by rule 22
= S (11)^a-3 (12)^2b+11 2^2 1 <D (11)^1 0^inf

24. 0^inf 2^2 1 <D (11)^c 0^inf --> 0^inf (11)^c+1 (12)^3 2^2 1 <D (11)^1 0^inf
by:
0^inf 2^2 1 <D (11)^c 0^inf
--> 0^inf 2^3 A> (11)^c 0^inf
--> 0^inf 2^3 (12)^c A> 0^inf
--> 0^inf 2^3 <A (11)^c+1 0^inf
--> 0^inf 2^2 <C 1 (11)^c+1 0^inf
--> 0^inf 2 <D (11)^c+2 0^inf
--> 0^inf <D (11)^c+3 2 0^inf by rule 10
--> 0^inf B> (11)^c+3 2 0^inf
--> 0^inf (11)^c+3 B> 2 0^inf
--> 0^inf (11)^c+3 <C 1 0^inf
--> 0^inf (11)^c+2 1 <A (11)^1 0^inf
--> 0^inf (11)^c+2 <A (11)^2 2 0^inf by rule 12
--> 0^inf (11)^c+1 1 <A (11)^3 2^2 0^inf by rule 13
--> 0^inf (11)^c+1 1 D> (11)^3 2^2 0^inf
--> 0^inf (11)^c+1 1 (21)^3 D> 2^2 0^inf
--> 0^inf (11)^c+1 1 (21)^3 2^2 D> 0^inf
--> 0^inf (11)^c+1 1 (21)^3 2^2 <B 2^2 0^inf
--> 0^inf (11)^c+1 (12)^3 1 2 <C 1 2^2 0^inf
--> 0^inf (11)^c+1 (12)^3 1 <D (11)^1 2^2 0^inf
--> 0^inf (11)^c+1 (12)^3 2 (12)^0 2 1 <D (11)^1 0^inf by rule 22
= 0^inf (11)^c+1 (12)^3 2^2 1 <D (11)^1 0^inf

25. 0^inf (11)^2 2^2 1 <D (11)^c 0^inf --> 0^inf 1 (11)^2c+8 (12)^3 2^2 1 <D (11)^1 0^inf
by:
0^inf (11)^2 2^2 1 <D (11)^c 0^inf
--> 0^inf (11)^2 2^3 A> (11)^c 0^inf
--> 0^inf (11)^2 2^3 (12)^c A> 0^inf
--> 0^inf (11)^2 2^3 <A (11)^c+1 0^inf
--> 0^inf (11)^2 2^2 <C 1 (11)^c+1 0^inf
--> 0^inf (11)^2 2 <D (11)^c+2 0^inf
--> 0^inf (11)^2 <D (11)^c+3 2 0^inf by rule 10
--> 0^inf (11)^1 1 2 A> (11)^c+3 2 0^inf
--> 0^inf (11)^1 (12)^c+4 A> 2 0^inf
--> 0^inf (11)^1 (12)^c+4 <C 1 0^inf
--> 0^inf (11)^1 (12)^c+3 1 <D (11)^1 0^inf
--> 0^inf (11)^1 1 <D (11)^2c+7 0^inf by rule 15
--> 0^inf (11)^1 2 A> (11)^2c+7 0^inf
--> 0^inf (11)^1 2 (12)^2c+7 A> 0^inf
--> 0^inf (11)^1 2 <A (11)^2c+8 0^inf
--> 0^inf (11)^1 <C 1 (11)^2c+8 0^inf
--> 0^inf 1 <A (11)^2c+9 0^inf
--> 0^inf <A (11)^2c+10 2 0^inf by rule 12
--> 0^inf 1 B> (11)^2c+10 2 0^inf
--> 0^inf 1 (11)^2c+10 B> 2 0^inf
--> 0^inf 1 (11)^2c+10 <C 1 0^inf
--> 0^inf (11)^2c+10 <A (11)^1 0^inf
--> 0^inf (11)^2c+9 1 <A (11)^2 2 0^inf by rule 12
--> 0^inf (11)^2c+9 <A (11)^3 2^2 0^inf by rule 13
--> 0^inf (11)^2c+9 D> (11)^3 2^2 0^inf
--> 0^inf (11)^2c+9 (21)^3 D> 2^2 0^inf
--> 0^inf (11)^2c+9 (21)^3 2^2 D> 0^inf
--> 0^inf (11)^2c+9 (21)^3 2^2 <B 2^2 0^inf
--> 0^inf (11)^2c+9 (21)^3 2 <C 1 2^2 0^inf
--> 0^inf 1 (11)^2c+8 (12)^3 1 <D (11)^1 2^2 0^inf
--> 0^inf 1 (11)^2c+8 (12)^3 2 (12)^0 2 1 <D (11)^1 0^inf by rule 22
= 0^inf 1 (11)^2c+8 (12)^3 2^2 1 <D (11)^1 0^inf

26. 0^inf 1 (11)^1 2^2 1 <D (11)^c 0^inf --> 0^inf 1 (11)^2c+7 (12)^3 2^2 1 <D (11)^1 0^inf
by:
0^inf 1 (11)^1 2^2 1 <D (11)^c 0^inf
--> 0^inf 1 (11)^1 2^3 A> (11)^c 0^inf
--> 0^inf 1 (11)^1 2^3 (12)^c A> 0^inf
--> 0^inf 1 (11)^1 2^3 <A (11)^c+1 0^inf
--> 0^inf 1 (11)^1 2^2 <C 1 (11)^c+1 0^inf
--> 0^inf 1 (11)^1 2 <D (11)^c+2 0^inf
--> 0^inf 1 (11)^1 <D (11)^c+3 2 0^inf by rule 10
--> 0^inf (11)^1 2 A> (11)^c+3 2 0^inf
--> 0^inf (11)^1 2 (12)^c+3 A> 2 0^inf
--> 0^inf (11)^1 2 (12)^c+3 <C 1 0^inf
--> 0^inf (11)^1 2 (12)^c+2 1 <D (11)^1 0^inf
--> 0^inf (11)^1 2 1 <D (11)^2c+5 0^inf by rule 15
--> 0^inf (11)^1 2^2 A> (11)^2c+5 0^inf
--> 0^inf (11)^1 2^2 (12)^2c+5 A> 0^inf
--> 0^inf (11)^1 2^2 <A (11)^2c+6 0^inf
--> 0^inf (11)^1 2 <C 1 (11)^2c+6 0^inf
--> 0^inf (11)^1 <D (11)^2c+7 0^inf
--> 0^inf 1 2 A> (11)^2c+7 0^inf
--> 0^inf (12)^2c+8 A> 0^inf
--> 0^inf <A (11)^2c+9 0^inf
--> 0^inf 1 B> (11)^2c+9 0^inf
--> 0^inf 1 (11)^2c+9 B> 0^inf
--> 0^inf 1 (11)^2c+9 <B 2 0^inf
--> 0^inf 1 (11)^2c+9 B> 2 0^inf
--> 0^inf 1 (11)^2c+9 <C 1 0^inf
--> 0^inf 1 (11)^2c+8 1 <A (11)^1 0^inf
--> 0^inf 1 (11)^2c+8 <A (11)^2 2 0^inf by rule 12
--> 0^inf (11)^2c+8 <A (11)^3 2^2 0^inf by rule 13
--> 0^inf (11)^2c+8 D> (11)^3 2^2 0^inf
--> 0^inf (11)^2c+8 (21)^3 D> 2^2 0^inf
--> 0^inf (11)^2c+8 (21)^3 2^2 D> 0^inf
--> 0^inf (11)^2c+8 (21)^3 2^2 <B 2^2 0^inf
--> 0^inf 1 (11)^2c+7 (12)^3 1 2 <C 1 2^2 0^inf
--> 0^inf 1 (11)^2c+7 (12)^3 1 <D (11)^1 2^2 0^inf
--> 0^inf 1 (11)^2c+7 (12)^3 2 (12)^0 2 1 <D (11)^1 0^inf by rule 22
= 0^inf 1 (11)^2c+7 (12)^3 2^2 1 <D (11)^1 0^inf

27. 0^inf 1 2^2 1 <D (11)^c 0^inf --> 0^inf (11)^2c+5 (12)^3 2^2 1 <D (11)^1 0^inf
by:
0^inf 1 2^2 1 <D (11)^c 0^inf
--> 0^inf 1 2^3 A> (11)^c 0^inf
--> 0^inf 1 2^3 (12)^c A> 0^inf
--> 0^inf 1 2^3 <A (11)^c+1 0^inf
--> 0^inf 1 2^2 <C 1 (11)^c+1 0^inf
--> 0^inf 1 2 <D (11)^c+2 0^inf
--> 0^inf 1 <D (11)^c+3 2 0^inf by rule 10
--> 0^inf 2 A> (11)^c+3 2 0^inf
--> 0^inf 2 (12)^c+3 A> 2 0^inf
--> 0^inf 2 (12)^c+3 <C 1 0^inf
--> 0^inf 2 (12)^c+2 1 <D (11)^1 0^inf
--> 0^inf 2 1 <D (11)^2c+5 0^inf by rule 15
--> 0^inf 2^2 A> (11)^2c+5 0^inf
--> 0^inf 2^2 (12)^2c+5 A> 0^inf
--> 0^inf 2^2 <A (11)^2c+6 0^inf
--> 0^inf 2 <C 1 (11)^2c+6 0^inf
--> 0^inf <D (11)^2c+7 0^inf
--> 0^inf B> (11)^2c+7 0^inf
--> 0^inf (11)^2c+7 B> 0^inf
--> 0^inf (11)^2c+7 <B 2 0^inf
--> 0^inf (11)^2c+7 B> 2 0^inf
--> 0^inf (11)^2c+7 <C 1 0^inf
--> 0^inf (11)^2c+6 1 <A (11)^1 0^inf
--> 0^inf (11)^2c+6 <A (11)^2 2 0^inf by rule 12
--> 0^inf (11)^2c+5 1 <A (11)^3 2^2 0^inf by rule 13
--> 0^inf (11)^2c+5 1 D> (11)^3 2^2 0^inf
--> 0^inf (11)^2c+5 1 (21)^3 D> 2^2 0^inf
--> 0^inf (11)^2c+5 (12)^3 1 2^2 D> 0^inf
--> 0^inf (11)^2c+5 (12)^3 1 2^2 <B 2^2 0^inf
--> 0^inf (11)^2c+5 (12)^3 1 2 <C 1 2^2 0^inf
--> 0^inf (11)^2c+5 (12)^3 1 <D (11)^1 2^2 0^inf
--> 0^inf (11)^2c+5 (12)^3 2 (12)^0 2 1 <D (11)^1 0^inf by rule 22
= 0^inf (11)^2c+5 (12)^3 2^2 1 <D (11)^1 0^inf

28. 0^inf (11)^1 2^2 1 <D (11)^c 0^inf --> 0^inf 1 Z> 1 (11)^2c+8 0^inf
by:
0^inf (11)^1 2^2 1 <D (11)^c 0^inf
--> 0^inf (11)^1 2^3 A> (11)^c 0^inf
--> 0^inf (11)^1 2^3 (12)^c A> 0^inf
--> 0^inf (11)^1 2^3 <A (11)^c+1 0^inf
--> 0^inf (11)^1 2^2 <C 1 (11)^c+1 0^inf
--> 0^inf (11)^1 2 <D (11)^c+2 0^inf
--> 0^inf (11)^1 <D (11)^c+3 2 0^inf by rule 10
--> 0^inf 1 2 A> (11)^c+3 2 0^inf
--> 0^inf (12)^c+4 A> 2 0^inf
--> 0^inf (12)^c+4 <C 1 0^inf
--> 0^inf (12)^c+3 1 <D (11)^1 0^inf
--> 0^inf 1 <D (11)^2c+7 0^inf by rule 15
--> 0^inf 2 A> (11)^2c+7 0^inf
--> 0^inf 2 (12)^2c+7 A> 0^inf
--> 0^inf 2 <A (11)^2c+8 0^inf
--> 0^inf <C 1 (11)^2c+8 0^inf
--> 0^inf 1 Z> 1 (11)^2c+8 0^inf

Note: Rule 29 is not relevant to this TMs trajectory.
29. 0^inf 1 (11)^2 2^2 1 <D (11)^c 0^inf --> 0^inf (11)^2c+10 (12)^2 2^2 1 <D (11)^1 0^inf
by:
0^inf 1 (11)^2 2^2 1 <D (11)^c 0^inf
--> 0^inf 1 (11)^2 2^3 A> (11)^c 0^inf
--> 0^inf 1 (11)^2 2^3 (12)^c A> 0^inf
--> 0^inf 1 (11)^2 2^3 <A (11)^c+1 0^inf
--> 0^inf 1 (11)^2 2^2 <C 1 (11)^c+1 0^inf
--> 0^inf 1 (11)^2 2 <D (11)^c+2 0^inf
--> 0^inf 1 (11)^2 <D (11)^c+3 2 0^inf by rule 10
--> 0^inf (11)^2 2 A> (11)^c+3 2 0^inf
--> 0^inf (11)^2 2 (12)^c+3 A> 2 0^inf
--> 0^inf (11)^2 2 (12)^c+3 <C 1 0^inf
--> 0^inf (11)^2 2 (12)^c+2 1 <D (11)^1 0^inf
--> 0^inf (11)^2 2 1 <D (11)^2c+5 0^inf by rule 15
--> 0^inf (11)^2 2^2 A> (11)^2c+5 0^inf
--> 0^inf (11)^2 2^2 (12)^2c+5 A> 0^inf
--> 0^inf (11)^2 2^2 <A (11)^2c+6 0^inf
--> 0^inf (11)^2 2 <C 1 (11)^2c+6 0^inf
--> 0^inf (11)^2 <D (11)^2c+7 0^inf
--> 0^inf (11)^1 1 2 A> (11)^2c+7 0^inf
--> 0^inf (11)^1 (12)^2c+8 A> 0^inf
--> 0^inf (11)^1 <A (11)^2c+9 0^inf
--> 0^inf 1 <A (11)^2c+10 2 0^inf by rule 12
--> 0^inf <A (11)^2c+11 2^2 0^inf by rule 13
--> 0^inf 1 B> (11)^2c+11 2^2 0^inf
--> 0^inf 1 (11)^2c+11 B> 2^2 0^inf
--> 0^inf 1 (11)^2c+11 <C 1 2 0^inf
--> 0^inf (11)^2c+11 <A (11)^1 2 0^inf
--> 0^inf (11)^2c+10 1 <A (11)^2 2^2 0^inf by rule 13
--> 0^inf (11)^2c+10 1 D> (11)^2 2^2 0^inf
--> 0^inf (11)^2c+10 1 (21)^2 D> 2^2 0^inf
--> 0^inf (11)^2c+10 (12)^2 1 2^2 D> 0^inf
--> 0^inf (11)^2c+10 (12)^2 1 2^2 <B 2^2 0^inf
--> 0^inf (11)^2c+10 (12)^2 1 2 <C 1 2^2 0^inf
--> 0^inf (11)^2c+10 (12)^2 1 <D (11)^1 2^2 0^inf
--> 0^inf (11)^2c+10 (12)^2 2 (12)^0 2 1 <D (11)^1 0^inf by rule 22
= 0^inf (11)^2c+10 (12)^2 2^2 1 <D (11)^1 0^inf

Functions

Let D(a, b, c) = 0^inf (11)^a (12)^b 2^2 1 <D (11)^c 0^inf

Let D_1(a, b, c) = 0^inf 1 (11)^a (12)^b 2^2 1 <D (11)^c 0^inf

Let $f_1(n)=2^{n+4}\times 3-5$

Let $f_2(a,b)=f_1^{2\times f_2(a-1,b)+11}(1)$, where$f_2(0,b)=b$

Rule 21 becomes:

• $D(a,b,c)-->D(a,b-1,2^{b+4}\times 3-5)$
• $D_1(a,b,c)-->D_1(a,b-1,2^{b+4}\times 3-5)$

Rule 23 becomes:

• $D(a,0,c)-->D(a-3,2c+11,1)$
• $D_1(a,0,c)-->D_1(a-3,2c+11,1)$

Rule 24 becomes:

• $D(0,0,c)-->D(c+1,3,1)$

Rule 25 becomes:

• $D(2,0,c)-->D(2c+8,3,1)$

Rule 26 becomes:

• $D_1(1,0,c)-->D_1(2c+7,3,1)$

Rule 27 becomes:

• $D_1(0,0,c)-->D(2c+5,3,1)$

Rule 28 becomes:

• D(1, 0, c) --> halt with score 4c + 18

Rule 29 becomes:

• $D_1(2,0,c)-->D(2c+10,2,1)$

By repeating rule 21, a stronger rule can be constructed:

• $D(a,b,c)-->D(a,0,f_1^b(c))$
• $D_1(a,b,c)-->D1(a,0,f_1^b(c))$

If a is greater than or equal to 3: $D(a,0,c)-->D(a-3,2c+11,1)-->D(a-3,0,f_1^{2c+11}(1))$ =$D(a-3,0,f_2(1,c))$

• $D(a,0,c)-->D(a-3,0,f_1^{2c+11}(1))$

This rule can also be repeated, also note that $f_1^{2c+11}(1)=f_2(1,c)$ and $f_1^{2\times f_2(a,b)+11}(1)=f_2(a+1,b)$:

• $D(3k+d,0,c)-->D(d,0,f_2(k,c))$
• $D_1(3k+d,0,c)-->D_1(d,0,f_2(k,c))$

Trajectory

S=0: 0^inf A> 0^inf
S=5: 0^inf <A (11)^1 0^inf
S=6: 0^inf 1 B> (11)^1 0^inf
S=8: 0^inf 1 (11)^1 B> 0^inf
S=9: 0^inf 1 (11)^1 <B 2 0^inf
S=10: 0^inf 1 (11)^1 B> 2 0^inf
S=11: 0^inf 1 (11)^1 <C 1 0^inf
S=12: 0^inf (11)^1 <A (11)^1 0^inf
S=23: 0^inf 1 <A (11)^2 2 0^inf
S=38: 0^inf <A (11)^3 2^2 0^inf
S=39: 0^inf 1 B> (11)^3 2^2 0^inf
S=45: 0^inf 1 (11)^3 B> 2^2 0^inf
S=46: 0^inf 1 (11)^3 <C 1 2 0^inf
S=47: 0^inf (11)^3 <A (11)^1 2 0^inf
S=58: 0^inf 1 (11)^2 <A (11)^2 2^2 0^inf
S=59: 0^inf 1 (11)^2 D> (11)^2 2^2 0^inf
S=63: 0^inf 1 (11)^2 (21)^2 D> 2^2 0^inf
S=65: 0^inf 1 (11)^2 (21)^2 2^2 D> 0^inf
S=68: 0^inf 1 (11)^2 (21)^2 2^2 <B 2^2 0^inf
S=69: 0^inf 1 (11)^2 (21)^2 2 <C 1 2^2 0^inf
S=70: 0^inf (11)^2 (12)^2 1 <D (11)^1 2^2 0^inf
--> 0^inf (11)^2 (12)^2 2 (12)^0 2 1 <D (11)^1 0^inf
=0^inf (11)^2 (12)^2 2^2 1 <D (11)^1 0^inf
= D(2, 2, 1)
So, the TM starts in configuration D(2, 2, 1).

D(2, 2, 1) -->

$D(2,0,f_1^2(1))=D(2,0,f_1(91))$

$e_1=f_1(91)=2^{95}\times 3-5$

f_1(n) = 2^(n+4)*3 - 5
Note that the times three means that this expression of of the form 3k - 5 which can be rewritten as 3(k-1)-2 which can again be rewritten as 3(k-2)+1.
Next, 3k+1 mod 3 = 1
So f_1(n) mod 3 = 1
Thus f_1^a(n) mod 3 = 1
f_2(a,b) = f_1^(2*f_2(a-1,b)+11)(1)
Note that f_1^(2*f_2(a-1,b)+11)(1) is also of the form f_1^a(n)
Thus f_2(a,b) mod 3 = 1

$D(2,0,e_1)$

-->$D_1(2e_1+8,3,1)-->D_1(2e_1+8,0,f_1^2(91))$

e_1 mod 3 = 1; 2*1 + 8 = 10 --> 10 mod 3 = 1

$D_1(2e_1+8,0,f_1^2(91))$

--> $D_1(1,0,f_2(\frac{2e_1+7}{3},f_1^2(91)))$

$e_2=f_2(\frac{2e_1+7}{3},f_1^2(91))$

$D_1(1,0,e_3)$

$e_{2}mod3=1$

--> $D_1(2e_2+7,3,1)-->D_1(2e_2+7,0,f_1^2(91))$

2e_3 + 7

Modulus: 2 + 7 --> 9 mod 3 = 0

--> $D_1(0,0,f_2(\frac{2e_2+7}{3},f_1^2(91)))$

$e_3=f_2(\frac{2e_2+7}{3},f_1^2(91))$

$D_1(0,0,e_3)$

--> $D(2e_3+5,3,1)-->D(2e_3+5,0,f_1^2(91))$

e_3 mod 3 = 1; 2*1+5 = 7 --> 7 mod 3 = 1

--> $D(1,0,f_2(\frac{2e_3+4}{3},f_1^2(91)))$

$e_4=f_2(\frac{2e_3+4}{3},f_1^2(91))$

$D(1,0,e_4)$

--> halts with score $4e_4+18$.

Approximate Score

$4e_4+18$

$e_4=f_2(\frac{2e_3+4}{3},f_1^2(91))$

$e_3=f_2(\frac{2e_2+7}{3},f_1^2(91))$

$e_2=f_2(\frac{e_1+7}{3},f_1^2(91))$

$e_1=2^{95}\times 3-5$

$f_1(n)=2^{n+4}\times 3-5$

$f_2(a,b)=f_1^{2\times f_2(a-1,b)+11}(1)$, where $f_2(0,b)=b$

• $f_1(n):$

$2^{n+5}<f_1(n)<2^{n+6}$

$(2\uparrow {)}^{a}n+5<f_1^a(n)<(2\uparrow {)}^{a}n+7$

$(2\uparrow {)}^{a}5<f_1^a(1)<(2\uparrow {)}^{a}8$

$2\uparrow \uparrow (a+2)<f_1^a(1)<2\uparrow \uparrow (a+3)$

• $f_2(a,b):$

$f_2(a,b)=f_1^{2\times f_2(a-1,b)+11}(1)$, where $f_2(0,b)=b$

$2\uparrow \uparrow (2\times f_2(a-1,b)+13)<f_2(a,b)<2\uparrow \uparrow (2\times f_2(a-1,b)+14)$

$(2\uparrow \uparrow {)}^{a}b<f_2(a,b)<(2\uparrow \uparrow {)}^{a+1}b$

$2\uparrow \uparrow 2\uparrow \uparrow 2<e_1<f_1^2(91)<2\uparrow \uparrow 2\uparrow \uparrow 2\uparrow \uparrow 2$

$(2\uparrow \uparrow {)}^a(2\uparrow \uparrow 2\uparrow \uparrow 2)<f_2(a,f_1^2(91))<(2\uparrow \uparrow {)}^a(2\uparrow \uparrow 2\uparrow \uparrow 2\uparrow \uparrow 2)$

$2\uparrow \uparrow \uparrow (a+3)<f_2(a,f_1^2(91))<2\uparrow \uparrow \uparrow (a+4)$

$2\uparrow \uparrow \uparrow (7.92\times 10^{28})<e_2<2\uparrow \uparrow \uparrow (7.93\times 10^{28})$

$2\uparrow \uparrow \uparrow 2\uparrow \uparrow \uparrow (7.92\times 10^{28})<e_3<2\uparrow \uparrow \uparrow 2\uparrow \uparrow \uparrow (7.93\times 10^{28})$

$2{\uparrow }^{4}5<2\uparrow \uparrow \uparrow 2\uparrow \uparrow \uparrow 2\uparrow \uparrow \uparrow (7.92\times 10^{28})<e_4<\sigma <S<2\uparrow \uparrow \uparrow 2\uparrow \uparrow \uparrow 2\uparrow \uparrow \uparrow (7.93\times 10^{28})$

This score would make 1RB1RD1LC_2LB1RB1LC_1RZ1LA1LD_0RB2RA2RD (bbch) the new BB(4,3) champion.

1RB2LB0LB_2LC2LA0LA_2RD1LC1RZ_1RA2LD1RD (bbch)

3. One of the seven potential BB(4,3) champions discovered by Pavel Kropitz in May 2024.

Analysis

	0	1	2
A	1RB	2LB	0LB
B	2LC	2LA	0LA
C	2RD	1LC	1RZ
D	1RA	2LD	1RD

S is any tape configuration

1. S 1^a <C S --> S <C 1^a S [+a steps]
2. S 1^a <D S --> S <D 2^a S [+a steps]
3. S D> 2^a S --> S 1^a D> S [+a steps]

4. S (11)^a <A S --> S <A (22)^a S [+2a steps]
   S (11)^a <B S --> S <B (22)^a S [+2a steps]

5. 0^inf 2 (11)^a A> (22)^b S --> 0^inf 2 (11)^a+3 A> (22)^b-1 S [+8a +24 steps]
by:
0^inf 2 (11)^a A> (22)^b S
--> 0^inf 2 (11)^a <B 0 2 (22)^b-1 S [+1]
--> 0^inf 2 <B (22)^a 0 2 (22)^b-1 S [+2a +1]
--> 0^inf <A 0 (22)^a 0 2 (22)^b-1 S [+2a +2]
--> 0^inf 1 B> 0 (22)^a 0 2 (22)^b-1 S [+2a +3]
--> 0^inf 1 <C 2 (22)^a 0 2 (22)^b-1 S [+2a +4]
--> 0^inf <C 1 2 (22)^a 0 2 (22)^b-1 S [+2a +5]
--> 0^inf 2 D> 1 2 (22)^a 0 2 (22)^b-1 S [+2a +6]
--> 0^inf 2 <D (22)^a+1 0 2 (22)^b-1 S [+2a +7]
--> 0^inf 1 D> (22)^a+1 0 2 (22)^b-1 S [+2a +8]
--> 0^inf 1 (11)^a+1 D> 0 2 (22)^b-1 S [+4a +10]
--> 0^inf (11)^a+2 A> 2 (22)^b-1 S [+4a +11]
--> 0^inf (11)^a+2 <B 0 (22)^b-1 S [+4a +12]
--> 0^inf <B (22)^a+2 0 (22)^b-1 S [+6a +16]
--> 0^inf <C 2 (22)^a+2 0 (22)^b-1 S [+6a +17]
--> 0^inf 2 D> 2 (22)^a+2 0 (22)^b-1 S [+6a +18]
--> 0^inf 2 1 (11)^a+2 D> 0 (22)^b-1 S [+8a +23]
--> 0^inf 2 (11)^a+3 A> (22)^b-1 S [+8a +24]

6. 0^inf 2 (11)^a A> (22)^b S --> 0^inf 2 (11)^a+3b A> S
by repetition of rule 5

7. 0^inf 2 (11)^a A> 0 (22)^b S --> 0^inf 2 1 (11)^1 A> (22)^a+2 0 (22)^b-1 S [+6a +28 steps]
by:
0^inf 2 (11)^a A> 0 (22)^b S
--> 0^inf 2 (11)^a 1 B> (22)^b S [+1]
--> 0^inf 2 1 (11)^a <A 0 2 (22)^b-1 S [+2]
--> 0^inf 2 1 <A (22)^a 0 2 (22)^b-1 S [+2a +2]
--> 0^inf 2 <B 2 (22)^a 0 2 (22)^b-1 S [+2a +3]
--> 0^inf <A 0 2 (22)^a 0 2 (22)^b-1 S [+2a +4]
--> 0^inf 1 B> 0 2 (22)^a 0 2 (22)^b-1 S [+2a +5]
--> 0^inf 1 <C (22)^a+1 0 2 (22)^b-1 S [+2a +6]
--> 0^inf <C 1 (22)^a+1 0 2 (22)^b-1 S [+2a +7]
--> 0^inf 2 D> 1 (22)^a+1 0 2 (22)^b-1 S [+2a +8]
--> 0^inf 2 <D 2 (22)^a+1 0 2 (22)^b-1 S [+2a +9]
--> 0^inf 1 D> 2 (22)^a+1 0 2 (22)^b-1 S [+2a +10]
--> 0^inf (11)^a+2 D> 0 2 (22)^b-1 S [+4a +13]
--> 0^inf (11)^a+2 1 A> 2 (22)^b-1 S [+4a +14]
--> 0^inf (11)^a+2 1 <B 0 (22)^b-1 S [+4a +15]
--> 0^inf 1 <B (22)^a+2 0 (22)^b-1 S [+6a +19]
--> 0^inf <A 2 (22)^a+2 0 (22)^b-1 S [+6a +20]
--> 0^inf 1 B> 2 (22)^a+2 0 (22)^b-1 S [+6a +21]
--> 0^inf 1 <A 0 (22)^a+2 0 (22)^b-1 S [+6a +22]
--> 0^inf <B 2 0 (22)^a+2 0 (22)^b-1 S [+6a +23]
--> 0^inf <C 2 2 0 (22)^a+2 0 (22)^b-1 S [+6a +24]
--> 0^inf 2 D> (22)^1 0 (22)^a+2 0 (22)^b-1 S [+6a +25]
--> 0^inf 2 1 1 D> 0 (22)^a+2 0 (22)^b-1 S [+6a +27]
--> 0^inf 2 1 (11)^1 A> (22)^a+2 0 (22)^b-1 S [+6a +28]

8. 0^inf 2 (11)^a A> 2 0 2 S --> 0^inf 2 1 (11)^a+3 A> S [+8a +27 steps]
by:
0^inf 2 (11)^a A> 2 0 2 S
--> 0^inf 2 (11)^a <B 0^2 2 S [+1]
--> 0^inf 2 <B (22)^a 0^2 2 S [+2a +1]
--> 0^inf <A 0 (22)^a 0^2 2 S [+2a +2]
--> 0^inf 1 B> 0 (22)^a 0^2 2 S [+2a +3]
--> 0^inf 1 <C 2 (22)^a 0^2 2 S [+2a +4]
--> 0^inf <C 1 2 (22)^a 0^2 2 S [+2a +5]
--> 0^inf 2 D> 1 2 (22)^a 0^2 2 S [+2a +6]
--> 0^inf 2 <D (22)^a+1 0^2 2 S [+2a +7]
--> 0^inf 1 D> (22)^a+1 0^2 2 S [+2a +8]
--> 0^inf 1 (11)^a+1 D> 0^2 2 S [+4a +10]
--> 0^inf (11)^a+2 A> 0 2 S [+4a +11]
--> 0^inf (11)^a+2 1 B> 2 S [+4a +12]
--> 0^inf (11)^a+2 1 <A 0 S [+4a +13]
--> 0^inf 1 <A (22)^a+2 0 S [+6a +17]
--> 0^inf <B 2 (22)^a+2 0 S [+6a +18]
--> 0^inf <C (22)^a+3 0 S [+6a +19]
--> 0^inf 2 D> (22)^a+3 0 S [+6a +20]
--> 0^inf 2 (11)^a+3 D> 0 S [+8a +26]
--> 0^inf 2 1 (11)^a+3 A> S [+8a +27]

9. 0^inf 2 1 (11)^a A> (22)^b S --> 0^inf 2 1 (11)^3a+4 A> (22)^b-1 S
by:
0^inf 2 1 (11)^a A> (22)^b S
--> 0^inf 2 1 (11)^a <B 0 2 (22)^b-1 S
--> 0^inf 2 1 <B (22)^a 0 2 (22)^b-1 S
--> 0^inf 2 <A 2 (22)^a 0 2 (22)^b-1 S
--> 0^inf <B 0 2 (22)^a 0 2 (22)^b-1 S
--> 0^inf <C 2 0 2 (22)^a 0 2 (22)^b-1 S
--> 0^inf 2 D> 2 0 2 (22)^a 0 2 (22)^b-1 S
--> 0^inf 2 1 D> 0 2 (22)^a 0 (22)^b-1 2 S
--> 0^inf 2 (11)^1 A> (22)^a 2 0 (22)^b-1 2 S
--> 0^inf 2 (11)^3a+1 A> 2 0 2 (22)^b-1 S by rule 6
--> 0^inf 2 1 (11)^3a+4 A> (22)^b-1 S by rule 8
= 0^inf 2 1 (11)^g_1(a) A> (22)^b-1 S

10. 0^inf 2 1 (11)^a A> (22)^b S --> 0^inf 2 1 (11)^g_1^b(a) A> S
by repetition of rule 9
g_1(n) = 3n + 4 

11. 0^inf 2 1 (11)^a A> 0 (22)^b S --> 0^inf 2 1 (11)^1 A> (22)^3a+6 0 (22)^b-2 2 S
by:
0^inf 2 1 (11)^a A> 0 (22)^b S
--> 0^inf 2 (11)^a+1 B> (22)^b S
--> 0^inf 2 (11)^a+1 <A 0 2 (22)^b-1 S
--> 0^inf 2 <A (22)^a+1 0 2 (22)^b-1 S
--> 0^inf <B 0 (22)^a+1 0 2 (22)^b-1 S
--> 0^inf <C 2 0 (22)^a+1 0 2 (22)^b-1 S
--> 0^inf 2 D> 2 0 (22)^a+1 0 2 (22)^b-1 S
--> 0^inf 2 1 D> 0 (22)^a+1 0 2 (22)^b-1 S
--> 0^inf 2 (11)^1 A> (22)^a+1 0 (22)^b-1 2 S
--> 0^inf 2 (11)^3a+4 A> 0 (22)^b-1 2 S by rule 6
Call this rule 11-1
--> 0^inf 2 1 (11)^1 A> (22)^3a+6 0 (22)^b-2 2 S by rule 7
Call this rule 11-2

12. 0^inf 2 (11)^a A> 0 11 S --> 0^inf 2 1 (11)^1 A> 0 (22)^a+2 2 S [+6a +31 steps]
by:
0^inf 2 (11)^a A> 0 11 S
--> 0^inf 2 (11)^a 1 B> 11 S [+1]
--> 0^inf 2 (11)^a 1 <A 2 1 S [+2]
--> 0^inf 2 1 <A (22)^a 2 1 S [+2a +2]
--> 0^inf 2 <B (22)^a+1 1 S [+2a +3]
--> 0^inf <A 0 (22)^a+1 1 S [+2a +4]
--> 0^inf 1 B> 0 (22)^a+1 1 S [+2a +5]
--> 0^inf 1 <C 2 (22)^a+1 1 S [+2a +6]
--> 0^inf <C 1 2 (22)^a+1 1 S [+2a +7]
--> 0^inf 2 D> 1 2 (22)^a+1 1 S [+2a +8]
--> 0^inf 2 <D (22)^a+2 1 S [+2a +9]
--> 0^inf 1 D> (22)^a+2 1 S [+2a +10]
--> 0^inf 1 (11)^a+2 D> 1 S [+4a +14]
--> 0^inf 1 (11)^a+2 <D 2 S [+4a +15]
--> 0^inf <D (22)^a+3 S [+6a +20]
--> 0^inf 1 A> (22)^a+3 S [+6a +21]
--> 0^inf 1 <B 0 2 (22)^a+2 S [+6a +22]
--> 0^inf <A 2 0 2 (22)^a+2 S [+6a +23]
--> 0^inf 1 B> 2 0 2 (22)^a+2 S [+6a +24]
--> 0^inf 1 <A 0 0 2 (22)^a+2 S [+6a +25]
--> 0^inf <B 2 0 0 2 (22)^a+2 S [+6a +26]
--> 0^inf <C (22)^1 0 0 2 (22)^a+2 S [+6a +27]
--> 0^inf 2 D> (22)^1 0 0 2 (22)^a+2 S [+6a +28]
--> 0^inf 2 (11)^1 D> 0 0 2 (22)^a+2 S [+6a +30]
--> 0^inf 2 1 (11)^1 A> 0 (22)^a+2 2 S [+6a +31]

13. 0^inf 2 1 (11)^a A> 0 2^b S --> 0^inf 2 1 (11)^g_2(a) A> 0 2^b-3 S
by:
0^inf 2 1 (11)^a A> 0 2^b S
--> 0^inf 2 1 (11)^1 A> (22)^3a+6 0 2^b-3 S by rule 11-2
--> 0^inf 2 1 (11)^g_1^(3a+6)(1) A> 0 2^b-3 S by rule 10
= 0^inf 2 1 (11)^(3^(3a+7)-2) A> 0 2^b-3 S
= 0^inf 2 1 (11)^g_2(a) A> 0 2^b-3 S

14. 0^inf 2 1 (11)^a A> 0 2^3k+v S --> 0^inf 2 1 (11)^(g_2)^k(a) A> 0 2^v S
by repetition of rule 13

15. 0^inf 2 1 <A S --> 0^inf 1 D> 2^3 S [+8 steps]
by:
0^inf 2 1 <A S
--> 0^inf 2 <B 2 S
--> 0^inf <A 0 2 S
--> 0^inf 1 B> 0 2 S
--> 0^inf 1 <C 2 2 S
--> 0^inf <C 1 2^2 S
--> 0^inf 2 D> 1 2^2 S
--> 0^inf 2 <D 2^3 S
--> 0^inf 1 D> 2^3 S

16. 0^inf 2 1 (11)^a A> 0 2 1 2 0^inf --> 0^inf 2 1 (11)^1 A> 0 (22)^1 (11)^3a+7 2 0^inf
by:
0^inf 2 1 (11)^a A> 0 2 1 2 0^inf
--> 0^inf 2 (11)^a+1 B> 2 1 2 0^inf
--> 0^inf 2 (11)^a+1 <A 0 1 2 0^inf
--> 0^inf 2 <A (22)^a+1 0 1 2 0^inf
--> 0^inf <B 0 (22)^a+1 0 1 2 0^inf
--> 0^inf <C 2 0 (22)^a+1 0 1 2 0^inf
--> 0^inf 2 D> 2 0 (22)^a+1 0 1 2 0^inf
--> 0^inf 2 1 D> 0 (22)^a+1 0 1 2 0^inf
--> 0^inf 2 (11)^1 A> (22)^a+1 0 1 2 0^inf
--> 0^inf 2 (11)^3a+4 A> 0 1 2 0^inf by rule 6
--> 0^inf 2 (11)^3a+4 1 B> 1 2 0^inf
--> 0^inf 2 (11)^3a+4 1 <A (22)^1 0^inf
--> 0^inf 2 1 <A (22)^3a+5 0^inf
--> 0^inf 1 D> 2 (22)^3a+6 0^inf by rule 15
--> 0^inf (11)^3a+7 D> 0^inf
--> 0^inf (11)^3a+7 1 A> 0^inf
--> 0^inf (11)^3a+8 B> 0^inf
--> 0^inf (11)^3a+8 <C 2 0^inf
--> 0^inf <C (11)^3a+8 2 0^inf
--> 0^inf 2 D> (11)^3a+8 2 0^inf
--> 0^inf 2 <D 2 1 (11)^3a+7 2 0^inf
--> 0^inf 1 D> 2 1 (11)^3a+7 2 0^inf
--> 0^inf (11)^1 D> 1 (11)^3a+7 2 0^inf
--> 0^inf (11)^1 <D 2 (11)^3a+7 2 0^inf
--> 0^inf <D 2^3 (11)^3a+7 2 0^inf
--> 0^inf 1 A> (22)^1 2 (11)^3a+7 2 0^inf
--> 0^inf 1 <B 0 (22)^1 (11)^3a+7 2 0^inf
--> 0^inf <A 2 0 (22)^1 (11)^3a+7 2 0^inf
--> 0^inf 1 B> 2 0 (22)^1 (11)^3a+7 2 0^inf
--> 0^inf 1 <A 0 0 (22)^1 (11)^3a+7 2 0^inf
--> 0^inf <B 2 0 0 (22)^1 (11)^3a+7 2 0^inf
--> 0^inf <C 2 2 0 0 (22)^1 (11)^3a+7 2 0^inf
--> 0^inf 2 D> 2^2 0 0 (22)^1 (11)^3a+7 2 0^inf
--> 0^inf 2 (11)^1 D> 0 0 (22)^1 (11)^3a+7 2 0^inf
--> 0^inf 2 1 (11)^1 A> 0 (22)^1 (11)^3a+7 2 0^inf

17. 0^inf 2 1 (11)^a A> 0 (22)^1 1 S --> 0^inf 2 1 (11)^1 A> (22)^3a+6 2 S
by:
0^inf 2 1 (11)^a A> 0 (22)^1 1 S
--> 0^inf 2 (11)^3a+4 A> 0 2 1 S by rule 11-1
--> 0^inf 2 (11)^3a+4 1 B> 2 1 S
--> 0^inf 2 1 (11)^3a+4 <A 0 1 S
--> 0^inf 2 1 <A (22)^3a+4 0 1 S
--> 0^inf 1 D> 2 (22)^3a+5 0 1 S by rule 15
--> 0^inf (11)^3a+6 D> 0 1 S
--> 0^inf (11)^3a+6 1 A> 1 S
--> 0^inf (11)^3a+6 1 <B 2 S
--> 0^inf 1 <B (22)^3a+6 2 S
--> 0^inf <A (22)^3a+7 S
--> 0^inf 1 B> (22)^3a+7 S
--> 0^inf 1 <A 0 2 (22)^3a+6 S
--> 0^inf <B 2 0 2 (22)^3a+6 S
--> 0^inf <C 2 2 0 2 (22)^3a+6 S
--> 0^inf 2 D> 2 2 0 (22)^3a+6 2 S
--> 0^inf 2 (11)^1 D> 0 (22)^3a+6 2 S
--> 0^inf 2 1 (11)^1 A> (22)^3a+6 2 S

18. 0^inf 2 1 (11)^a A> 0 (22)^1 1 S --> 0^inf 2 1 (11)^g_2(a) A> 2 S
by:
0^inf 2 1 (11)^a A> 0 (22)^1 1 S
--> 0^inf 2 1 (11)^1 A> (22)^3a+6 2 S by rule 17
--> 0^inf 2 1 (11)^g_1^(3a+6)(1) A> 2 S by rule 10
= 0^inf 2 1 (11)^(3^(3a+7)-2) A> 2 S
= 0^inf 2 1 (11)^g_2(a) A> 2 S

19. 0^inf 2 1 (11)^a A> 2 1^3 S --> 0^inf 2 1 (11)^1 A> 0 (22)^3a+5 2 S
by:
0^inf 2 1 (11)^a A> 2 1^3 S
--> 0^inf 2 1 (11)^a <B 0 1^3 S
--> 0^inf 2 1 <B (22)^a 0 1^3 S
--> 0^inf 2 <A 2 (22)^a 0 1^3 S
--> 0^inf <B 0 2 (22)^a 0 1^3 S
--> 0^inf <C 2 0 2 (22)^a 0 1^3 S
--> 0^inf 2 D> 2 0 2 (22)^a 0 1^3 S
--> 0^inf 2 1 D> 0 (22)^a 2 0 1^3 S
--> 0^inf 2 (11)^1 A> (22)^a 2 0 1^3 S
--> 0^inf 2 (11)^3a+1 A> 2 0 1^3 S by rule 6
--> 0^inf 2 (11)^3a+1 <B 0 0 1^3 S
--> 0^inf 2 <B (22)^3a+1 0 0 1^3 S
--> 0^inf <A 0 (22)^3a+1 0 0 1^3 S
--> 0^inf 1 B> 0 (22)^3a+1 0 0 1^3 S
--> 0^inf 1 <C 2 (22)^3a+1 0 0 1^3 S
--> 0^inf <C 1 2 (22)^3a+1 0 0 1^3 S
--> 0^inf 2 D> 1 2 (22)^3a+1 0 0 1^3 S
--> 0^inf 2 <D (22)^3a+2 0 0 1^3 S
--> 0^inf 1 D> (22)^3a+2 0 0 1^3 S
--> 0^inf 1 (11)^3a+2 D> 0 0 1^3 S
--> 0^inf (11)^3a+3 A> 0 1^3 S
--> 0^inf (11)^3a+3 1 B> 1^3 S
Call this rule 19***
with:
0^inf 2 1 (11)^a A> 2 S --> 0^inf (11)^3a+3 1 B> S
Continuing:
--> 0^inf (11)^3a+3 1 <A 2 1^2 S
--> 0^inf 1 <A (22)^3a+3 2 1^2 S
--> 0^inf <B (22)^3a+4 1^2 S
Call this rule 19**
with:
0^inf 2 1 (11)^a A> 2 1 S --> 0^inf <B (22)^3a+4 S
Continuing:
--> 0^inf <C 2 (22)^3a+4 1^2 S
--> 0^inf 2 D> 2 (22)^3a+4 1^2 S
--> 0^inf 2 1 (11)^3a+4 D> 1^2 S
--> 0^inf 2 1 (11)^3a+4 <D 2 1 S
--> 0^inf 2 <D (22)^3a+5 1 S
--> 0^inf 1 D> (22)^3a+5 1 S
--> 0^inf 1 (11)^3a+5 D> 1 S
Call this rule 19*
with:
0^inf 2 1 (11)^a A> 2 1^2 S --> 0^inf 1 (11)^3a+5 D> S
Continuing:
--> 0^inf 1 (11)^3a+5 <D 2 S
--> 0^inf <D (22)^3a+6 S
--> 0^inf 1 A> (22)^3a+6 S
--> 0^inf 1 <B 0 2 (22)^3a+5 S
--> 0^inf <A 2 0 2 (22)^3a+5 S
--> 0^inf 1 B> 2 0 2 (22)^3a+5 S
--> 0^inf 1 <A 0 0 2 (22)^3a+5 S
--> 0^inf <B 2 0 0 (22)^3a+5 2 S
--> 0^inf <C (22)^1 0 0 (22)^3a+5 2 S
--> 0^inf 2 D> (22)^1 0 0 (22)^3a+5 2 S
--> 0^inf 2 (11)^1 D> 0 0 (22)^3a+5 2 S
--> 0^inf 2 1 (11)^1 A> 0 (22)^3a+5 2 S
This rule can be rewritten as:
0^inf 2 1 (11)^a A> 2 1^b S --> 0^inf 2 1 (11)^1 A> 0 (22)^3a+5 2 1^b-3 S

20. 0^inf 2 1 (11)^a A> 0 (22)^1 1^b S --> 0^inf 2 1 (11)^g_3(a) A> 0 (22)^1 1^b-4 S
by:
0^inf 2 1 (11)^a A> 0 (22)^1 1^b S
--> 0^inf 2 1 (11)^g_2(a) A> 2 1^b-1 S by rule 18
--> 0^inf 2 1 (11)^1 A> 0 (22)^3*g_2(a)+5 2 1^b-4 S by rule 19
= 0^inf 2 1 (11)^1 A> 0 2^6*g_2(a)+11 1^b-4 S
Modulus for rule 14:
6*g_2(a)+11 = 3(2*g_2(a)+3)+2 = 3k+2
3k+2 mod 3 = 2
--> 0^inf 2 1 (11)^(g_2)^(2*g_2(a)+3)(1) A> 0 (22)^1 1^b-4 S
= 0^inf 2 1 (11)^g_3(a) A> 0 (22)^1 1^b-4 S

21. 0^inf 2 1 (11)^a A> 0 (22)^1 1^4k+v S --> 0^inf 2 1 (11)^g_3^k(a) A> 0 (22)^1 1^v S
by repetition of rule 20

22. 0^inf 2 1 (11)^a A> 0 (22)^1 1^3 2 0^inf --> 0^inf 2 1 (11)^1 A> 0 (22)^1 1^6*g_2(a)+12 2 0^inf
by:
0^inf 2 1 (11)^a A> 0 (22)^1 1^3 2 0^inf
--> 0^inf 2 1 (11)^g_2(a) A> 2 1^2 2 0^inf by rule 18
--> 0^inf 1 (11)^3*g_2(a)+5 D> 2 0^inf by rule 19*
--> 0^inf (11)^3*g_2(a)+6 D> 0^inf
--> 0^inf (11)^3*g_2(a)+6 1 A> 0^inf
--> 0^inf (11)^3*g_2(a)+7 B> 0^inf
--> 0^inf (11)^3*g_2(a)+7 <C 2 0^inf
--> 0^inf <C (11)^3*g_2(a)+7 2 0^inf
--> 0^inf 2 D> (11)^3*g_2(a)+7 2 0^inf
--> 0^inf 2 <D 2 1 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf 1 D> 2 1 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf (11)^1 D> 1 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf (11)^1 <D 2 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf <D 2^3 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf 1 A> 2^3 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf 1 <B 0 2^2 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf <A 2 0 (22)^1 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf 1 B> 2 0 (22)^1 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf 1 <A 0 0 (22)^1 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf <B 2 0 0 (22)^1 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf <C 2 2 0 0 (22)^1 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf 2 D> 2 2 0 0 (22)^1 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf 2 (11)^1 D> 0 0 (22)^1 (11)^3*g_2(a)+6 2 0^inf
--> 0^inf 2 1 (11)^1 A> 0 (22)^1 (11)^3*g_2(a)+6 2 0^inf
= 0^inf 2 1 (11)^1 A> 0 (22)^1 1^6*g_2(a)+12 2 0^inf

23. 0^inf 2 1 (11)^a A> 0 (22)^1 1^2 2 0^inf --> 0^inf 1 Z> (11)^3*g_2(a)+6 2 0^inf
by:
0^inf 2 1 (11)^a A> 0 (22)^1 1^2 2 0^inf
--> 0^inf 2 1 (11)^g_2(a) A> 2 1 2 0^inf by rule 18
--> 0^inf <B (22)^3*g_2(a)+4 2 0^inf by rule 19**
--> 0^inf <C (22)^3*g_2(a)+5 0^inf
--> 0^inf 2 D> (22)^3*g_2(a)+5 0^inf
--> 0^inf 2 (11)^3*g_2(a)+5 D> 0^inf
--> 0^inf 2 1 (11)^3*g_2(a)+5 A> 0^inf
--> 0^inf 2 (11)^3*g_2(a)+6 B> 0^inf
--> 0^inf 2 (11)^3*g_2(a)+6 <C 2 0^inf
--> 0^inf 2 <C (11)^3*g_2(a)+6 2 0^inf
--> 0^inf 1 Z> (11)^3*g_2(a)+6 2 0^inf

24. 0^inf (11)^a A> 0 (22)^1 1 2 0^inf --> 0^inf 1 Z> (11)^3*g_2(a)+5 2 0^inf
by:
0^inf (11)^a A> 0 (22)^1 1 2 0^inf
--> 0^inf 2 1 (11)^g_2(a) A> 2 2 0^inf by rule 18
--> 0^inf (11)^3*g_2(a)+3 1 B> 2 0^inf by rule 19***
--> 0^inf (11)^3*g_2(a)+3 1 <A 0^inf
--> 0^inf 1 <A (22)^3*g_2(a)+3 0^inf
--> 0^inf <B 2 (22)^3*g_2(a)+3 0^inf
--> 0^inf <C (22)^3*g_2(a)+4 0^inf
--> 0^inf 2 D> (22)^3*g_2(a)+4 0^inf
--> 0^inf 2 (11)^3*g_2(a)+4 D> 0^inf
--> 0^inf 2 1 (11)^3*g_2(a)+4 A> 0^inf
--> 0^inf 2 (11)^3*g_2(a)+5 B> 0^inf
--> 0^inf 2 (11)^3*g_2(a)+5 <C 2 0^inf
--> 0^inf 2 <C (11)^3*g_2(a)+5 2 0^inf
--> 0^inf 1 Z> (11)^3*g_2(a)+5 2 0^inf

25. 0^inf 2 1 (11)^a A> 0 (22)^1 2 0^inf --> 0^inf 1 Z> (11)^g_2(a)+1 2 0^inf
by:
0^inf 2 1 (11)^a A> 0 (22)^1 2 0^inf
--> 0^inf 2 1 (11)^g_2(a) A> 0^inf by rule 14
--> 0^inf 2 (11)^g_2(a)+1 B> 0^inf
--> 0^inf 2 (11)^g_2(a)+1 <C 2 0^inf
--> 0^inf 2 <C (11)^g_2(a)+1 2 0^inf
--> 0^inf 1 Z> (11)^g_2(a)+1 2 0^inf

Functions

$g_1(n)=3n+4$

Note that $(3^k-2)\times 3+4=3^{k+1}-2$

And $1=3^1-2$

It follows that $g_1^n(1)=3^{n+1}-2$

$g_2(n)=3^{3n+7}-2$

$g_3(n)=g_2^{2\times (g_2(n)+3)}(1)$

Modulus of g_2^a(1):

1 is of the form 4k+1
g_2(n) = 3^(3n+7)-2
3^2k mod 4 = 1
3^2k+1 mod 4 = 3

g_2(4k+1) = 3^(3*(4k+1)+7)-2 = 3^(12k+10)-2 = 3^2m-2
3^2m mod 4 = 1 --> -2
3^2m - 2 mod 4 = 3
g_2(4k+1) mod 4 = 3
--> g_2(4k+1) = 4m+3

g_2(4k+3) = 3^(3*(4k+3)+7)-2 = 3^(12k+16)-2 = 3^2m-2
3^2m-2 mod 4 = 3
g_2(4k+1) mod 4 = 3
--> g_2(4k+3) = 4m+3

-->g_2^k(1) = 4m+3
-->g_2^k(1) mod 4 = 3

Let's have L(a, b) = 0^inf 2 1 (11)^a A> 0 (22)^1 1^b 2 0^inf

* L(a, 4k+v) --> L(g_3^k(a), v) by rule 21
* L(a, 0) --> 0^inf 1 Z> (11)^g_2(a)+1 2 0^inf by rule 25
* L(a, 1) --> 0^inf 1 Z> (11)^3*g_2(a)+5 2 0^inf by rule 24
* L(a, 2) --> 0^inf 1 Z> (11)^3*g_2(a)+6 2 0^inf by rule 23
* L(a, 3) --> L(1, 6*g_2(a) + 12) by rule 22

Trajectory

S=0: 0^inf <A 0^inf
S=1: 0^inf 1 B> 0^inf
S=2: 0^inf 1 <C 2 0^inf
S=3: 0^inf <C 1 2 0^inf
S=4: 0^inf 2 D> 1 2 0^inf
S=5: 0^inf 2 <D 2^2 0^inf
S=6: 0^inf 1 D> 2^2 0^inf
S=8: 0^inf 1^3 D> 0^inf
S=9: 0^inf (11)^2 A> 0^inf
S=10: 0^inf (11)^2 1 B> 0^inf
S=11: 0^inf (11)^2 1 <C 2 0^inf
S=16: 0^inf <C (11)^2 1 2 0^inf
S=17: 0^inf 2 D> (11)^2 1 2 0^inf
S=18: 0^inf 2 <D 2 (11)^2 2 0^inf
S=19: 0^inf 1 D> 2 (11)^2 2 0^inf
S=20: 0^inf (11)^1 D> (11)^2 2 0^inf
S=21: 0^inf (11)^1 <D 2 1 (11)^1 2 0^inf
S=23: 0^inf <D 2^3 1^3 2 0^inf
S=24: 0^inf 1 A> 2^3 1^3 2 0^inf
S=25: 0^inf 1 <B 0 2^2 1^3 2 0^inf
S=26: 0^inf <A 2 0 2^2 1^3 2 0^inf
S=27: 0^inf 1 B> 2 0 2^2 1^3 2 0^inf
S=28: 0^inf 1 <A 0 0 2^2 1^3 2 0^inf
S=29: 0^inf <B 2 0 0 2^2 1^3 2 0^inf
S=30: 0^inf <C 2 2 0 0 2^2 1^3 2 0^inf
S=31: 0^inf 2 D> 2^2 0 0 2^2 1^3 2 0^inf
S=33: 0^inf 2 (11)^1 D> 0^2 2^2 1^3 2 0^inf
S=34: 0^inf 2 1 (11)^1 A> 0 (22)^1 1^3 2 0^inf
= L(1, 3) after 34 steps

L(1, 3) --> $L(1,6*g_2(1)+12)$ by rule 22, which can be simplified to L(1, 354294)

--> $L(g_3^{88573}(1),2)$

$L(g_3^{88573}(1),2)$ --> 0^inf 1 Z> $(11{)}^{3\times (g_2(g_3^{88573}(1))+6}$ 2 0^inf

$\sigma =6\times g_2(g_3^{88573}(1))+14$

Approximate Score

$g_2(n)=3^{3n+7}-2$

$3^n<g_2(n)<3^{3^n}$

$g_3(n)=g_2^{2\times (g_2(n))+3}(1)$

$(3\uparrow {)}^{k}n<g_2^k(n)<(3\uparrow {)}^{2k}n$

$(3\uparrow {)}^{k}1<g_2^k(1)<(3\uparrow {)}^{2k}1$

$3\uparrow \uparrow k<g_2^k(1)<3\uparrow \uparrow 2k$

$3\uparrow \uparrow 2\times g_2(n)+6<g_3(n)<3\uparrow \uparrow 4\times g_2(n)+12$

$3\uparrow \uparrow 2\times 3^{3\uparrow \uparrow 2\times g_2(n)+6}+6<g_3^2(n)$

$3\uparrow \uparrow 3\uparrow \uparrow (2\times g_2(n)+7)<g_3^2(n)<3\uparrow \uparrow 3\uparrow \uparrow (4\times g_2(n)+13)$

$(3\uparrow \uparrow {)}^k(2\times g_2(n)+7)<g_3^k(n)<(3\uparrow \uparrow {)}^k(5\times g_2(n)+13)$

$(3\uparrow \uparrow {)}^{k}118101<g_3^k(1)<(3\uparrow \uparrow {)}^{k}295248$

$3\uparrow \uparrow \uparrow k+1<g_3^k(1)<3\uparrow \uparrow \uparrow k+2$

$\sigma =6\times g_2(g_3^{88573}(1))+14$

$3\uparrow \uparrow \uparrow 88574<\sigma <S<3\uparrow \uparrow \uparrow 88575$