Comment: This TM produces >2.2x10^2372 nonzeros in >5.9x10^4744 steps.
| State | on 0 |
on 1 |
on 2 |
on 3 |
on 0 | on 1 | on 2 | on 3 | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | Move | Goto | |||||||||
| A | 1RB | 1RA | 1LB | 1RC | 1 | right | B | 1 | right | A | 1 | left | B | 1 | right | C |
| B | 2LA | 0LB | 3LC | 1RH | 2 | left | A | 0 | left | B | 3 | left | C | 1 | right | H |
| C | 1LB | 0RC | 2RA | 2RC | 1 | left | B | 0 | right | C | 2 | right | A | 2 | right | C |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as 2-bck-macro machine.
Simulation is done as 2-bck-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing macro factor 2.
Pushing BCK machine.
Steps BasSteps BasTpos Tape contents
0 0 0 (00)A>
1 13 -3 <B(13) 11
2 20 0 02 (02)C> 11
3 22 2 022 (00)C>
4 33 -1 022 <A(21) 21
5 37 -5 <A(21) 213
6 42 -2 (20)C> 213
7 44 0 20 (21)A> 212
8 47 -3 20 <C(30) 11 21
9 49 -5 <C(31) 30 11 21
10 51 -7 <A(21) 31 30 11 21
11 56 -4 (20)C> 31 30 11 21
12 58 -2 20 (20)C> 30 11 21
13 63 -5 20 <C(31) 31 11 21
14 65 -7 <C(31) 312 11 21
15 67 -9 <A(21) 313 11 21
16 72 -6 (20)C> 313 11 21
17 78 0 203 (20)C> 11 21
18 80 2 204 (00)C> 21
19 82 4 204 00 (21)A>
20 89 1 204 00 <C(30) 01
21 91 -1 204 <A(21) 30 01
22 96 2 204 (20)C> 30 01
23 101 -1 204 <C(31) 31 01
24 109 -9 <C(31) 315 01
25 111 -11 <A(21) 316 01
26 116 -8 (20)C> 316 01
27 128 4 206 (20)C> 01
28 131 1 206 <B(12) 11
29 143 -11 <B(12) 126 11
30 150 -8 02 (02)A> 126 11
31 155 -11 02 <B(13) 01 125 11
32 157 -13 <B(13) 13 01 125 11
33 164 -10 02 (02)C> 13 01 125 11
34 166 -8 022 (02)C> 01 125 11
35 169 -11 022 <B(13) 11 125 11
36 173 -15 <B(13) 132 11 125 11
37 180 -12 02 (02)C> 132 11 125 11
38 184 -8 023 (02)C> 11 125 11
39 186 -6 024 (00)C> 125 11
40 188 -4 024 00 (02)A> 124 11
41 193 -7 024 00 <B(13) 01 123 11
42 200 -4 025 (02)C> 01 123 11
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 021+V(1) (02)C> 01 123+V(2) [*]*
1 3 -3 021+V(1) <B(13) 11 123+V(2) [*]*
2 5+2*V(1) -5+-2*V(1) <B(13) 131+V(1) 11 123+V(2) [*]*
3 12+2*V(1) -2+-2*V(1) 02 (02)C> 131+V(1) 11 123+V(2) [*]*
4 14+4*V(1) 0 022+V(1) (02)C> 11 123+V(2) [*]*
5 16+4*V(1) 2 023+V(1) (00)C> 123+V(2) [*]*
6 18+4*V(1) 4 023+V(1) 00 (02)A> 122+V(2) [*]*
7 23+4*V(1) 1 023+V(1) 00 <B(13) 01 121+V(2) [*]*
8 30+4*V(1) 4 024+V(1) (02)C> 01 121+V(2) [*]*
<< Success! ==> defined new CTR 1 (PA)
42 200 -4 025 (02)C> 01 123 11
== Executing PA-CTR 1, V(1)=4, V(2)=0, repcount=1, factor=3/2
50 246 0 028 (02)C> 01 12 11
51 249 -3 028 <B(13) 11 12 11
52 265 -19 <B(13) 138 11 12 11
53 272 -16 02 (02)C> 138 11 12 11
54 288 0 029 (02)C> 11 12 11
55 290 2 0210 (00)C> 12 11
56 292 4 0210 00 (02)A> 11
57 294 6 0210 00 02 (11)A>
58 301 3 0210 00 02 <B(00) 01
59 303 1 0210 00 <B(13) 00 01
60 310 4 0211 (02)C> 00 01
61 313 1 0211 <B(13) 10 01
62 335 -21 <B(13) 1311 10 01
63 342 -18 02 (02)C> 1311 10 01
64 364 4 0212 (02)C> 10 01
65 369 1 0212 <A(21) 21 01
66 393 -23 <A(21) 2113 01
67 398 -20 (20)C> 2113 01
68 400 -18 20 (21)A> 2112 01
69 403 -21 20 <C(30) 11 2111 01
70 405 -23 <C(31) 30 11 2111 01
71 407 -25 <A(21) 31 30 11 2111 01
72 412 -22 (20)C> 31 30 11 2111 01
73 414 -20 20 (20)C> 30 11 2111 01
74 419 -23 20 <C(31) 31 11 2111 01
75 421 -25 <C(31) 312 11 2111 01
76 423 -27 <A(21) 313 11 2111 01
77 428 -24 (20)C> 313 11 2111 01
78 434 -18 203 (20)C> 11 2111 01
79 436 -16 204 (00)C> 2111 01
80 438 -14 204 00 (21)A> 2110 01
81 441 -17 204 00 <C(30) 11 219 01
82 443 -19 204 <A(21) 30 11 219 01
83 448 -16 204 (20)C> 30 11 219 01
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 201+V(1) (20)C> 30 11 213+V(2) [*]*
1 5 -3 201+V(1) <C(31) 31 11 213+V(2) [*]*
2 7+2*V(1) -5+-2*V(1) <C(31) 312+V(1) 11 213+V(2) [*]*
3 9+2*V(1) -7+-2*V(1) <A(21) 313+V(1) 11 213+V(2) [*]*
4 14+2*V(1) -4+-2*V(1) (20)C> 313+V(1) 11 213+V(2) [*]*
5 20+4*V(1) 2 203+V(1) (20)C> 11 213+V(2) [*]*
6 22+4*V(1) 4 204+V(1) (00)C> 213+V(2) [*]*
7 24+4*V(1) 6 204+V(1) 00 (21)A> 212+V(2) [*]*
8 27+4*V(1) 3 204+V(1) 00 <C(30) 11 211+V(2) [*]*
9 29+4*V(1) 1 204+V(1) <A(21) 30 11 211+V(2) [*]*
10 34+4*V(1) 4 204+V(1) (20)C> 30 11 211+V(2) [*]*
<< Success! ==> defined new CTR 2 (PA)
83 448 -16 204 (20)C> 30 11 219 01
== Executing PA-CTR 2, V(1)=3, V(2)=6, repcount=4, factor=3/2
123 704 0 2016 (20)C> 30 11 21 01
124 709 -3 2016 <C(31) 31 11 21 01
125 741 -35 <C(31) 3117 11 21 01
126 743 -37 <A(21) 3118 11 21 01
127 748 -34 (20)C> 3118 11 21 01
128 784 2 2018 (20)C> 11 21 01
129 786 4 2019 (00)C> 21 01
130 788 6 2019 00 (21)A> 01
131 793 3 2019 00 <C(30)
132 795 1 2019 <A(21) 30
133 800 4 2019 (20)C> 30
134 805 1 2019 <C(31) 31
135 843 -37 <C(31) 3120
136 845 -39 <A(21) 3121
137 850 -36 (20)C> 3121
138 892 6 2021 (20)C>
139 895 3 2021 <B(12) 10
140 937 -39 <B(12) 1221 10
141 944 -36 02 (02)A> 1221 10
142 949 -39 02 <B(13) 01 1220 10
143 951 -41 <B(13) 13 01 1220 10
144 958 -38 02 (02)C> 13 01 1220 10
145 960 -36 022 (02)C> 01 1220 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 201+V(1) (20)C> 30 11 21 01
1 5 -3 201+V(1) <C(31) 31 11 21 01
2 7+2*V(1) -5+-2*V(1) <C(31) 312+V(1) 11 21 01
3 9+2*V(1) -7+-2*V(1) <A(21) 313+V(1) 11 21 01
4 14+2*V(1) -4+-2*V(1) (20)C> 313+V(1) 11 21 01
5 20+4*V(1) 2 203+V(1) (20)C> 11 21 01
6 22+4*V(1) 4 204+V(1) (00)C> 21 01
7 24+4*V(1) 6 204+V(1) 00 (21)A> 01
8 29+4*V(1) 3 204+V(1) 00 <C(30)
9 31+4*V(1) 1 204+V(1) <A(21) 30
10 36+4*V(1) 4 204+V(1) (20)C> 30
11 41+4*V(1) 1 204+V(1) <C(31) 31
12 49+6*V(1) -7+-2*V(1) <C(31) 315+V(1)
13 51+6*V(1) -9+-2*V(1) <A(21) 316+V(1)
14 56+6*V(1) -6+-2*V(1) (20)C> 316+V(1)
15 68+8*V(1) 6 206+V(1) (20)C>
16 71+8*V(1) 3 206+V(1) <B(12) 10
17 83+10*V(1) -9+-2*V(1) <B(12) 126+V(1) 10
18 90+10*V(1) -6+-2*V(1) 02 (02)A> 126+V(1) 10
19 95+10*V(1) -9+-2*V(1) 02 <B(13) 01 125+V(1) 10
20 97+10*V(1) -11+-2*V(1) <B(13) 13 01 125+V(1) 10
21 104+10*V(1) -8+-2*V(1) 02 (02)C> 13 01 125+V(1) 10
22 106+10*V(1) -6+-2*V(1) 022 (02)C> 01 125+V(1) 10
<< Success! ==> defined new CTR 3 (PPA)
145 960 -36 022 (02)C> 01 1220 10
== Executing PA-CTR 1, V(1)=1, V(2)=17, repcount=9, factor=3/2
217 1698 0 0229 (02)C> 01 122 10
218 1701 -3 0229 <B(13) 11 122 10
219 1759 -61 <B(13) 1329 11 122 10
220 1766 -58 02 (02)C> 1329 11 122 10
221 1824 0 0230 (02)C> 11 122 10
222 1826 2 0231 (00)C> 122 10
223 1828 4 0231 00 (02)A> 12 10
224 1833 1 0231 00 <B(13) 01 10
225 1840 4 0232 (02)C> 01 10
226 1843 1 0232 <B(13) 11 10
227 1907 -63 <B(13) 1332 11 10
228 1914 -60 02 (02)C> 1332 11 10
229 1978 4 0233 (02)C> 11 10
230 1980 6 0234 (00)C> 10
231 1988 8 0234 00 (20)C>
232 1991 5 0234 00 <B(12) 10
233 1998 8 0235 (02)A> 10
234 2000 10 0236 (11)B>
235 2005 7 0236 <B(00) 10
236 2007 5 0235 <B(13) 00 10
237 2077 -65 <B(13) 1335 00 10
238 2084 -62 02 (02)C> 1335 00 10
239 2154 8 0236 (02)C> 00 10
240 2157 5 0236 <B(13) 102
241 2229 -67 <B(13) 1336 102
242 2236 -64 02 (02)C> 1336 102
243 2308 8 0237 (02)C> 102
244 2313 5 0237 <A(21) 21 10
245 2387 -69 <A(21) 2138 10
246 2392 -66 (20)C> 2138 10
247 2394 -64 20 (21)A> 2137 10
248 2397 -67 20 <C(30) 11 2136 10
249 2399 -69 <C(31) 30 11 2136 10
250 2401 -71 <A(21) 31 30 11 2136 10
251 2406 -68 (20)C> 31 30 11 2136 10
252 2408 -66 20 (20)C> 30 11 2136 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 021+V(1) (02)C> 01 122 10
1 3 -3 021+V(1) <B(13) 11 122 10
2 5+2*V(1) -5+-2*V(1) <B(13) 131+V(1) 11 122 10
3 12+2*V(1) -2+-2*V(1) 02 (02)C> 131+V(1) 11 122 10
4 14+4*V(1) 0 022+V(1) (02)C> 11 122 10
5 16+4*V(1) 2 023+V(1) (00)C> 122 10
6 18+4*V(1) 4 023+V(1) 00 (02)A> 12 10
7 23+4*V(1) 1 023+V(1) 00 <B(13) 01 10
8 30+4*V(1) 4 024+V(1) (02)C> 01 10
9 33+4*V(1) 1 024+V(1) <B(13) 11 10
10 41+6*V(1) -7+-2*V(1) <B(13) 134+V(1) 11 10
11 48+6*V(1) -4+-2*V(1) 02 (02)C> 134+V(1) 11 10
12 56+8*V(1) 4 025+V(1) (02)C> 11 10
13 58+8*V(1) 6 026+V(1) (00)C> 10
14 66+8*V(1) 8 026+V(1) 00 (20)C>
15 69+8*V(1) 5 026+V(1) 00 <B(12) 10
16 76+8*V(1) 8 027+V(1) (02)A> 10
17 78+8*V(1) 10 028+V(1) (11)B>
18 83+8*V(1) 7 028+V(1) <B(00) 10
19 85+8*V(1) 5 027+V(1) <B(13) 00 10
20 99+10*V(1) -9+-2*V(1) <B(13) 137+V(1) 00 10
21 106+10*V(1) -6+-2*V(1) 02 (02)C> 137+V(1) 00 10
22 120+12*V(1) 8 028+V(1) (02)C> 00 10
23 123+12*V(1) 5 028+V(1) <B(13) 102
24 139+14*V(1) -11+-2*V(1) <B(13) 138+V(1) 102
25 146+14*V(1) -8+-2*V(1) 02 (02)C> 138+V(1) 102
26 162+16*V(1) 8 029+V(1) (02)C> 102
27 167+16*V(1) 5 029+V(1) <A(21) 21 10
28 185+18*V(1) -13+-2*V(1) <A(21) 2110+V(1) 10
29 190+18*V(1) -10+-2*V(1) (20)C> 2110+V(1) 10
30 192+18*V(1) -8+-2*V(1) 20 (21)A> 219+V(1) 10
31 195+18*V(1) -11+-2*V(1) 20 <C(30) 11 218+V(1) 10
32 197+18*V(1) -13+-2*V(1) <C(31) 30 11 218+V(1) 10
33 199+18*V(1) -15+-2*V(1) <A(21) 31 30 11 218+V(1) 10
34 204+18*V(1) -12+-2*V(1) (20)C> 31 30 11 218+V(1) 10
35 206+18*V(1) -10+-2*V(1) 20 (20)C> 30 11 218+V(1) 10
<< Success! ==> defined new CTR 4 (PPA)
252 2408 -66 20 (20)C> 30 11 2136 10
== Executing PA-CTR 2, V(1)=0, V(2)=33, repcount=17, factor=3/2
422 4618 2 2052 (20)C> 30 11 212 10
423 4623 -1 2052 <C(31) 31 11 212 10
424 4727 -105 <C(31) 3153 11 212 10
425 4729 -107 <A(21) 3154 11 212 10
426 4734 -104 (20)C> 3154 11 212 10
427 4842 4 2054 (20)C> 11 212 10
428 4844 6 2055 (00)C> 212 10
429 4846 8 2055 00 (21)A> 21 10
430 4849 5 2055 00 <C(30) 11 10
431 4851 3 2055 <A(21) 30 11 10
432 4856 6 2055 (20)C> 30 11 10
433 4861 3 2055 <C(31) 31 11 10
434 4971 -107 <C(31) 3156 11 10
435 4973 -109 <A(21) 3157 11 10
436 4978 -106 (20)C> 3157 11 10
437 5092 8 2057 (20)C> 11 10
438 5094 10 2058 (00)C> 10
439 5102 12 2058 00 (20)C>
440 5105 9 2058 00 <B(12) 10
441 5112 12 2058 02 (02)A> 10
442 5114 14 2058 022 (11)B>
443 5119 11 2058 022 <B(00) 10
444 5121 9 2058 02 <B(13) 00 10
445 5123 7 2058 <B(13) 13 00 10
446 5125 5 2057 <B(12) 132 00 10
447 5239 -109 <B(12) 1257 132 00 10
448 5246 -106 02 (02)A> 1257 132 00 10
449 5251 -109 02 <B(13) 01 1256 132 00 10
450 5253 -111 <B(13) 13 01 1256 132 00 10
451 5260 -108 02 (02)C> 13 01 1256 132 00 10
452 5262 -106 022 (02)C> 01 1256 132 00 10
453 5265 -109 022 <B(13) 11 1256 132 00 10
454 5269 -113 <B(13) 132 11 1256 132 00 10
455 5276 -110 02 (02)C> 132 11 1256 132 00 10
456 5280 -106 023 (02)C> 11 1256 132 00 10
457 5282 -104 024 (00)C> 1256 132 00 10
458 5284 -102 024 00 (02)A> 1255 132 00 10
459 5289 -105 024 00 <B(13) 01 1254 132 00 10
460 5296 -102 025 (02)C> 01 1254 132 00 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 021+V(1) (02)C> 01 123+V(2) [*]* [*]* [*]*
1 3 -3 021+V(1) <B(13) 11 123+V(2) [*]* [*]* [*]*
2 5+2*V(1) -5+-2*V(1) <B(13) 131+V(1) 11 123+V(2) [*]* [*]* [*]*
3 12+2*V(1) -2+-2*V(1) 02 (02)C> 131+V(1) 11 123+V(2) [*]* [*]* [*]*
4 14+4*V(1) 0 022+V(1) (02)C> 11 123+V(2) [*]* [*]* [*]*
5 16+4*V(1) 2 023+V(1) (00)C> 123+V(2) [*]* [*]* [*]*
6 18+4*V(1) 4 023+V(1) 00 (02)A> 122+V(2) [*]* [*]* [*]*
7 23+4*V(1) 1 023+V(1) 00 <B(13) 01 121+V(2) [*]* [*]* [*]*
8 30+4*V(1) 4 024+V(1) (02)C> 01 121+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 5 (PA)
460 5296 -102 025 (02)C> 01 1254 132 00 10
== Executing PA-CTR 5, V(1)=4, V(2)=51, repcount=26, factor=3/2
668 10392 2 0283 (02)C> 01 122 132 00 10
669 10395 -1 0283 <B(13) 11 122 132 00 10
670 10561 -167 <B(13) 1383 11 122 132 00 10
671 10568 -164 02 (02)C> 1383 11 122 132 00 10
672 10734 2 0284 (02)C> 11 122 132 00 10
673 10736 4 0285 (00)C> 122 132 00 10
674 10738 6 0285 00 (02)A> 12 132 00 10
675 10743 3 0285 00 <B(13) 01 132 00 10
676 10750 6 0286 (02)C> 01 132 00 10
677 10753 3 0286 <B(13) 11 132 00 10
678 10925 -169 <B(13) 1386 11 132 00 10
679 10932 -166 02 (02)C> 1386 11 132 00 10
680 11104 6 0287 (02)C> 11 132 00 10
681 11106 8 0288 (00)C> 132 00 10
682 11108 10 0288 00 (02)C> 13 00 10
683 11110 12 0288 00 02 (02)C> 00 10
684 11113 9 0288 00 02 <B(13) 102
685 11115 7 0288 00 <B(13) 13 102
686 11122 10 0289 (02)C> 13 102
687 11124 12 0290 (02)C> 102
688 11129 9 0290 <A(21) 21 10
689 11309 -171 <A(21) 2191 10
690 11314 -168 (20)C> 2191 10
691 11316 -166 20 (21)A> 2190 10
692 11319 -169 20 <C(30) 11 2189 10
693 11321 -171 <C(31) 30 11 2189 10
694 11323 -173 <A(21) 31 30 11 2189 10
695 11328 -170 (20)C> 31 30 11 2189 10
696 11330 -168 20 (20)C> 30 11 2189 10
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 021+V(1) (02)C> 01 122 132+V(3) 00 101+V(2)
1 3 -3 021+V(1) <B(13) 11 122 132+V(3) 00 101+V(2)
2 5+2*V(1) -5+-2*V(1) <B(13) 131+V(1) 11 122 132+V(3) 00 101+V(2)
3 12+2*V(1) -2+-2*V(1) 02 (02)C> 131+V(1) 11 122 132+V(3) 00 101+V(2)
4 14+4*V(1) 0 022+V(1) (02)C> 11 122 132+V(3) 00 101+V(2)
5 16+4*V(1) 2 023+V(1) (00)C> 122 132+V(3) 00 101+V(2)
6 18+4*V(1) 4 023+V(1) 00 (02)A> 12 132+V(3) 00 101+V(2)
7 23+4*V(1) 1 023+V(1) 00 <B(13) 01 132+V(3) 00 101+V(2)
8 30+4*V(1) 4 024+V(1) (02)C> 01 132+V(3) 00 101+V(2)
9 33+4*V(1) 1 024+V(1) <B(13) 11 132+V(3) 00 101+V(2)
10 41+6*V(1) -7+-2*V(1) <B(13) 134+V(1) 11 132+V(3) 00 101+V(2)
11 48+6*V(1) -4+-2*V(1) 02 (02)C> 134+V(1) 11 132+V(3) 00 101+V(2)
12 56+8*V(1) 4 025+V(1) (02)C> 11 132+V(3) 00 101+V(2)
13 58+8*V(1) 6 026+V(1) (00)C> 132+V(3) 00 101+V(2)
14 60+8*V(1) 8 026+V(1) 00 (02)C> 131+V(3) 00 101+V(2)
15 62+8*V(1)+2*V(3) 10+2*V(3) 026+V(1) 00 021+V(3) (02)C> 00 101+V(2)
16 65+8*V(1)+2*V(3) 7+2*V(3) 026+V(1) 00 021+V(3) <B(13) 102+V(2)
17 67+8*V(1)+4*V(3) 5 026+V(1) 00 <B(13) 131+V(3) 102+V(2)
18 74+8*V(1)+4*V(3) 8 027+V(1) (02)C> 131+V(3) 102+V(2)
19 76+8*V(1)+6*V(3) 10+2*V(3) 028+V(1)+V(3) (02)C> 102+V(2)
20 81+8*V(1)+6*V(3) 7+2*V(3) 028+V(1)+V(3) <A(21) 21 101+V(2)
21 97+10*V(1)+8*V(3) -9+-2*V(1) <A(21) 219+V(1)+V(3) 101+V(2)
22 102+10*V(1)+8*V(3) -6+-2*V(1) (20)C> 219+V(1)+V(3) 101+V(2)
23 104+10*V(1)+8*V(3) -4+-2*V(1) 20 (21)A> 218+V(1)+V(3) 101+V(2)
24 107+10*V(1)+8*V(3) -7+-2*V(1) 20 <C(30) 11 217+V(1)+V(3) 101+V(2)
25 109+10*V(1)+8*V(3) -9+-2*V(1) <C(31) 30 11 217+V(1)+V(3) 101+V(2)
26 111+10*V(1)+8*V(3) -11+-2*V(1) <A(21) 31 30 11 217+V(1)+V(3) 101+V(2)
27 116+10*V(1)+8*V(3) -8+-2*V(1) (20)C> 31 30 11 217+V(1)+V(3) 101+V(2)
28 118+10*V(1)+8*V(3) -6+-2*V(1) 20 (20)C> 30 11 217+V(1)+V(3) 101+V(2)
<< Success! ==> defined new CTR 6 (PPA)
696 11330 -168 20 (20)C> 30 11 2189 10
== Executing PA-CTR 2, V(1)=0, V(2)=86, repcount=44, factor=3/2
1136 24178 8 20133 (20)C> 30 11 21 10
1137 24183 5 20133 <C(31) 31 11 21 10
1138 24449 -261 <C(31) 31134 11 21 10
1139 24451 -263 <A(21) 31135 11 21 10
1140 24456 -260 (20)C> 31135 11 21 10
1141 24726 10 20135 (20)C> 11 21 10
1142 24728 12 20136 (00)C> 21 10
1143 24730 14 20136 00 (21)A> 10
1144 24732 16 20136 00 21 (11)B>
1145 24737 13 20136 00 21 <B(00) 10
1146 24739 11 20136 00 <C(30) 00 10
1147 24741 9 20136 <A(21) 30 00 10
1148 24746 12 20136 (20)C> 30 00 10
1149 24751 9 20136 <C(31) 31 00 10
1150 25023 -263 <C(31) 31137 00 10
1151 25025 -265 <A(21) 31138 00 10
1152 25030 -262 (20)C> 31138 00 10
1153 25306 14 20138 (20)C> 00 10
1154 25309 11 20138 <B(12) 102
1155 25585 -265 <B(12) 12138 102
1156 25592 -262 02 (02)A> 12138 102
1157 25597 -265 02 <B(13) 01 12137 102
1158 25599 -267 <B(13) 13 01 12137 102
1159 25606 -264 02 (02)C> 13 01 12137 102
1160 25608 -262 022 (02)C> 01 12137 102
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 201+V(1) (20)C> 30 11 21 10
1 5 -3 201+V(1) <C(31) 31 11 21 10
2 7+2*V(1) -5+-2*V(1) <C(31) 312+V(1) 11 21 10
3 9+2*V(1) -7+-2*V(1) <A(21) 313+V(1) 11 21 10
4 14+2*V(1) -4+-2*V(1) (20)C> 313+V(1) 11 21 10
5 20+4*V(1) 2 203+V(1) (20)C> 11 21 10
6 22+4*V(1) 4 204+V(1) (00)C> 21 10
7 24+4*V(1) 6 204+V(1) 00 (21)A> 10
8 26+4*V(1) 8 204+V(1) 00 21 (11)B>
9 31+4*V(1) 5 204+V(1) 00 21 <B(00) 10
10 33+4*V(1) 3 204+V(1) 00 <C(30) 00 10
11 35+4*V(1) 1 204+V(1) <A(21) 30 00 10
12 40+4*V(1) 4 204+V(1) (20)C> 30 00 10
13 45+4*V(1) 1 204+V(1) <C(31) 31 00 10
14 53+6*V(1) -7+-2*V(1) <C(31) 315+V(1) 00 10
15 55+6*V(1) -9+-2*V(1) <A(21) 316+V(1) 00 10
16 60+6*V(1) -6+-2*V(1) (20)C> 316+V(1) 00 10
17 72+8*V(1) 6 206+V(1) (20)C> 00 10
18 75+8*V(1) 3 206+V(1) <B(12) 102
19 87+10*V(1) -9+-2*V(1) <B(12) 126+V(1) 102
20 94+10*V(1) -6+-2*V(1) 02 (02)A> 126+V(1) 102
21 99+10*V(1) -9+-2*V(1) 02 <B(13) 01 125+V(1) 102
22 101+10*V(1) -11+-2*V(1) <B(13) 13 01 125+V(1) 102
23 108+10*V(1) -8+-2*V(1) 02 (02)C> 13 01 125+V(1) 102
24 110+10*V(1) -6+-2*V(1) 022 (02)C> 01 125+V(1) 102
<< Success! ==> defined new CTR 7 (PPA)
1160 25608 -262 022 (02)C> 01 12137 102
== Executing PA-CTR 1, V(1)=1, V(2)=134, repcount=68, factor=3/2
1704 55256 10 02206 (02)C> 01 12 102
1705 55259 7 02206 <B(13) 11 12 102
1706 55671 -405 <B(13) 13206 11 12 102
1707 55678 -402 02 (02)C> 13206 11 12 102
1708 56090 10 02207 (02)C> 11 12 102
1709 56092 12 02208 (00)C> 12 102
1710 56094 14 02208 00 (02)A> 102
1711 56096 16 02208 00 02 (11)B> 10
1712 56099 13 02208 00 02 <B(00)
1713 56101 11 02208 00 <B(13)
1714 56108 14 02209 (02)C>
1715 56111 11 02209 <B(13) 10
1716 56529 -407 <B(13) 13209 10
1717 56536 -404 02 (02)C> 13209 10
1718 56954 14 02210 (02)C> 10
1719 56959 11 02210 <A(21) 21
1720 57379 -409 <A(21) 21211
1721 57384 -406 (20)C> 21211
1722 57386 -404 20 (21)A> 21210
1723 57389 -407 20 <C(30) 11 21209
1724 57391 -409 <C(31) 30 11 21209
1725 57393 -411 <A(21) 31 30 11 21209
1726 57398 -408 (20)C> 31 30 11 21209
1727 57400 -406 20 (20)C> 30 11 21209
1728 57405 -409 20 <C(31) 31 11 21209
1729 57407 -411 <C(31) 312 11 21209
1730 57409 -413 <A(21) 313 11 21209
1731 57414 -410 (20)C> 313 11 21209
1732 57420 -404 203 (20)C> 11 21209
1733 57422 -402 204 (00)C> 21209
1734 57424 -400 204 00 (21)A> 21208
1735 57427 -403 204 00 <C(30) 11 21207
1736 57429 -405 204 <A(21) 30 11 21207
1737 57434 -402 204 (20)C> 30 11 21207
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 201+V(1) (20)C> 30 11 213+V(2)
1 5 -3 201+V(1) <C(31) 31 11 213+V(2)
2 7+2*V(1) -5+-2*V(1) <C(31) 312+V(1) 11 213+V(2)
3 9+2*V(1) -7+-2*V(1) <A(21) 313+V(1) 11 213+V(2)
4 14+2*V(1) -4+-2*V(1) (20)C> 313+V(1) 11 213+V(2)
5 20+4*V(1) 2 203+V(1) (20)C> 11 213+V(2)
6 22+4*V(1) 4 204+V(1) (00)C> 213+V(2)
7 24+4*V(1) 6 204+V(1) 00 (21)A> 212+V(2)
8 27+4*V(1) 3 204+V(1) 00 <C(30) 11 211+V(2)
9 29+4*V(1) 1 204+V(1) <A(21) 30 11 211+V(2)
10 34+4*V(1) 4 204+V(1) (20)C> 30 11 211+V(2)
<< Success! ==> defined new CTR 8 (PA)
1737 57434 -402 204 (20)C> 30 11 21207
== Executing PA-CTR 8, V(1)=3, V(2)=204, repcount=103, factor=3/2
2767 125208 10 20313 (20)C> 30 11 21
2768 125213 7 20313 <C(31) 31 11 21
2769 125839 -619 <C(31) 31314 11 21
2770 125841 -621 <A(21) 31315 11 21
2771 125846 -618 (20)C> 31315 11 21
2772 126476 12 20315 (20)C> 11 21
2773 126478 14 20316 (00)C> 21
2774 126480 16 20316 00 (21)A>
2775 126487 13 20316 00 <C(30) 01
2776 126489 11 20316 <A(21) 30 01
2777 126494 14 20316 (20)C> 30 01
2778 126499 11 20316 <C(31) 31 01
2779 127131 -621 <C(31) 31317 01
2780 127133 -623 <A(21) 31318 01
2781 127138 -620 (20)C> 31318 01
2782 127774 16 20318 (20)C> 01
2783 127777 13 20318 <B(12) 11
2784 128413 -623 <B(12) 12318 11
2785 128420 -620 02 (02)A> 12318 11
2786 128425 -623 02 <B(13) 01 12317 11
2787 128427 -625 <B(13) 13 01 12317 11
2788 128434 -622 02 (02)C> 13 01 12317 11
2789 128436 -620 022 (02)C> 01 12317 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 201+V(1) (20)C> 30 11 21
1 5 -3 201+V(1) <C(31) 31 11 21
2 7+2*V(1) -5+-2*V(1) <C(31) 312+V(1) 11 21
3 9+2*V(1) -7+-2*V(1) <A(21) 313+V(1) 11 21
4 14+2*V(1) -4+-2*V(1) (20)C> 313+V(1) 11 21
5 20+4*V(1) 2 203+V(1) (20)C> 11 21
6 22+4*V(1) 4 204+V(1) (00)C> 21
7 24+4*V(1) 6 204+V(1) 00 (21)A>
8 31+4*V(1) 3 204+V(1) 00 <C(30) 01
9 33+4*V(1) 1 204+V(1) <A(21) 30 01
10 38+4*V(1) 4 204+V(1) (20)C> 30 01
11 43+4*V(1) 1 204+V(1) <C(31) 31 01
12 51+6*V(1) -7+-2*V(1) <C(31) 315+V(1) 01
13 53+6*V(1) -9+-2*V(1) <A(21) 316+V(1) 01
14 58+6*V(1) -6+-2*V(1) (20)C> 316+V(1) 01
15 70+8*V(1) 6 206+V(1) (20)C> 01
16 73+8*V(1) 3 206+V(1) <B(12) 11
17 85+10*V(1) -9+-2*V(1) <B(12) 126+V(1) 11
18 92+10*V(1) -6+-2*V(1) 02 (02)A> 126+V(1) 11
19 97+10*V(1) -9+-2*V(1) 02 <B(13) 01 125+V(1) 11
20 99+10*V(1) -11+-2*V(1) <B(13) 13 01 125+V(1) 11
21 106+10*V(1) -8+-2*V(1) 02 (02)C> 13 01 125+V(1) 11
22 108+10*V(1) -6+-2*V(1) 022 (02)C> 01 125+V(1) 11
<< Success! ==> defined new CTR 9 (PPA)
2789 128436 -620 022 (02)C> 01 12317 11
== Executing PA-CTR 1, V(1)=1, V(2)=314, repcount=158, factor=3/2
4053 282644 12 02476 (02)C> 01 12 11
4054 282647 9 02476 <B(13) 11 12 11
4055 283599 -943 <B(13) 13476 11 12 11
4056 283606 -940 02 (02)C> 13476 11 12 11
4057 284558 12 02477 (02)C> 11 12 11
4058 284560 14 02478 (00)C> 12 11
4059 284562 16 02478 00 (02)A> 11
4060 284564 18 02478 00 02 (11)A>
4061 284571 15 02478 00 02 <B(00) 01
4062 284573 13 02478 00 <B(13) 00 01
4063 284580 16 02479 (02)C> 00 01
4064 284583 13 02479 <B(13) 10 01
4065 285541 -945 <B(13) 13479 10 01
4066 285548 -942 02 (02)C> 13479 10 01
4067 286506 16 02480 (02)C> 10 01
4068 286511 13 02480 <A(21) 21 01
4069 287471 -947 <A(21) 21481 01
4070 287476 -944 (20)C> 21481 01
4071 287478 -942 20 (21)A> 21480 01
4072 287481 -945 20 <C(30) 11 21479 01
4073 287483 -947 <C(31) 30 11 21479 01
4074 287485 -949 <A(21) 31 30 11 21479 01
4075 287490 -946 (20)C> 31 30 11 21479 01
4076 287492 -944 20 (20)C> 30 11 21479 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 021+V(1) (02)C> 01 12 11
1 3 -3 021+V(1) <B(13) 11 12 11
2 5+2*V(1) -5+-2*V(1) <B(13) 131+V(1) 11 12 11
3 12+2*V(1) -2+-2*V(1) 02 (02)C> 131+V(1) 11 12 11
4 14+4*V(1) 0 022+V(1) (02)C> 11 12 11
5 16+4*V(1) 2 023+V(1) (00)C> 12 11
6 18+4*V(1) 4 023+V(1) 00 (02)A> 11
7 20+4*V(1) 6 023+V(1) 00 02 (11)A>
8 27+4*V(1) 3 023+V(1) 00 02 <B(00) 01
9 29+4*V(1) 1 023+V(1) 00 <B(13) 00 01
10 36+4*V(1) 4 024+V(1) (02)C> 00 01
11 39+4*V(1) 1 024+V(1) <B(13) 10 01
12 47+6*V(1) -7+-2*V(1) <B(13) 134+V(1) 10 01
13 54+6*V(1) -4+-2*V(1) 02 (02)C> 134+V(1) 10 01
14 62+8*V(1) 4 025+V(1) (02)C> 10 01
15 67+8*V(1) 1 025+V(1) <A(21) 21 01
16 77+10*V(1) -9+-2*V(1) <A(21) 216+V(1) 01
17 82+10*V(1) -6+-2*V(1) (20)C> 216+V(1) 01
18 84+10*V(1) -4+-2*V(1) 20 (21)A> 215+V(1) 01
19 87+10*V(1) -7+-2*V(1) 20 <C(30) 11 214+V(1) 01
20 89+10*V(1) -9+-2*V(1) <C(31) 30 11 214+V(1) 01
21 91+10*V(1) -11+-2*V(1) <A(21) 31 30 11 214+V(1) 01
22 96+10*V(1) -8+-2*V(1) (20)C> 31 30 11 214+V(1) 01
23 98+10*V(1) -6+-2*V(1) 20 (20)C> 30 11 214+V(1) 01
<< Success! ==> defined new CTR 10 (PPA)
4076 287492 -944 20 (20)C> 30 11 21479 01
== Executing PA-CTR 2, V(1)=0, V(2)=476, repcount=239, factor=3/2
6466 636910 12 20718 (20)C> 30 11 21 01
== Executing PPA-CTR 3 (once), V(1)=717
6488 644186 -1428 022 (02)C> 01 12722 10
== Executing PA-CTR 1, V(1)=1, V(2)=719, repcount=360, factor=3/2
9368 1431866 12 021082 (02)C> 01 122 10
== Executing PPA-CTR 4 (once), V(1)=1081
9403 1451530 -2160 20 (20)C> 30 11 211089 10
== Executing PA-CTR 2, V(1)=0, V(2)=1086, repcount=544, factor=3/2
14843 3242378 16 201633 (20)C> 30 11 21 10
== Executing PPA-CTR 7 (once), V(1)=1632
14867 3258808 -3254 022 (02)C> 01 121637 102
== Executing PA-CTR 1, V(1)=1, V(2)=1634, repcount=818, factor=3/2
21411 7296456 18 022456 (02)C> 01 12 102
21412 7296459 15 022456 <B(13) 11 12 102
21413 7301371 -4897 <B(13) 132456 11 12 102
21414 7301378 -4894 02 (02)C> 132456 11 12 102
21415 7306290 18 022457 (02)C> 11 12 102
21416 7306292 20 022458 (00)C> 12 102
21417 7306294 22 022458 00 (02)A> 102
21418 7306296 24 022458 00 02 (11)B> 10
21419 7306299 21 022458 00 02 <B(00)
21420 7306301 19 022458 00 <B(13)
21421 7306308 22 022459 (02)C>
21422 7306311 19 022459 <B(13) 10
21423 7311229 -4899 <B(13) 132459 10
21424 7311236 -4896 02 (02)C> 132459 10
21425 7316154 22 022460 (02)C> 10
21426 7316159 19 022460 <A(21) 21
21427 7321079 -4901 <A(21) 212461
21428 7321084 -4898 (20)C> 212461
21429 7321086 -4896 20 (21)A> 212460
21430 7321089 -4899 20 <C(30) 11 212459
21431 7321091 -4901 <C(31) 30 11 212459
21432 7321093 -4903 <A(21) 31 30 11 212459
21433 7321098 -4900 (20)C> 31 30 11 212459
21434 7321100 -4898 20 (20)C> 30 11 212459
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 021+V(1) (02)C> 01 12 102
1 3 -3 021+V(1) <B(13) 11 12 102
2 5+2*V(1) -5+-2*V(1) <B(13) 131+V(1) 11 12 102
3 12+2*V(1) -2+-2*V(1) 02 (02)C> 131+V(1) 11 12 102
4 14+4*V(1) 0 022+V(1) (02)C> 11 12 102
5 16+4*V(1) 2 023+V(1) (00)C> 12 102
6 18+4*V(1) 4 023+V(1) 00 (02)A> 102
7 20+4*V(1) 6 023+V(1) 00 02 (11)B> 10
8 23+4*V(1) 3 023+V(1) 00 02 <B(00)
9 25+4*V(1) 1 023+V(1) 00 <B(13)
10 32+4*V(1) 4 024+V(1) (02)C>
11 35+4*V(1) 1 024+V(1) <B(13) 10
12 43+6*V(1) -7+-2*V(1) <B(13) 134+V(1) 10
13 50+6*V(1) -4+-2*V(1) 02 (02)C> 134+V(1) 10
14 58+8*V(1) 4 025+V(1) (02)C> 10
15 63+8*V(1) 1 025+V(1) <A(21) 21
16 73+10*V(1) -9+-2*V(1) <A(21) 216+V(1)
17 78+10*V(1) -6+-2*V(1) (20)C> 216+V(1)
18 80+10*V(1) -4+-2*V(1) 20 (21)A> 215+V(1)
19 83+10*V(1) -7+-2*V(1) 20 <C(30) 11 214+V(1)
20 85+10*V(1) -9+-2*V(1) <C(31) 30 11 214+V(1)
21 87+10*V(1) -11+-2*V(1) <A(21) 31 30 11 214+V(1)
22 92+10*V(1) -8+-2*V(1) (20)C> 31 30 11 214+V(1)
23 94+10*V(1) -6+-2*V(1) 20 (20)C> 30 11 214+V(1)
<< Success! ==> defined new CTR 11 (PPA)
21434 7321100 -4898 20 (20)C> 30 11 212459
== Executing PA-CTR 8, V(1)=0, V(2)=2456, repcount=1229, factor=3/2
33724 16418158 18 203688 (20)C> 30 11 21
== Executing PPA-CTR 9 (once), V(1)=3687
33746 16455136 -7362 022 (02)C> 01 123692 11
== Executing PA-CTR 1, V(1)=1, V(2)=3689, repcount=1845, factor=3/2
48506 36930946 18 025537 (02)C> 01 122 11
48507 36930949 15 025537 <B(13) 11 122 11
48508 36942023 -11059 <B(13) 135537 11 122 11
48509 36942030 -11056 02 (02)C> 135537 11 122 11
48510 36953104 18 025538 (02)C> 11 122 11
48511 36953106 20 025539 (00)C> 122 11
48512 36953108 22 025539 00 (02)A> 12 11
48513 36953113 19 025539 00 <B(13) 01 11
48514 36953120 22 025540 (02)C> 01 11
48515 36953123 19 025540 <B(13) 112
48516 36964203 -11061 <B(13) 135540 112
48517 36964210 -11058 02 (02)C> 135540 112
48518 36975290 22 025541 (02)C> 112
48519 36975292 24 025542 (00)C> 11
48520 36975294 26 025542 00 (00)C>
48521 36975305 23 025542 00 <A(21) 21
48522 36975310 26 025542 00 (20)C> 21
48523 36975312 28 025542 00 20 (21)A>
48524 36975319 25 025542 00 20 <C(30) 01
48525 36975321 23 025542 00 <C(31) 30 01
48526 36975323 21 025542 <A(21) 31 30 01
48527 36986407 -11063 <A(21) 215542 31 30 01
48528 36986412 -11060 (20)C> 215542 31 30 01
48529 36986414 -11058 20 (21)A> 215541 31 30 01
48530 36986417 -11061 20 <C(30) 11 215540 31 30 01
48531 36986419 -11063 <C(31) 30 11 215540 31 30 01
48532 36986421 -11065 <A(21) 31 30 11 215540 31 30 01
48533 36986426 -11062 (20)C> 31 30 11 215540 31 30 01
48534 36986428 -11060 20 (20)C> 30 11 215540 31 30 01
48535 36986433 -11063 20 <C(31) 31 11 215540 31 30 01
48536 36986435 -11065 <C(31) 312 11 215540 31 30 01
48537 36986437 -11067 <A(21) 313 11 215540 31 30 01
48538 36986442 -11064 (20)C> 313 11 215540 31 30 01
48539 36986448 -11058 203 (20)C> 11 215540 31 30 01
48540 36986450 -11056 204 (00)C> 215540 31 30 01
48541 36986452 -11054 204 00 (21)A> 215539 31 30 01
48542 36986455 -11057 204 00 <C(30) 11 215538 31 30 01
48543 36986457 -11059 204 <A(21) 30 11 215538 31 30 01
48544 36986462 -11056 204 (20)C> 30 11 215538 31 30 01
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 201+V(1) (20)C> 30 11 213+V(2) [*]* [*]* [*]*
1 5 -3 201+V(1) <C(31) 31 11 213+V(2) [*]* [*]* [*]*
2 7+2*V(1) -5+-2*V(1) <C(31) 312+V(1) 11 213+V(2) [*]* [*]* [*]*
3 9+2*V(1) -7+-2*V(1) <A(21) 313+V(1) 11 213+V(2) [*]* [*]* [*]*
4 14+2*V(1) -4+-2*V(1) (20)C> 313+V(1) 11 213+V(2) [*]* [*]* [*]*
5 20+4*V(1) 2 203+V(1) (20)C> 11 213+V(2) [*]* [*]* [*]*
6 22+4*V(1) 4 204+V(1) (00)C> 213+V(2) [*]* [*]* [*]*
7 24+4*V(1) 6 204+V(1) 00 (21)A> 212+V(2) [*]* [*]* [*]*
8 27+4*V(1) 3 204+V(1) 00 <C(30) 11 211+V(2) [*]* [*]* [*]*
9 29+4*V(1) 1 204+V(1) <A(21) 30 11 211+V(2) [*]* [*]* [*]*
10 34+4*V(1) 4 204+V(1) (20)C> 30 11 211+V(2) [*]* [*]* [*]*
<< Success! ==> defined new CTR 12 (PA)
48544 36986462 -11056 204 (20)C> 30 11 215538 31 30 01
== Executing PA-CTR 12, V(1)=3, V(2)=5535, repcount=2768, factor=3/2
76224 83068126 16 208308 (20)C> 30 11 212 31 30 01
76225 83068131 13 208308 <C(31) 31 11 212 31 30 01
76226 83084747 -16603 <C(31) 318309 11 212 31 30 01
76227 83084749 -16605 <A(21) 318310 11 212 31 30 01
76228 83084754 -16602 (20)C> 318310 11 212 31 30 01
76229 83101374 18 208310 (20)C> 11 212 31 30 01
76230 83101376 20 208311 (00)C> 212 31 30 01
76231 83101378 22 208311 00 (21)A> 21 31 30 01
76232 83101381 19 208311 00 <C(30) 11 31 30 01
76233 83101383 17 208311 <A(21) 30 11 31 30 01
76234 83101388 20 208311 (20)C> 30 11 31 30 01
76235 83101393 17 208311 <C(31) 31 11 31 30 01
76236 83118015 -16605 <C(31) 318312 11 31 30 01
76237 83118017 -16607 <A(21) 318313 11 31 30 01
76238 83118022 -16604 (20)C> 318313 11 31 30 01
76239 83134648 22 208313 (20)C> 11 31 30 01
76240 83134650 24 208314 (00)C> 31 30 01
76241 83134652 26 208314 00 (20)C> 30 01
76242 83134657 23 208314 00 <C(31) 31 01
76243 83134659 21 208314 <A(21) 312 01
76244 83134664 24 208314 (20)C> 312 01
76245 83134668 28 208316 (20)C> 01
76246 83134671 25 208316 <B(12) 11
76247 83151303 -16607 <B(12) 128316 11
76248 83151310 -16604 02 (02)A> 128316 11
76249 83151315 -16607 02 <B(13) 01 128315 11
76250 83151317 -16609 <B(13) 13 01 128315 11
76251 83151324 -16606 02 (02)C> 13 01 128315 11
76252 83151326 -16604 022 (02)C> 01 128315 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 201+V(1) (20)C> 30 11 212 31 30 01
1 5 -3 201+V(1) <C(31) 31 11 212 31 30 01
2 7+2*V(1) -5+-2*V(1) <C(31) 312+V(1) 11 212 31 30 01
3 9+2*V(1) -7+-2*V(1) <A(21) 313+V(1) 11 212 31 30 01
4 14+2*V(1) -4+-2*V(1) (20)C> 313+V(1) 11 212 31 30 01
5 20+4*V(1) 2 203+V(1) (20)C> 11 212 31 30 01
6 22+4*V(1) 4 204+V(1) (00)C> 212 31 30 01
7 24+4*V(1) 6 204+V(1) 00 (21)A> 21 31 30 01
8 27+4*V(1) 3 204+V(1) 00 <C(30) 11 31 30 01
9 29+4*V(1) 1 204+V(1) <A(21) 30 11 31 30 01
10 34+4*V(1) 4 204+V(1) (20)C> 30 11 31 30 01
11 39+4*V(1) 1 204+V(1) <C(31) 31 11 31 30 01
12 47+6*V(1) -7+-2*V(1) <C(31) 315+V(1) 11 31 30 01
13 49+6*V(1) -9+-2*V(1) <A(21) 316+V(1) 11 31 30 01
14 54+6*V(1) -6+-2*V(1) (20)C> 316+V(1) 11 31 30 01
15 66+8*V(1) 6 206+V(1) (20)C> 11 31 30 01
16 68+8*V(1) 8 207+V(1) (00)C> 31 30 01
17 70+8*V(1) 10 207+V(1) 00 (20)C> 30 01
18 75+8*V(1) 7 207+V(1) 00 <C(31) 31 01
19 77+8*V(1) 5 207+V(1) <A(21) 312 01
20 82+8*V(1) 8 207+V(1) (20)C> 312 01
21 86+8*V(1) 12 209+V(1) (20)C> 01
22 89+8*V(1) 9 209+V(1) <B(12) 11
23 107+10*V(1) -9+-2*V(1) <B(12) 129+V(1) 11
24 114+10*V(1) -6+-2*V(1) 02 (02)A> 129+V(1) 11
25 119+10*V(1) -9+-2*V(1) 02 <B(13) 01 128+V(1) 11
26 121+10*V(1) -11+-2*V(1) <B(13) 13 01 128+V(1) 11
27 128+10*V(1) -8+-2*V(1) 02 (02)C> 13 01 128+V(1) 11
28 130+10*V(1) -6+-2*V(1) 022 (02)C> 01 128+V(1) 11
<< Success! ==> defined new CTR 13 (PPA)
76252 83151326 -16604 022 (02)C> 01 128315 11
== Executing PA-CTR 1, V(1)=1, V(2)=8312, repcount=4157, factor=3/2
109508 186951616 24 0212473 (02)C> 01 12 11
== Executing PPA-CTR 10 (once), V(1)=12472
109531 187076434 -24926 20 (20)C> 30 11 2112476 01
== Executing PA-CTR 2, V(1)=0, V(2)=12473, repcount=6237, factor=3/2
171901 420652084 22 2018712 (20)C> 30 11 212 01
171902 420652089 19 2018712 <C(31) 31 11 212 01
171903 420689513 -37405 <C(31) 3118713 11 212 01
171904 420689515 -37407 <A(21) 3118714 11 212 01
171905 420689520 -37404 (20)C> 3118714 11 212 01
171906 420726948 24 2018714 (20)C> 11 212 01
171907 420726950 26 2018715 (00)C> 212 01
171908 420726952 28 2018715 00 (21)A> 21 01
171909 420726955 25 2018715 00 <C(30) 11 01
171910 420726957 23 2018715 <A(21) 30 11 01
171911 420726962 26 2018715 (20)C> 30 11 01
171912 420726967 23 2018715 <C(31) 31 11 01
171913 420764397 -37407 <C(31) 3118716 11 01
171914 420764399 -37409 <A(21) 3118717 11 01
171915 420764404 -37406 (20)C> 3118717 11 01
171916 420801838 28 2018717 (20)C> 11 01
171917 420801840 30 2018718 (00)C> 01
171918 420801848 32 2018718 02 (00)C>
171919 420801859 29 2018718 02 <A(21) 21
171920 420801861 27 2018718 <A(21) 212
171921 420801866 30 2018718 (20)C> 212
171922 420801868 32 2018719 (21)A> 21
171923 420801871 29 2018719 <C(30) 11
171924 420801873 27 2018718 <C(31) 30 11
171925 420839309 -37409 <C(31) 3118718 30 11
171926 420839311 -37411 <A(21) 3118719 30 11
171927 420839316 -37408 (20)C> 3118719 30 11
171928 420876754 30 2018719 (20)C> 30 11
171929 420876759 27 2018719 <C(31) 31 11
171930 420914197 -37411 <C(31) 3118720 11
171931 420914199 -37413 <A(21) 3118721 11
171932 420914204 -37410 (20)C> 3118721 11
171933 420951646 32 2018721 (20)C> 11
171934 420951648 34 2018722 (00)C>
171935 420951659 31 2018722 <A(21) 21
171936 420951664 34 2018722 (20)C> 21
171937 420951666 36 2018723 (21)A>
171938 420951673 33 2018723 <C(30) 01
171939 420951675 31 2018722 <C(31) 30 01
171940 420989119 -37413 <C(31) 3118722 30 01
171941 420989121 -37415 <A(21) 3118723 30 01
171942 420989126 -37412 (20)C> 3118723 30 01
171943 421026572 34 2018723 (20)C> 30 01
171944 421026577 31 2018723 <C(31) 31 01
171945 421064023 -37415 <C(31) 3118724 01
171946 421064025 -37417 <A(21) 3118725 01
171947 421064030 -37414 (20)C> 3118725 01
171948 421101480 36 2018725 (20)C> 01
171949 421101483 33 2018725 <B(12) 11
171950 421138933 -37417 <B(12) 1218725 11
171951 421138940 -37414 02 (02)A> 1218725 11
171952 421138945 -37417 02 <B(13) 01 1218724 11
171953 421138947 -37419 <B(13) 13 01 1218724 11
171954 421138954 -37416 02 (02)C> 13 01 1218724 11
171955 421138956 -37414 022 (02)C> 01 1218724 11
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 201+V(1) (20)C> 30 11 212 01
1 5 -3 201+V(1) <C(31) 31 11 212 01
2 7+2*V(1) -5+-2*V(1) <C(31) 312+V(1) 11 212 01
3 9+2*V(1) -7+-2*V(1) <A(21) 313+V(1) 11 212 01
4 14+2*V(1) -4+-2*V(1) (20)C> 313+V(1) 11 212 01
5 20+4*V(1) 2 203+V(1) (20)C> 11 212 01
6 22+4*V(1) 4 204+V(1) (00)C> 212 01
7 24+4*V(1) 6 204+V(1) 00 (21)A> 21 01
8 27+4*V(1) 3 204+V(1) 00 <C(30) 11 01
9 29+4*V(1) 1 204+V(1) <A(21) 30 11 01
10 34+4*V(1) 4 204+V(1) (20)C> 30 11 01
11 39+4*V(1) 1 204+V(1) <C(31) 31 11 01
12 47+6*V(1) -7+-2*V(1) <C(31) 315+V(1) 11 01
13 49+6*V(1) -9+-2*V(1) <A(21) 316+V(1) 11 01
14 54+6*V(1) -6+-2*V(1) (20)C> 316+V(1) 11 01
15 66+8*V(1) 6 206+V(1) (20)C> 11 01
16 68+8*V(1) 8 207+V(1) (00)C> 01
17 76+8*V(1) 10 207+V(1) 02 (00)C>
18 87+8*V(1) 7 207+V(1) 02 <A(21) 21
19 89+8*V(1) 5 207+V(1) <A(21) 212
20 94+8*V(1) 8 207+V(1) (20)C> 212
21 96+8*V(1) 10 208+V(1) (21)A> 21
22 99+8*V(1) 7 208+V(1) <C(30) 11
23 101+8*V(1) 5 207+V(1) <C(31) 30 11
24 115+10*V(1) -9+-2*V(1) <C(31) 317+V(1) 30 11
25 117+10*V(1) -11+-2*V(1) <A(21) 318+V(1) 30 11
26 122+10*V(1) -8+-2*V(1) (20)C> 318+V(1) 30 11
27 138+12*V(1) 8 208+V(1) (20)C> 30 11
28 143+12*V(1) 5 208+V(1) <C(31) 31 11
29 159+14*V(1) -11+-2*V(1) <C(31) 319+V(1) 11
30 161+14*V(1) -13+-2*V(1) <A(21) 3110+V(1) 11
31 166+14*V(1) -10+-2*V(1) (20)C> 3110+V(1) 11
32 186+16*V(1) 10 2010+V(1) (20)C> 11
33 188+16*V(1) 12 2011+V(1) (00)C>
34 199+16*V(1) 9 2011+V(1) <A(21) 21
35 204+16*V(1) 12 2011+V(1) (20)C> 21
36 206+16*V(1) 14 2012+V(1) (21)A>
37 213+16*V(1) 11 2012+V(1) <C(30) 01
38 215+16*V(1) 9 2011+V(1) <C(31) 30 01
39 237+18*V(1) -13+-2*V(1) <C(31) 3111+V(1) 30 01
40 239+18*V(1) -15+-2*V(1) <A(21) 3112+V(1) 30 01
41 244+18*V(1) -12+-2*V(1) (20)C> 3112+V(1) 30 01
42 268+20*V(1) 12 2012+V(1) (20)C> 30 01
43 273+20*V(1) 9 2012+V(1) <C(31) 31 01
44 297+22*V(1) -15+-2*V(1) <C(31) 3113+V(1) 01
45 299+22*V(1) -17+-2*V(1) <A(21) 3114+V(1) 01
46 304+22*V(1) -14+-2*V(1) (20)C> 3114+V(1) 01
47 332+24*V(1) 14 2014+V(1) (20)C> 01
48 335+24*V(1) 11 2014+V(1) <B(12) 11
49 363+26*V(1) -17+-2*V(1) <B(12) 1214+V(1) 11
50 370+26*V(1) -14+-2*V(1) 02 (02)A> 1214+V(1) 11
51 375+26*V(1) -17+-2*V(1) 02 <B(13) 01 1213+V(1) 11
52 377+26*V(1) -19+-2*V(1) <B(13) 13 01 1213+V(1) 11
53 384+26*V(1) -16+-2*V(1) 02 (02)C> 13 01 1213+V(1) 11
54 386+26*V(1) -14+-2*V(1) 022 (02)C> 01 1213+V(1) 11
<< Success! ==> defined new CTR 14 (PPA)
171955 421138956 -37414 022 (02)C> 01 1218724 11
== Executing PA-CTR 1, V(1)=1, V(2)=18721, repcount=9361, factor=3/2
246843 947170990 30 0228085 (02)C> 01 122 11
246844 947170993 27 0228085 <B(13) 11 122 11
246845 947227163 -56143 <B(13) 1328085 11 122 11
246846 947227170 -56140 02 (02)C> 1328085 11 122 11
246847 947283340 30 0228086 (02)C> 11 122 11
246848 947283342 32 0228087 (00)C> 122 11
246849 947283344 34 0228087 00 (02)A> 12 11
246850 947283349 31 0228087 00 <B(13) 01 11
246851 947283356 34 0228088 (02)C> 01 11
246852 947283359 31 0228088 <B(13) 112
246853 947339535 -56145 <B(13) 1328088 112
246854 947339542 -56142 02 (02)C> 1328088 112
246855 947395718 34 0228089 (02)C> 112
246856 947395720 36 0228090 (00)C> 11
246857 947395722 38 0228090 00 (00)C>
246858 947395733 35 0228090 00 <A(21) 21
246859 947395738 38 0228090 00 (20)C> 21
246860 947395740 40 0228090 00 20 (21)A>
246861 947395747 37 0228090 00 20 <C(30) 01
246862 947395749 35 0228090 00 <C(31) 30 01
246863 947395751 33 0228090 <A(21) 31 30 01
246864 947451931 -56147 <A(21) 2128090 31 30 01
246865 947451936 -56144 (20)C> 2128090 31 30 01
246866 947451938 -56142 20 (21)A> 2128089 31 30 01
246867 947451941 -56145 20 <C(30) 11 2128088 31 30 01
246868 947451943 -56147 <C(31) 30 11 2128088 31 30 01
246869 947451945 -56149 <A(21) 31 30 11 2128088 31 30 01
246870 947451950 -56146 (20)C> 31 30 11 2128088 31 30 01
246871 947451952 -56144 20 (20)C> 30 11 2128088 31 30 01
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 021+V(1) (02)C> 01 122 11
1 3 -3 021+V(1) <B(13) 11 122 11
2 5+2*V(1) -5+-2*V(1) <B(13) 131+V(1) 11 122 11
3 12+2*V(1) -2+-2*V(1) 02 (02)C> 131+V(1) 11 122 11
4 14+4*V(1) 0 022+V(1) (02)C> 11 122 11
5 16+4*V(1) 2 023+V(1) (00)C> 122 11
6 18+4*V(1) 4 023+V(1) 00 (02)A> 12 11
7 23+4*V(1) 1 023+V(1) 00 <B(13) 01 11
8 30+4*V(1) 4 024+V(1) (02)C> 01 11
9 33+4*V(1) 1 024+V(1) <B(13) 112
10 41+6*V(1) -7+-2*V(1) <B(13) 134+V(1) 112
11 48+6*V(1) -4+-2*V(1) 02 (02)C> 134+V(1) 112
12 56+8*V(1) 4 025+V(1) (02)C> 112
13 58+8*V(1) 6 026+V(1) (00)C> 11
14 60+8*V(1) 8 026+V(1) 00 (00)C>
15 71+8*V(1) 5 026+V(1) 00 <A(21) 21
16 76+8*V(1) 8 026+V(1) 00 (20)C> 21
17 78+8*V(1) 10 026+V(1) 00 20 (21)A>
18 85+8*V(1) 7 026+V(1) 00 20 <C(30) 01
19 87+8*V(1) 5 026+V(1) 00 <C(31) 30 01
20 89+8*V(1) 3 026+V(1) <A(21) 31 30 01
21 101+10*V(1) -9+-2*V(1) <A(21) 216+V(1) 31 30 01
22 106+10*V(1) -6+-2*V(1) (20)C> 216+V(1) 31 30 01
23 108+10*V(1) -4+-2*V(1) 20 (21)A> 215+V(1) 31 30 01
24 111+10*V(1) -7+-2*V(1) 20 <C(30) 11 214+V(1) 31 30 01
25 113+10*V(1) -9+-2*V(1) <C(31) 30 11 214+V(1) 31 30 01
26 115+10*V(1) -11+-2*V(1) <A(21) 31 30 11 214+V(1) 31 30 01
27 120+10*V(1) -8+-2*V(1) (20)C> 31 30 11 214+V(1) 31 30 01
28 122+10*V(1) -6+-2*V(1) 20 (20)C> 30 11 214+V(1) 31 30 01
<< Success! ==> defined new CTR 15 (PPA)
246871 947451952 -56144 20 (20)C> 30 11 2128088 31 30 01
== Executing PA-CTR 12, V(1)=0, V(2)=28085, repcount=14043, factor=3/2
387301 2131080250 28 2042130 (20)C> 30 11 212 31 30 01
== Executing PPA-CTR 13 (once), V(1)=42129
387329 2131501670 -84236 022 (02)C> 01 1242137 11
== Executing PA-CTR 1, V(1)=1, V(2)=42134, repcount=21068, factor=3/2
555873 4795255318 36 0263206 (02)C> 01 12 11
== Executing PPA-CTR 10 (once), V(1)=63205
555896 4795887466 -126380 20 (20)C> 30 11 2163209 01
== Executing PA-CTR 2, V(1)=0, V(2)=63206, repcount=31604, factor=3/2
871936 10789649274 36 2094813 (20)C> 30 11 21 01
== Executing PPA-CTR 3 (once), V(1)=94812
871958 10790597500 -189594 022 (02)C> 01 1294817 10
== Executing PA-CTR 1, V(1)=1, V(2)=94814, repcount=47408, factor=3/2
1251222 24277035708 38 02142226 (02)C> 01 12 10
1251223 24277035711 35 02142226 <B(13) 11 12 10
1251224 24277320163 -284417 <B(13) 13142226 11 12 10
1251225 24277320170 -284414 02 (02)C> 13142226 11 12 10
1251226 24277604622 38 02142227 (02)C> 11 12 10
1251227 24277604624 40 02142228 (00)C> 12 10
1251228 24277604626 42 02142228 00 (02)A> 10
1251229 24277604628 44 02142228 00 02 (11)B>
Lines: 510
Top steps: 509
Macro steps: 1251229
Basic steps: 24277604628
Tape index: 44
nonzeros: 142231
log10(nonzeros): 5.153
log10(steps ): 10.385
Input to awk program:
gohalt 1
nbs 4
T 3-state 4-symbol #h (T.J. & S. Ligocki)
: >2.2x10^2372 >5.9x10^4744
5T 1RB 1RA 1LB 1RC 2LA 0LB 3LC 1RH 1LB 0RC 2RA 2RC
L 16
M 510
pref sim
machv Lig34_h just simple
machv Lig34_h-r with repetitions reduced
machv Lig34_h-1 with tape symbol exponents
machv Lig34_h-m as 2-bck-macro machine
machv Lig34_h-a as 2-bck-macro machine with pure additive config-TRs
iam Lig34_h-a
mtype 2 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:13:55 CEST 2010
edate Tue Jul 6 22:13:56 CEST 2010
bnspeed 1
short 7
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:13:55 CEST 2010