Comment: This TM produces 64'665 nonzeros in 4'561'535'055 steps.
| State | on 0 |
on 1 |
on 2 |
on 3 |
on 4 |
on 0 | on 1 | on 2 | on 3 | on 4 | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | Move | Goto | Move | Goto | |||||||||||
| A | B1R | B2R | A3L | A2R | A3R | 1 | right | B | 2 | right | B | 3 | left | A | 2 | right | A | 3 | right | A |
| B | B2L | A2L | A1L | B4R | Z1R | 2 | left | B | 2 | left | A | 1 | left | A | 4 | right | B | 1 | right | Z |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 1-bck-macro machine.
Simulation is done as 1-bck-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 1.
Pushing BCK machine.
Steps BasSteps BasTpos Tape contents
0 0 0 (0)A>
1 1 1 (1)B>
2 3 -1 <A(2) 2
3 8 -2 <A(3) 22
4 10 0 1 (4)B> 22
5 13 1 1 3 (2)B> 2
6 15 -1 1 3 <A(3) 1
7 17 1 1 2 (2)A> 1
8 18 2 1 22 (2)B>
9 20 0 1 22 <A(1) 2
10 21 -1 1 2 <A(3) 1 2
11 22 -2 1 <A(3) 3 1 2
12 24 0 2 (4)B> 3 1 2
13 25 1 2 4 (4)B> 1 2
14 30 2 2 4 2 (2)A> 2
15 32 0 2 4 2 <A(3) 3
16 33 -1 2 4 <A(3) 32
17 35 1 2 3 (2)A> 32
18 37 3 2 3 22 (2)A>
19 38 4 2 3 23 (1)B>
20 40 2 2 3 23 <A(2) 2
21 41 1 2 3 22 <A(3) 22
22 43 -1 2 3 <A(3) 32 22
23 45 1 22 (2)A> 32 22
24 47 3 24 (2)A> 22
25 49 1 24 <A(3) 3 2
26 53 -3 <A(3) 35 2
27 55 -1 1 (4)B> 35 2
28 60 4 1 45 (4)B> 2
29 63 5 1 45 3 (2)B>
30 65 3 1 45 3 <A(1) 2
31 67 5 1 45 2 (2)B> 2
32 69 3 1 45 2 <A(3) 1
33 70 2 1 45 <A(3) 3 1
34 72 4 1 44 3 (2)A> 3 1
35 73 5 1 44 3 2 (2)A> 1
36 74 6 1 44 3 22 (2)B>
37 76 4 1 44 3 22 <A(1) 2
38 77 3 1 44 3 2 <A(3) 1 2
39 78 2 1 44 3 <A(3) 3 1 2
40 80 4 1 44 2 (2)A> 3 1 2
41 81 5 1 44 22 (2)A> 1 2
42 82 6 1 44 23 (2)B> 2
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 42+V(2) 21+V(1) (2)B> 2
1 2 -2 [*]* 42+V(2) 21+V(1) <A(3) 1
2 3+V(1) -3+-1*V(1) [*]* 42+V(2) <A(3) 31+V(1) 1
3 5+V(1) -1+-1*V(1) [*]* 41+V(2) 3 (2)A> 31+V(1) 1
4 6+2*V(1) 0 [*]* 41+V(2) 3 21+V(1) (2)A> 1
5 7+2*V(1) 1 [*]* 41+V(2) 3 22+V(1) (2)B>
6 9+2*V(1) -1 [*]* 41+V(2) 3 22+V(1) <A(1) 2
7 10+2*V(1) -2 [*]* 41+V(2) 3 21+V(1) <A(3) 1 2
8 11+3*V(1) -3+-1*V(1) [*]* 41+V(2) 3 <A(3) 31+V(1) 1 2
9 13+3*V(1) -1+-1*V(1) [*]* 41+V(2) 2 (2)A> 31+V(1) 1 2
10 14+4*V(1) 0 [*]* 41+V(2) 22+V(1) (2)A> 1 2
11 15+4*V(1) 1 [*]* 41+V(2) 23+V(1) (2)B> 2
<< Success! ==> defined new CTR 1 (PA)
42 82 6 1 44 23 (2)B> 2
== Executing PA-CTR 1, V(1)=2, V(2)=2, repcount=3, factor=2/1
75 175 9 1 4 29 (2)B> 2
76 177 7 1 4 29 <A(3) 1
77 186 -2 1 4 <A(3) 39 1
78 188 0 1 3 (2)A> 39 1
79 197 9 1 3 29 (2)A> 1
80 198 10 1 3 210 (2)B>
81 200 8 1 3 210 <A(1) 2
82 201 7 1 3 29 <A(3) 1 2
83 210 -2 1 3 <A(3) 39 1 2
84 212 0 1 2 (2)A> 39 1 2
85 221 9 1 210 (2)A> 1 2
86 222 10 1 211 (2)B> 2
87 224 8 1 211 <A(3) 1
88 235 -3 1 <A(3) 311 1
89 237 -1 2 (4)B> 311 1
90 248 10 2 411 (4)B> 1
91 253 11 2 411 2 (2)A>
92 254 12 2 411 22 (1)B>
93 256 10 2 411 22 <A(2) 2
94 257 9 2 411 2 <A(3) 22
95 258 8 2 411 <A(3) 3 22
96 260 10 2 410 3 (2)A> 3 22
97 261 11 2 410 3 2 (2)A> 22
98 263 9 2 410 3 2 <A(3) 3 2
99 264 8 2 410 3 <A(3) 32 2
100 266 10 2 410 2 (2)A> 32 2
101 268 12 2 410 23 (2)A> 2
102 270 10 2 410 23 <A(3) 3
103 273 7 2 410 <A(3) 34
104 275 9 2 49 3 (2)A> 34
105 279 13 2 49 3 24 (2)A>
106 280 14 2 49 3 25 (1)B>
107 282 12 2 49 3 25 <A(2) 2
108 283 11 2 49 3 24 <A(3) 22
109 287 7 2 49 3 <A(3) 34 22
110 289 9 2 49 2 (2)A> 34 22
111 293 13 2 49 25 (2)A> 22
112 295 11 2 49 25 <A(3) 3 2
113 300 6 2 49 <A(3) 36 2
114 302 8 2 48 3 (2)A> 36 2
115 308 14 2 48 3 26 (2)A> 2
116 310 12 2 48 3 26 <A(3) 3
117 316 6 2 48 3 <A(3) 37
118 318 8 2 48 2 (2)A> 37
119 325 15 2 48 28 (2)A>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 44+V(2) 21+V(1) (2)A>
1 1 1 [*]* 44+V(2) 22+V(1) (1)B>
2 3 -1 [*]* 44+V(2) 22+V(1) <A(2) 2
3 4 -2 [*]* 44+V(2) 21+V(1) <A(3) 22
4 5+V(1) -3+-1*V(1) [*]* 44+V(2) <A(3) 31+V(1) 22
5 7+V(1) -1+-1*V(1) [*]* 43+V(2) 3 (2)A> 31+V(1) 22
6 8+2*V(1) 0 [*]* 43+V(2) 3 21+V(1) (2)A> 22
7 10+2*V(1) -2 [*]* 43+V(2) 3 21+V(1) <A(3) 3 2
8 11+3*V(1) -3+-1*V(1) [*]* 43+V(2) 3 <A(3) 32+V(1) 2
9 13+3*V(1) -1+-1*V(1) [*]* 43+V(2) 2 (2)A> 32+V(1) 2
10 15+4*V(1) 1 [*]* 43+V(2) 23+V(1) (2)A> 2
11 17+4*V(1) -1 [*]* 43+V(2) 23+V(1) <A(3) 3
12 20+5*V(1) -4+-1*V(1) [*]* 43+V(2) <A(3) 34+V(1)
13 22+5*V(1) -2+-1*V(1) [*]* 42+V(2) 3 (2)A> 34+V(1)
14 26+6*V(1) 2 [*]* 42+V(2) 3 24+V(1) (2)A>
15 27+6*V(1) 3 [*]* 42+V(2) 3 25+V(1) (1)B>
16 29+6*V(1) 1 [*]* 42+V(2) 3 25+V(1) <A(2) 2
17 30+6*V(1) 0 [*]* 42+V(2) 3 24+V(1) <A(3) 22
18 34+7*V(1) -4+-1*V(1) [*]* 42+V(2) 3 <A(3) 34+V(1) 22
19 36+7*V(1) -2+-1*V(1) [*]* 42+V(2) 2 (2)A> 34+V(1) 22
20 40+8*V(1) 2 [*]* 42+V(2) 25+V(1) (2)A> 22
21 42+8*V(1) 0 [*]* 42+V(2) 25+V(1) <A(3) 3 2
22 47+9*V(1) -5+-1*V(1) [*]* 42+V(2) <A(3) 36+V(1) 2
23 49+9*V(1) -3+-1*V(1) [*]* 41+V(2) 3 (2)A> 36+V(1) 2
24 55+10*V(1) 3 [*]* 41+V(2) 3 26+V(1) (2)A> 2
25 57+10*V(1) 1 [*]* 41+V(2) 3 26+V(1) <A(3) 3
26 63+11*V(1) -5+-1*V(1) [*]* 41+V(2) 3 <A(3) 37+V(1)
27 65+11*V(1) -3+-1*V(1) [*]* 41+V(2) 2 (2)A> 37+V(1)
28 72+12*V(1) 4 [*]* 41+V(2) 28+V(1) (2)A>
<< Success! ==> defined new CTR 2 (PA)
119 325 15 2 48 28 (2)A>
== Executing PA-CTR 2, V(1)=7, V(2)=4, repcount=2, factor=7/3
175 721 23 2 42 222 (2)A>
176 722 24 2 42 223 (1)B>
177 724 22 2 42 223 <A(2) 2
178 725 21 2 42 222 <A(3) 22
179 747 -1 2 42 <A(3) 322 22
180 749 1 2 4 3 (2)A> 322 22
181 771 23 2 4 3 222 (2)A> 22
182 773 21 2 4 3 222 <A(3) 3 2
183 795 -1 2 4 3 <A(3) 323 2
184 797 1 2 4 2 (2)A> 323 2
185 820 24 2 4 224 (2)A> 2
186 822 22 2 4 224 <A(3) 3
187 846 -2 2 4 <A(3) 325
188 848 0 2 3 (2)A> 325
189 873 25 2 3 225 (2)A>
190 874 26 2 3 226 (1)B>
191 876 24 2 3 226 <A(2) 2
192 877 23 2 3 225 <A(3) 22
193 902 -2 2 3 <A(3) 325 22
194 904 0 22 (2)A> 325 22
195 929 25 227 (2)A> 22
196 931 23 227 <A(3) 3 2
197 958 -4 <A(3) 328 2
198 960 -2 1 (4)B> 328 2
199 988 26 1 428 (4)B> 2
200 991 27 1 428 3 (2)B>
201 993 25 1 428 3 <A(1) 2
202 995 27 1 428 2 (2)B> 2
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 21+V(2) 42 21+V(1) (2)A>
1 1 1 21+V(2) 42 22+V(1) (1)B>
2 3 -1 21+V(2) 42 22+V(1) <A(2) 2
3 4 -2 21+V(2) 42 21+V(1) <A(3) 22
4 5+V(1) -3+-1*V(1) 21+V(2) 42 <A(3) 31+V(1) 22
5 7+V(1) -1+-1*V(1) 21+V(2) 4 3 (2)A> 31+V(1) 22
6 8+2*V(1) 0 21+V(2) 4 3 21+V(1) (2)A> 22
7 10+2*V(1) -2 21+V(2) 4 3 21+V(1) <A(3) 3 2
8 11+3*V(1) -3+-1*V(1) 21+V(2) 4 3 <A(3) 32+V(1) 2
9 13+3*V(1) -1+-1*V(1) 21+V(2) 4 2 (2)A> 32+V(1) 2
10 15+4*V(1) 1 21+V(2) 4 23+V(1) (2)A> 2
11 17+4*V(1) -1 21+V(2) 4 23+V(1) <A(3) 3
12 20+5*V(1) -4+-1*V(1) 21+V(2) 4 <A(3) 34+V(1)
13 22+5*V(1) -2+-1*V(1) 21+V(2) 3 (2)A> 34+V(1)
14 26+6*V(1) 2 21+V(2) 3 24+V(1) (2)A>
15 27+6*V(1) 3 21+V(2) 3 25+V(1) (1)B>
16 29+6*V(1) 1 21+V(2) 3 25+V(1) <A(2) 2
17 30+6*V(1) 0 21+V(2) 3 24+V(1) <A(3) 22
18 34+7*V(1) -4+-1*V(1) 21+V(2) 3 <A(3) 34+V(1) 22
19 36+7*V(1) -2+-1*V(1) 22+V(2) (2)A> 34+V(1) 22
20 40+8*V(1) 2 26+V(1)+V(2) (2)A> 22
21 42+8*V(1) 0 26+V(1)+V(2) <A(3) 3 2
22 48+9*V(1)+V(2) -6+-1*V(1)+-1*V(2) <A(3) 37+V(1)+V(2) 2
23 50+9*V(1)+V(2) -4+-1*V(1)+-1*V(2) 1 (4)B> 37+V(1)+V(2) 2
24 57+10*V(1)+2*V(2) 3 1 47+V(1)+V(2) (4)B> 2
25 60+10*V(1)+2*V(2) 4 1 47+V(1)+V(2) 3 (2)B>
26 62+10*V(1)+2*V(2) 2 1 47+V(1)+V(2) 3 <A(1) 2
27 64+10*V(1)+2*V(2) 4 1 47+V(1)+V(2) 2 (2)B> 2
<< Success! ==> defined new CTR 3 (PPA)
202 995 27 1 428 2 (2)B> 2
== Executing PA-CTR 1, V(1)=0, V(2)=26, repcount=27, factor=2/1
499 4208 54 1 4 255 (2)B> 2
500 4210 52 1 4 255 <A(3) 1
501 4265 -3 1 4 <A(3) 355 1
502 4267 -1 1 3 (2)A> 355 1
503 4322 54 1 3 255 (2)A> 1
504 4323 55 1 3 256 (2)B>
505 4325 53 1 3 256 <A(1) 2
506 4326 52 1 3 255 <A(3) 1 2
507 4381 -3 1 3 <A(3) 355 1 2
508 4383 -1 1 2 (2)A> 355 1 2
509 4438 54 1 256 (2)A> 1 2
510 4439 55 1 257 (2)B> 2
511 4441 53 1 257 <A(3) 1
512 4498 -4 1 <A(3) 357 1
513 4500 -2 2 (4)B> 357 1
514 4557 55 2 457 (4)B> 1
515 4562 56 2 457 2 (2)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 1 4 22+V(1) (2)B> 2
1 2 -2 1 4 22+V(1) <A(3) 1
2 4+V(1) -4+-1*V(1) 1 4 <A(3) 32+V(1) 1
3 6+V(1) -2+-1*V(1) 1 3 (2)A> 32+V(1) 1
4 8+2*V(1) 0 1 3 22+V(1) (2)A> 1
5 9+2*V(1) 1 1 3 23+V(1) (2)B>
6 11+2*V(1) -1 1 3 23+V(1) <A(1) 2
7 12+2*V(1) -2 1 3 22+V(1) <A(3) 1 2
8 14+3*V(1) -4+-1*V(1) 1 3 <A(3) 32+V(1) 1 2
9 16+3*V(1) -2+-1*V(1) 1 2 (2)A> 32+V(1) 1 2
10 18+4*V(1) 0 1 23+V(1) (2)A> 1 2
11 19+4*V(1) 1 1 24+V(1) (2)B> 2
12 21+4*V(1) -1 1 24+V(1) <A(3) 1
13 25+5*V(1) -5+-1*V(1) 1 <A(3) 34+V(1) 1
14 27+5*V(1) -3+-1*V(1) 2 (4)B> 34+V(1) 1
15 31+6*V(1) 1 2 44+V(1) (4)B> 1
16 36+6*V(1) 2 2 44+V(1) 2 (2)A>
<< Success! ==> defined new CTR 4 (PPA)
515 4562 56 2 457 2 (2)A>
== Executing PA-CTR 2, V(1)=0, V(2)=53, repcount=18, factor=7/3
1019 18710 128 2 43 2127 (2)A>
1020 18711 129 2 43 2128 (1)B>
1021 18713 127 2 43 2128 <A(2) 2
1022 18714 126 2 43 2127 <A(3) 22
1023 18841 -1 2 43 <A(3) 3127 22
1024 18843 1 2 42 3 (2)A> 3127 22
1025 18970 128 2 42 3 2127 (2)A> 22
1026 18972 126 2 42 3 2127 <A(3) 3 2
1027 19099 -1 2 42 3 <A(3) 3128 2
1028 19101 1 2 42 2 (2)A> 3128 2
1029 19229 129 2 42 2129 (2)A> 2
1030 19231 127 2 42 2129 <A(3) 3
1031 19360 -2 2 42 <A(3) 3130
1032 19362 0 2 4 3 (2)A> 3130
1033 19492 130 2 4 3 2130 (2)A>
1034 19493 131 2 4 3 2131 (1)B>
1035 19495 129 2 4 3 2131 <A(2) 2
1036 19496 128 2 4 3 2130 <A(3) 22
1037 19626 -2 2 4 3 <A(3) 3130 22
1038 19628 0 2 4 2 (2)A> 3130 22
1039 19758 130 2 4 2131 (2)A> 22
1040 19760 128 2 4 2131 <A(3) 3 2
1041 19891 -3 2 4 <A(3) 3132 2
1042 19893 -1 2 3 (2)A> 3132 2
1043 20025 131 2 3 2132 (2)A> 2
1044 20027 129 2 3 2132 <A(3) 3
1045 20159 -3 2 3 <A(3) 3133
1046 20161 -1 22 (2)A> 3133
1047 20294 132 2135 (2)A>
1048 20295 133 2136 (1)B>
1049 20297 131 2136 <A(2) 2
1050 20298 130 2135 <A(3) 22
1051 20433 -5 <A(3) 3135 22
1052 20435 -3 1 (4)B> 3135 22
1053 20570 132 1 4135 (4)B> 22
1054 20573 133 1 4135 3 (2)B> 2
1055 20575 131 1 4135 3 <A(3) 1
1056 20577 133 1 4135 2 (2)A> 1
1057 20578 134 1 4135 22 (2)B>
1058 20580 132 1 4135 22 <A(1) 2
1059 20581 131 1 4135 2 <A(3) 1 2
1060 20582 130 1 4135 <A(3) 3 1 2
1061 20584 132 1 4134 3 (2)A> 3 1 2
1062 20585 133 1 4134 3 2 (2)A> 1 2
1063 20586 134 1 4134 3 22 (2)B> 2
1064 20588 132 1 4134 3 22 <A(3) 1
1065 20590 130 1 4134 3 <A(3) 32 1
1066 20592 132 1 4134 2 (2)A> 32 1
1067 20594 134 1 4134 23 (2)A> 1
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 42+V(2) 21+V(1) (2)A> 1
1 1 1 [*]* 42+V(2) 22+V(1) (2)B>
2 3 -1 [*]* 42+V(2) 22+V(1) <A(1) 2
3 4 -2 [*]* 42+V(2) 21+V(1) <A(3) 1 2
4 5+V(1) -3+-1*V(1) [*]* 42+V(2) <A(3) 31+V(1) 1 2
5 7+V(1) -1+-1*V(1) [*]* 41+V(2) 3 (2)A> 31+V(1) 1 2
6 8+2*V(1) 0 [*]* 41+V(2) 3 21+V(1) (2)A> 1 2
7 9+2*V(1) 1 [*]* 41+V(2) 3 22+V(1) (2)B> 2
8 11+2*V(1) -1 [*]* 41+V(2) 3 22+V(1) <A(3) 1
9 13+3*V(1) -3+-1*V(1) [*]* 41+V(2) 3 <A(3) 32+V(1) 1
10 15+3*V(1) -1+-1*V(1) [*]* 41+V(2) 2 (2)A> 32+V(1) 1
11 17+4*V(1) 1 [*]* 41+V(2) 23+V(1) (2)A> 1
<< Success! ==> defined new CTR 5 (PA)
1067 20594 134 1 4134 23 (2)A> 1
== Executing PA-CTR 5, V(1)=2, V(2)=132, repcount=133, factor=2/1
2530 94143 267 1 4 2269 (2)A> 1
2531 94144 268 1 4 2270 (2)B>
2532 94146 266 1 4 2270 <A(1) 2
2533 94147 265 1 4 2269 <A(3) 1 2
2534 94416 -4 1 4 <A(3) 3269 1 2
2535 94418 -2 1 3 (2)A> 3269 1 2
2536 94687 267 1 3 2269 (2)A> 1 2
2537 94688 268 1 3 2270 (2)B> 2
2538 94690 266 1 3 2270 <A(3) 1
2539 94960 -4 1 3 <A(3) 3270 1
2540 94962 -2 1 2 (2)A> 3270 1
2541 95232 268 1 2271 (2)A> 1
2542 95233 269 1 2272 (2)B>
2543 95235 267 1 2272 <A(1) 2
2544 95236 266 1 2271 <A(3) 1 2
2545 95507 -5 1 <A(3) 3271 1 2
2546 95509 -3 2 (4)B> 3271 1 2
2547 95780 268 2 4271 (4)B> 1 2
2548 95785 269 2 4271 2 (2)A> 2
2549 95787 267 2 4271 2 <A(3) 3
2550 95788 266 2 4271 <A(3) 32
2551 95790 268 2 4270 3 (2)A> 32
2552 95792 270 2 4270 3 22 (2)A>
2553 95793 271 2 4270 3 23 (1)B>
2554 95795 269 2 4270 3 23 <A(2) 2
2555 95796 268 2 4270 3 22 <A(3) 22
2556 95798 266 2 4270 3 <A(3) 32 22
2557 95800 268 2 4270 2 (2)A> 32 22
2558 95802 270 2 4270 23 (2)A> 22
2559 95804 268 2 4270 23 <A(3) 3 2
2560 95807 265 2 4270 <A(3) 34 2
2561 95809 267 2 4269 3 (2)A> 34 2
2562 95813 271 2 4269 3 24 (2)A> 2
2563 95815 269 2 4269 3 24 <A(3) 3
2564 95819 265 2 4269 3 <A(3) 35
2565 95821 267 2 4269 2 (2)A> 35
2566 95826 272 2 4269 26 (2)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 1 4 24+V(1) (2)A> 1
1 1 1 1 4 25+V(1) (2)B>
2 3 -1 1 4 25+V(1) <A(1) 2
3 4 -2 1 4 24+V(1) <A(3) 1 2
4 8+V(1) -6+-1*V(1) 1 4 <A(3) 34+V(1) 1 2
5 10+V(1) -4+-1*V(1) 1 3 (2)A> 34+V(1) 1 2
6 14+2*V(1) 0 1 3 24+V(1) (2)A> 1 2
7 15+2*V(1) 1 1 3 25+V(1) (2)B> 2
8 17+2*V(1) -1 1 3 25+V(1) <A(3) 1
9 22+3*V(1) -6+-1*V(1) 1 3 <A(3) 35+V(1) 1
10 24+3*V(1) -4+-1*V(1) 1 2 (2)A> 35+V(1) 1
11 29+4*V(1) 1 1 26+V(1) (2)A> 1
12 30+4*V(1) 2 1 27+V(1) (2)B>
13 32+4*V(1) 0 1 27+V(1) <A(1) 2
14 33+4*V(1) -1 1 26+V(1) <A(3) 1 2
15 39+5*V(1) -7+-1*V(1) 1 <A(3) 36+V(1) 1 2
16 41+5*V(1) -5+-1*V(1) 2 (4)B> 36+V(1) 1 2
17 47+6*V(1) 1 2 46+V(1) (4)B> 1 2
18 52+6*V(1) 2 2 46+V(1) 2 (2)A> 2
19 54+6*V(1) 0 2 46+V(1) 2 <A(3) 3
20 55+6*V(1) -1 2 46+V(1) <A(3) 32
21 57+6*V(1) 1 2 45+V(1) 3 (2)A> 32
22 59+6*V(1) 3 2 45+V(1) 3 22 (2)A>
23 60+6*V(1) 4 2 45+V(1) 3 23 (1)B>
24 62+6*V(1) 2 2 45+V(1) 3 23 <A(2) 2
25 63+6*V(1) 1 2 45+V(1) 3 22 <A(3) 22
26 65+6*V(1) -1 2 45+V(1) 3 <A(3) 32 22
27 67+6*V(1) 1 2 45+V(1) 2 (2)A> 32 22
28 69+6*V(1) 3 2 45+V(1) 23 (2)A> 22
29 71+6*V(1) 1 2 45+V(1) 23 <A(3) 3 2
30 74+6*V(1) -2 2 45+V(1) <A(3) 34 2
31 76+6*V(1) 0 2 44+V(1) 3 (2)A> 34 2
32 80+6*V(1) 4 2 44+V(1) 3 24 (2)A> 2
33 82+6*V(1) 2 2 44+V(1) 3 24 <A(3) 3
34 86+6*V(1) -2 2 44+V(1) 3 <A(3) 35
35 88+6*V(1) 0 2 44+V(1) 2 (2)A> 35
36 93+6*V(1) 5 2 44+V(1) 26 (2)A>
<< Success! ==> defined new CTR 6 (PPA)
2566 95826 272 2 4269 26 (2)A>
== Executing PA-CTR 2, V(1)=5, V(2)=265, repcount=89, factor=7/3
5058 436518 628 2 42 2629 (2)A>
== Executing PPA-CTR 3 (once), V(1)=628, V(2)=0
5085 442862 632 1 4635 2 (2)B> 2
== Executing PA-CTR 1, V(1)=0, V(2)=633, repcount=634, factor=2/1
12059 2057660 1266 1 4 21269 (2)B> 2
== Executing PPA-CTR 4 (once), V(1)=1267
12075 2065298 1268 2 41271 2 (2)A>
== Executing PA-CTR 2, V(1)=0, V(2)=1267, repcount=423, factor=7/3
23919 9593006 2960 2 42 22962 (2)A>
== Executing PPA-CTR 3 (once), V(1)=2961, V(2)=0
23946 9622680 2964 1 42968 2 (2)B> 2
== Executing PA-CTR 1, V(1)=0, V(2)=2966, repcount=2967, factor=2/1
56583 44867673 5931 1 4 25935 (2)B> 2
== Executing PPA-CTR 4 (once), V(1)=5933
56599 44903307 5933 2 45937 2 (2)A>
== Executing PA-CTR 2, V(1)=0, V(2)=5933, repcount=1978, factor=7/3
111983 209286975 13845 2 43 213847 (2)A>
111984 209286976 13846 2 43 213848 (1)B>
111985 209286978 13844 2 43 213848 <A(2) 2
111986 209286979 13843 2 43 213847 <A(3) 22
111987 209300826 -4 2 43 <A(3) 313847 22
111988 209300828 -2 2 42 3 (2)A> 313847 22
111989 209314675 13845 2 42 3 213847 (2)A> 22
111990 209314677 13843 2 42 3 213847 <A(3) 3 2
111991 209328524 -4 2 42 3 <A(3) 313848 2
111992 209328526 -2 2 42 2 (2)A> 313848 2
111993 209342374 13846 2 42 213849 (2)A> 2
111994 209342376 13844 2 42 213849 <A(3) 3
111995 209356225 -5 2 42 <A(3) 313850
111996 209356227 -3 2 4 3 (2)A> 313850
111997 209370077 13847 2 4 3 213850 (2)A>
111998 209370078 13848 2 4 3 213851 (1)B>
111999 209370080 13846 2 4 3 213851 <A(2) 2
112000 209370081 13845 2 4 3 213850 <A(3) 22
112001 209383931 -5 2 4 3 <A(3) 313850 22
112002 209383933 -3 2 4 2 (2)A> 313850 22
112003 209397783 13847 2 4 213851 (2)A> 22
112004 209397785 13845 2 4 213851 <A(3) 3 2
112005 209411636 -6 2 4 <A(3) 313852 2
112006 209411638 -4 2 3 (2)A> 313852 2
112007 209425490 13848 2 3 213852 (2)A> 2
112008 209425492 13846 2 3 213852 <A(3) 3
112009 209439344 -6 2 3 <A(3) 313853
112010 209439346 -4 22 (2)A> 313853
112011 209453199 13849 213855 (2)A>
112012 209453200 13850 213856 (1)B>
112013 209453202 13848 213856 <A(2) 2
112014 209453203 13847 213855 <A(3) 22
112015 209467058 -8 <A(3) 313855 22
112016 209467060 -6 1 (4)B> 313855 22
112017 209480915 13849 1 413855 (4)B> 22
112018 209480918 13850 1 413855 3 (2)B> 2
112019 209480920 13848 1 413855 3 <A(3) 1
112020 209480922 13850 1 413855 2 (2)A> 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 21+V(2) 43 21+V(1) (2)A>
1 1 1 21+V(2) 43 22+V(1) (1)B>
2 3 -1 21+V(2) 43 22+V(1) <A(2) 2
3 4 -2 21+V(2) 43 21+V(1) <A(3) 22
4 5+V(1) -3+-1*V(1) 21+V(2) 43 <A(3) 31+V(1) 22
5 7+V(1) -1+-1*V(1) 21+V(2) 42 3 (2)A> 31+V(1) 22
6 8+2*V(1) 0 21+V(2) 42 3 21+V(1) (2)A> 22
7 10+2*V(1) -2 21+V(2) 42 3 21+V(1) <A(3) 3 2
8 11+3*V(1) -3+-1*V(1) 21+V(2) 42 3 <A(3) 32+V(1) 2
9 13+3*V(1) -1+-1*V(1) 21+V(2) 42 2 (2)A> 32+V(1) 2
10 15+4*V(1) 1 21+V(2) 42 23+V(1) (2)A> 2
11 17+4*V(1) -1 21+V(2) 42 23+V(1) <A(3) 3
12 20+5*V(1) -4+-1*V(1) 21+V(2) 42 <A(3) 34+V(1)
13 22+5*V(1) -2+-1*V(1) 21+V(2) 4 3 (2)A> 34+V(1)
14 26+6*V(1) 2 21+V(2) 4 3 24+V(1) (2)A>
15 27+6*V(1) 3 21+V(2) 4 3 25+V(1) (1)B>
16 29+6*V(1) 1 21+V(2) 4 3 25+V(1) <A(2) 2
17 30+6*V(1) 0 21+V(2) 4 3 24+V(1) <A(3) 22
18 34+7*V(1) -4+-1*V(1) 21+V(2) 4 3 <A(3) 34+V(1) 22
19 36+7*V(1) -2+-1*V(1) 21+V(2) 4 2 (2)A> 34+V(1) 22
20 40+8*V(1) 2 21+V(2) 4 25+V(1) (2)A> 22
21 42+8*V(1) 0 21+V(2) 4 25+V(1) <A(3) 3 2
22 47+9*V(1) -5+-1*V(1) 21+V(2) 4 <A(3) 36+V(1) 2
23 49+9*V(1) -3+-1*V(1) 21+V(2) 3 (2)A> 36+V(1) 2
24 55+10*V(1) 3 21+V(2) 3 26+V(1) (2)A> 2
25 57+10*V(1) 1 21+V(2) 3 26+V(1) <A(3) 3
26 63+11*V(1) -5+-1*V(1) 21+V(2) 3 <A(3) 37+V(1)
27 65+11*V(1) -3+-1*V(1) 22+V(2) (2)A> 37+V(1)
28 72+12*V(1) 4 29+V(1)+V(2) (2)A>
29 73+12*V(1) 5 210+V(1)+V(2) (1)B>
30 75+12*V(1) 3 210+V(1)+V(2) <A(2) 2
31 76+12*V(1) 2 29+V(1)+V(2) <A(3) 22
32 85+13*V(1)+V(2) -7+-1*V(1)+-1*V(2) <A(3) 39+V(1)+V(2) 22
33 87+13*V(1)+V(2) -5+-1*V(1)+-1*V(2) 1 (4)B> 39+V(1)+V(2) 22
34 96+14*V(1)+2*V(2) 4 1 49+V(1)+V(2) (4)B> 22
35 99+14*V(1)+2*V(2) 5 1 49+V(1)+V(2) 3 (2)B> 2
36 101+14*V(1)+2*V(2) 3 1 49+V(1)+V(2) 3 <A(3) 1
37 103+14*V(1)+2*V(2) 5 1 49+V(1)+V(2) 2 (2)A> 1
<< Success! ==> defined new CTR 7 (PPA)
112020 209480922 13850 1 413855 2 (2)A> 1
== Executing PA-CTR 5, V(1)=0, V(2)=13853, repcount=13854, factor=2/1
264414 977394288 27704 1 4 227709 (2)A> 1
== Executing PPA-CTR 6 (once), V(1)=27705
264450 977560611 27709 2 427709 26 (2)A>
== Executing PA-CTR 2, V(1)=5, V(2)=27705, repcount=9236, factor=7/3
523058 4561147083 64653 2 4 264658 (2)A>
523059 4561147084 64654 2 4 264659 (1)B>
523060 4561147086 64652 2 4 264659 <A(2) 2
523061 4561147087 64651 2 4 264658 <A(3) 22
523062 4561211745 -7 2 4 <A(3) 364658 22
523063 4561211747 -5 2 3 (2)A> 364658 22
523064 4561276405 64653 2 3 264658 (2)A> 22
523065 4561276407 64651 2 3 264658 <A(3) 3 2
523066 4561341065 -7 2 3 <A(3) 364659 2
523067 4561341067 -5 22 (2)A> 364659 2
523068 4561405726 64654 264661 (2)A> 2
523069 4561405728 64652 264661 <A(3) 3
523070 4561470389 -9 <A(3) 364662
523071 4561470391 -7 1 (4)B> 364662
523072 4561535053 64655 1 464662 (4)B>
523073 4561535055 64655 1 464662 (1)Z> 2 [stop]
Lines: 283
Top steps: 282
Macro steps: 523073
Basic steps: 4561535055
Tape index: 64655
nonzeros: 64665
log10(nonzeros): 4.811
log10(steps ): 9.659
Run state: stop
Input to awk program:
gohalt 1
nbs 5
T 2-state 5-symbol TM #b (G. Lafitte & C. Papazian)
5T B1R B2R A3L A2R A3R B2L A2L A1L B4R Z1R
: 64'665 4'561'535'055
L 4
M 400
pref sim
machv Laf25_b just simple
machv Laf25_b-r with repetitions reduced
machv Laf25_b-1 with tape symbol exponents
machv Laf25_b-m as 1-bck-macro machine
machv Laf25_b-a as 1-bck-macro machine with pure additive config-TRs
iam Laf25_b-a
mtype 1 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:11:54 CEST 2010
edate Tue Jul 6 22:11:55 CEST 2010
bnspeed 1
Constructed by: $Id: tmJob.awk,v 1.34 2010/05/06 18:26:17 heiner Exp $
$Id: basics.awk,v 1.1 2010/05/06 17:24:17 heiner Exp $
$Id: htSupp.awk,v 1.14 2010/07/06 19:48:32 heiner Exp $
$Id: mmSim.awk,v 1.34 2005/01/09 22:23:28 heiner Exp $
$Id: bignum.awk,v 1.34 2010/05/06 17:58:14 heiner Exp $
$Id: varLI.awk,v 1.11 2005/01/15 21:01:29 heiner Exp $
bignum signature: LEN={S++:9 U++:9 S+:8 U+:8 S*:4 U*:4} DONT: y i o;
Start: Tue Jul 6 22:11:54 CEST 2010