Comment: This TM produces >2.5x10^4561 nonzeros in >3.9x10^9122 steps.
| State | on 0 |
on 1 |
on 2 |
on 0 | on 1 | on 2 | ||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | |||||||
| A | 1RB | 2LD | 1RH | 1 | right | B | 2 | left | D | 1 | right | H |
| B | 2LC | 2RC | 2RB | 2 | left | C | 2 | right | C | 2 | right | B |
| C | 1LD | 0RC | 1RC | 1 | left | D | 0 | right | C | 1 | right | C |
| D | 2LA | 2LD | 0LB | 2 | left | A | 2 | left | D | 0 | left | B |
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 4 2 (1)C>
3 6 0 <D(2) 1
4 7 -1 <A(2) 2 1
5 9 1 1 (2)B> 2 1
6 10 2 1 2 (2)B> 1
7 11 3 1 22 (2)C>
8 13 1 1 22 <B(0) 1
9 17 3 1 2 1 (1)C> 1
10 18 4 1 2 12 (0)C>
11 20 2 1 2 12 <A(2) 1
12 21 1 1 2 1 <D(2) 2 1
13 22 0 1 2 <D(2) 22 1
14 23 -1 1 <B(0) 23 1
15 26 -2 <B(0) 1 23 1
16 27 -3 <C(2) 0 1 23 1
17 28 -4 <D(1) 2 0 1 23 1
18 29 -5 <A(2) 1 2 0 1 23 1
19 31 -3 1 (2)B> 1 2 0 1 23 1
20 32 -2 1 2 (2)C> 2 0 1 23 1
21 33 -1 1 22 (1)C> 0 1 23 1
22 35 -3 1 22 <D(2) 12 23 1
23 36 -4 1 2 <B(0) 2 12 23 1
24 40 -2 12 (1)C> 2 12 23 1
25 41 -1 13 (1)C> 12 23 1
26 42 0 14 (0)C> 1 23 1
27 43 1 14 0 (0)C> 23 1
28 44 2 14 02 (1)C> 22 1
29 46 4 14 02 12 (1)C> 1
30 47 5 14 02 13 (0)C>
31 49 3 14 02 13 <A(2) 1
32 50 2 14 02 12 <D(2) 2 1
33 52 0 14 02 <D(2) 23 1
34 53 -1 14 0 <A(2) 24 1
35 55 1 15 (2)B> 24 1
36 59 5 15 24 (2)B> 1
37 60 6 15 25 (2)C>
38 62 4 15 25 <B(0) 1
39 66 6 15 24 1 (1)C> 1
40 67 7 15 24 12 (0)C>
41 69 5 15 24 12 <A(2) 1
42 70 4 15 24 1 <D(2) 2 1
43 71 3 15 24 <D(2) 22 1
44 72 2 15 23 <B(0) 23 1
45 76 4 15 22 1 (1)C> 23 1
46 79 7 15 22 14 (1)C> 1
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 23+V(2) 11+V(1) (1)C> 1
1 1 1 [*]* 23+V(2) 12+V(1) (0)C>
2 3 -1 [*]* 23+V(2) 12+V(1) <A(2) 1
3 4 -2 [*]* 23+V(2) 11+V(1) <D(2) 2 1
4 5+V(1) -3+-1*V(1) [*]* 23+V(2) <D(2) 22+V(1) 1
5 6+V(1) -4+-1*V(1) [*]* 22+V(2) <B(0) 23+V(1) 1
6 10+V(1) -2+-1*V(1) [*]* 21+V(2) 1 (1)C> 23+V(1) 1
7 13+2*V(1) 1 [*]* 21+V(2) 14+V(1) (1)C> 1
<< Success! ==> defined new CTR 1 (PA)
47 80 8 15 22 15 (0)C>
48 82 6 15 22 15 <A(2) 1
49 83 5 15 22 14 <D(2) 2 1
50 87 1 15 22 <D(2) 25 1
51 88 0 15 2 <B(0) 26 1
52 92 2 16 (1)C> 26 1
53 98 8 112 (1)C> 1
54 99 9 113 (0)C>
55 101 7 113 <A(2) 1
56 102 6 112 <D(2) 2 1
57 114 -6 <D(2) 213 1
58 115 -7 <A(2) 214 1
59 117 -5 1 (2)B> 214 1
60 131 9 1 214 (2)B> 1
61 132 10 1 215 (2)C>
62 134 8 1 215 <B(0) 1
63 138 10 1 214 1 (1)C> 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(2) 22 11+V(1) (1)C> 1
1 1 1 11+V(2) 22 12+V(1) (0)C>
2 3 -1 11+V(2) 22 12+V(1) <A(2) 1
3 4 -2 11+V(2) 22 11+V(1) <D(2) 2 1
4 5+V(1) -3+-1*V(1) 11+V(2) 22 <D(2) 22+V(1) 1
5 6+V(1) -4+-1*V(1) 11+V(2) 2 <B(0) 23+V(1) 1
6 10+V(1) -2+-1*V(1) 12+V(2) (1)C> 23+V(1) 1
7 13+2*V(1) 1 15+V(1)+V(2) (1)C> 1
8 14+2*V(1) 2 16+V(1)+V(2) (0)C>
9 16+2*V(1) 0 16+V(1)+V(2) <A(2) 1
10 17+2*V(1) -1 15+V(1)+V(2) <D(2) 2 1
11 22+3*V(1)+V(2) -6+-1*V(1)+-1*V(2) <D(2) 26+V(1)+V(2) 1
12 23+3*V(1)+V(2) -7+-1*V(1)+-1*V(2) <A(2) 27+V(1)+V(2) 1
13 25+3*V(1)+V(2) -5+-1*V(1)+-1*V(2) 1 (2)B> 27+V(1)+V(2) 1
14 32+4*V(1)+2*V(2) 2 1 27+V(1)+V(2) (2)B> 1
15 33+4*V(1)+2*V(2) 3 1 28+V(1)+V(2) (2)C>
16 35+4*V(1)+2*V(2) 1 1 28+V(1)+V(2) <B(0) 1
17 39+4*V(1)+2*V(2) 3 1 27+V(1)+V(2) 1 (1)C> 1
<< Success! ==> defined new CTR 2 (PPA)
63 138 10 1 214 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=11, repcount=6, factor=3/2
105 306 16 1 22 119 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=18, V(2)=0
122 417 19 1 225 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=22, repcount=12, factor=3/2
206 969 31 1 2 137 (1)C> 1
207 970 32 1 2 138 (0)C>
208 972 30 1 2 138 <A(2) 1
209 973 29 1 2 137 <D(2) 2 1
210 1010 -8 1 2 <D(2) 238 1
211 1011 -9 1 <B(0) 239 1
212 1014 -10 <B(0) 1 239 1
213 1015 -11 <C(2) 0 1 239 1
214 1016 -12 <D(1) 2 0 1 239 1
215 1017 -13 <A(2) 1 2 0 1 239 1
216 1019 -11 1 (2)B> 1 2 0 1 239 1
217 1020 -10 1 2 (2)C> 2 0 1 239 1
218 1021 -9 1 22 (1)C> 0 1 239 1
219 1023 -11 1 22 <D(2) 12 239 1
220 1024 -12 1 2 <B(0) 2 12 239 1
221 1028 -10 12 (1)C> 2 12 239 1
222 1029 -9 13 (1)C> 12 239 1
223 1030 -8 14 (0)C> 1 239 1
224 1031 -7 14 0 (0)C> 239 1
225 1032 -6 14 02 (1)C> 238 1
226 1070 32 14 02 138 (1)C> 1
227 1071 33 14 02 139 (0)C>
228 1073 31 14 02 139 <A(2) 1
229 1074 30 14 02 138 <D(2) 2 1
230 1112 -8 14 02 <D(2) 239 1
231 1113 -9 14 0 <A(2) 240 1
232 1115 -7 15 (2)B> 240 1
233 1155 33 15 240 (2)B> 1
234 1156 34 15 241 (2)C>
235 1158 32 15 241 <B(0) 1
236 1162 34 15 240 1 (1)C> 1
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 1 2 11+V(1) (1)C> 1
1 1 1 1 2 12+V(1) (0)C>
2 3 -1 1 2 12+V(1) <A(2) 1
3 4 -2 1 2 11+V(1) <D(2) 2 1
4 5+V(1) -3+-1*V(1) 1 2 <D(2) 22+V(1) 1
5 6+V(1) -4+-1*V(1) 1 <B(0) 23+V(1) 1
6 9+V(1) -5+-1*V(1) <B(0) 1 23+V(1) 1
7 10+V(1) -6+-1*V(1) <C(2) 0 1 23+V(1) 1
8 11+V(1) -7+-1*V(1) <D(1) 2 0 1 23+V(1) 1
9 12+V(1) -8+-1*V(1) <A(2) 1 2 0 1 23+V(1) 1
10 14+V(1) -6+-1*V(1) 1 (2)B> 1 2 0 1 23+V(1) 1
11 15+V(1) -5+-1*V(1) 1 2 (2)C> 2 0 1 23+V(1) 1
12 16+V(1) -4+-1*V(1) 1 22 (1)C> 0 1 23+V(1) 1
13 18+V(1) -6+-1*V(1) 1 22 <D(2) 12 23+V(1) 1
14 19+V(1) -7+-1*V(1) 1 2 <B(0) 2 12 23+V(1) 1
15 23+V(1) -5+-1*V(1) 12 (1)C> 2 12 23+V(1) 1
16 24+V(1) -4+-1*V(1) 13 (1)C> 12 23+V(1) 1
17 25+V(1) -3+-1*V(1) 14 (0)C> 1 23+V(1) 1
18 26+V(1) -2+-1*V(1) 14 0 (0)C> 23+V(1) 1
19 27+V(1) -1+-1*V(1) 14 02 (1)C> 22+V(1) 1
20 29+2*V(1) 1 14 02 12+V(1) (1)C> 1
21 30+2*V(1) 2 14 02 13+V(1) (0)C>
22 32+2*V(1) 0 14 02 13+V(1) <A(2) 1
23 33+2*V(1) -1 14 02 12+V(1) <D(2) 2 1
24 35+3*V(1) -3+-1*V(1) 14 02 <D(2) 23+V(1) 1
25 36+3*V(1) -4+-1*V(1) 14 0 <A(2) 24+V(1) 1
26 38+3*V(1) -2+-1*V(1) 15 (2)B> 24+V(1) 1
27 42+4*V(1) 2 15 24+V(1) (2)B> 1
28 43+4*V(1) 3 15 25+V(1) (2)C>
29 45+4*V(1) 1 15 25+V(1) <B(0) 1
30 49+4*V(1) 3 15 24+V(1) 1 (1)C> 1
<< Success! ==> defined new CTR 3 (PPA)
236 1162 34 15 240 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=37, repcount=19, factor=3/2
369 2435 53 15 22 158 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=57, V(2)=4
386 2710 56 1 268 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=65, repcount=33, factor=3/2
617 6307 89 1 22 1100 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=99, V(2)=0
634 6742 92 1 2106 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=103, repcount=52, factor=3/2
998 15374 144 1 22 1157 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=156, V(2)=0
1015 16037 147 1 2163 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=160, repcount=81, factor=3/2
1582 36530 228 1 2 1244 (1)C> 1
== Executing PPA-CTR 3 (once), V(1)=243
1612 37551 231 15 2247 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=244, repcount=123, factor=3/2
2473 84168 354 15 2 1370 (1)C> 1
2474 84169 355 15 2 1371 (0)C>
2475 84171 353 15 2 1371 <A(2) 1
2476 84172 352 15 2 1370 <D(2) 2 1
2477 84542 -18 15 2 <D(2) 2371 1
2478 84543 -19 15 <B(0) 2372 1
2479 84558 -24 <B(0) 15 2372 1
2480 84559 -25 <C(2) 0 15 2372 1
2481 84560 -26 <D(1) 2 0 15 2372 1
2482 84561 -27 <A(2) 1 2 0 15 2372 1
2483 84563 -25 1 (2)B> 1 2 0 15 2372 1
2484 84564 -24 1 2 (2)C> 2 0 15 2372 1
2485 84565 -23 1 22 (1)C> 0 15 2372 1
2486 84567 -25 1 22 <D(2) 16 2372 1
2487 84568 -26 1 2 <B(0) 2 16 2372 1
2488 84572 -24 12 (1)C> 2 16 2372 1
2489 84573 -23 13 (1)C> 16 2372 1
2490 84574 -22 14 (0)C> 15 2372 1
2491 84579 -17 14 05 (0)C> 2372 1
2492 84580 -16 14 06 (1)C> 2371 1
2493 84951 355 14 06 1371 (1)C> 1
2494 84952 356 14 06 1372 (0)C>
2495 84954 354 14 06 1372 <A(2) 1
2496 84955 353 14 06 1371 <D(2) 2 1
2497 85326 -18 14 06 <D(2) 2372 1
2498 85327 -19 14 05 <A(2) 2373 1
2499 85329 -17 14 04 1 (2)B> 2373 1
2500 85702 356 14 04 1 2373 (2)B> 1
2501 85703 357 14 04 1 2374 (2)C>
2502 85705 355 14 04 1 2374 <B(0) 1
2503 85709 357 14 04 1 2373 1 (1)C> 1
2504 85710 358 14 04 1 2373 12 (0)C>
2505 85712 356 14 04 1 2373 12 <A(2) 1
2506 85713 355 14 04 1 2373 1 <D(2) 2 1
2507 85714 354 14 04 1 2373 <D(2) 22 1
2508 85715 353 14 04 1 2372 <B(0) 23 1
2509 85719 355 14 04 1 2371 1 (1)C> 23 1
2510 85722 358 14 04 1 2371 14 (1)C> 1
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* 23+V(2) 11+V(1) (1)C> 1
1 1 1 [*]* [*]* [*]* 23+V(2) 12+V(1) (0)C>
2 3 -1 [*]* [*]* [*]* 23+V(2) 12+V(1) <A(2) 1
3 4 -2 [*]* [*]* [*]* 23+V(2) 11+V(1) <D(2) 2 1
4 5+V(1) -3+-1*V(1) [*]* [*]* [*]* 23+V(2) <D(2) 22+V(1) 1
5 6+V(1) -4+-1*V(1) [*]* [*]* [*]* 22+V(2) <B(0) 23+V(1) 1
6 10+V(1) -2+-1*V(1) [*]* [*]* [*]* 21+V(2) 1 (1)C> 23+V(1) 1
7 13+2*V(1) 1 [*]* [*]* [*]* 21+V(2) 14+V(1) (1)C> 1
<< Success! ==> defined new CTR 4 (PA)
2510 85722 358 14 04 1 2371 14 (1)C> 1
== Executing PA-CTR 4, V(1)=3, V(2)=368, repcount=185, factor=3/2
3805 191357 543 14 04 1 2 1559 (1)C> 1
3806 191358 544 14 04 1 2 1560 (0)C>
3807 191360 542 14 04 1 2 1560 <A(2) 1
3808 191361 541 14 04 1 2 1559 <D(2) 2 1
3809 191920 -18 14 04 1 2 <D(2) 2560 1
3810 191921 -19 14 04 1 <B(0) 2561 1
3811 191924 -20 14 04 <B(0) 1 2561 1
3812 191925 -21 14 03 <C(2) 0 1 2561 1
3813 191926 -22 14 02 <D(1) 2 0 1 2561 1
3814 191927 -23 14 0 <A(2) 1 2 0 1 2561 1
3815 191929 -21 15 (2)B> 1 2 0 1 2561 1
3816 191930 -20 15 2 (2)C> 2 0 1 2561 1
3817 191931 -19 15 22 (1)C> 0 1 2561 1
3818 191933 -21 15 22 <D(2) 12 2561 1
3819 191934 -22 15 2 <B(0) 2 12 2561 1
3820 191938 -20 16 (1)C> 2 12 2561 1
3821 191939 -19 17 (1)C> 12 2561 1
3822 191940 -18 18 (0)C> 1 2561 1
3823 191941 -17 18 0 (0)C> 2561 1
3824 191942 -16 18 02 (1)C> 2560 1
3825 192502 544 18 02 1560 (1)C> 1
3826 192503 545 18 02 1561 (0)C>
3827 192505 543 18 02 1561 <A(2) 1
3828 192506 542 18 02 1560 <D(2) 2 1
3829 193066 -18 18 02 <D(2) 2561 1
3830 193067 -19 18 0 <A(2) 2562 1
3831 193069 -17 19 (2)B> 2562 1
3832 193631 545 19 2562 (2)B> 1
3833 193632 546 19 2563 (2)C>
3834 193634 544 19 2563 <B(0) 1
3835 193638 546 19 2562 1 (1)C> 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 11+V(2) 04 1 2 11+V(1) (1)C> 1
1 1 1 11+V(2) 04 1 2 12+V(1) (0)C>
2 3 -1 11+V(2) 04 1 2 12+V(1) <A(2) 1
3 4 -2 11+V(2) 04 1 2 11+V(1) <D(2) 2 1
4 5+V(1) -3+-1*V(1) 11+V(2) 04 1 2 <D(2) 22+V(1) 1
5 6+V(1) -4+-1*V(1) 11+V(2) 04 1 <B(0) 23+V(1) 1
6 9+V(1) -5+-1*V(1) 11+V(2) 04 <B(0) 1 23+V(1) 1
7 10+V(1) -6+-1*V(1) 11+V(2) 03 <C(2) 0 1 23+V(1) 1
8 11+V(1) -7+-1*V(1) 11+V(2) 02 <D(1) 2 0 1 23+V(1) 1
9 12+V(1) -8+-1*V(1) 11+V(2) 0 <A(2) 1 2 0 1 23+V(1) 1
10 14+V(1) -6+-1*V(1) 12+V(2) (2)B> 1 2 0 1 23+V(1) 1
11 15+V(1) -5+-1*V(1) 12+V(2) 2 (2)C> 2 0 1 23+V(1) 1
12 16+V(1) -4+-1*V(1) 12+V(2) 22 (1)C> 0 1 23+V(1) 1
13 18+V(1) -6+-1*V(1) 12+V(2) 22 <D(2) 12 23+V(1) 1
14 19+V(1) -7+-1*V(1) 12+V(2) 2 <B(0) 2 12 23+V(1) 1
15 23+V(1) -5+-1*V(1) 13+V(2) (1)C> 2 12 23+V(1) 1
16 24+V(1) -4+-1*V(1) 14+V(2) (1)C> 12 23+V(1) 1
17 25+V(1) -3+-1*V(1) 15+V(2) (0)C> 1 23+V(1) 1
18 26+V(1) -2+-1*V(1) 15+V(2) 0 (0)C> 23+V(1) 1
19 27+V(1) -1+-1*V(1) 15+V(2) 02 (1)C> 22+V(1) 1
20 29+2*V(1) 1 15+V(2) 02 12+V(1) (1)C> 1
21 30+2*V(1) 2 15+V(2) 02 13+V(1) (0)C>
22 32+2*V(1) 0 15+V(2) 02 13+V(1) <A(2) 1
23 33+2*V(1) -1 15+V(2) 02 12+V(1) <D(2) 2 1
24 35+3*V(1) -3+-1*V(1) 15+V(2) 02 <D(2) 23+V(1) 1
25 36+3*V(1) -4+-1*V(1) 15+V(2) 0 <A(2) 24+V(1) 1
26 38+3*V(1) -2+-1*V(1) 16+V(2) (2)B> 24+V(1) 1
27 42+4*V(1) 2 16+V(2) 24+V(1) (2)B> 1
28 43+4*V(1) 3 16+V(2) 25+V(1) (2)C>
29 45+4*V(1) 1 16+V(2) 25+V(1) <B(0) 1
30 49+4*V(1) 3 16+V(2) 24+V(1) 1 (1)C> 1
<< Success! ==> defined new CTR 5 (PPA)
3835 193638 546 19 2562 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=559, repcount=280, factor=3/2
5795 431638 826 19 22 1841 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=840, V(2)=8
5812 435053 829 1 2855 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=852, repcount=427, factor=3/2
8801 986310 1256 1 2 11282 (1)C> 1
== Executing PPA-CTR 3 (once), V(1)=1281
8831 991483 1259 15 21285 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=1282, repcount=642, factor=3/2
13325 2234395 1901 15 2 11927 (1)C> 1
13326 2234396 1902 15 2 11928 (0)C>
13327 2234398 1900 15 2 11928 <A(2) 1
13328 2234399 1899 15 2 11927 <D(2) 2 1
13329 2236326 -28 15 2 <D(2) 21928 1
13330 2236327 -29 15 <B(0) 21929 1
13331 2236342 -34 <B(0) 15 21929 1
13332 2236343 -35 <C(2) 0 15 21929 1
13333 2236344 -36 <D(1) 2 0 15 21929 1
13334 2236345 -37 <A(2) 1 2 0 15 21929 1
13335 2236347 -35 1 (2)B> 1 2 0 15 21929 1
13336 2236348 -34 1 2 (2)C> 2 0 15 21929 1
13337 2236349 -33 1 22 (1)C> 0 15 21929 1
13338 2236351 -35 1 22 <D(2) 16 21929 1
13339 2236352 -36 1 2 <B(0) 2 16 21929 1
13340 2236356 -34 12 (1)C> 2 16 21929 1
13341 2236357 -33 13 (1)C> 16 21929 1
13342 2236358 -32 14 (0)C> 15 21929 1
13343 2236363 -27 14 05 (0)C> 21929 1
13344 2236364 -26 14 06 (1)C> 21928 1
13345 2238292 1902 14 06 11928 (1)C> 1
13346 2238293 1903 14 06 11929 (0)C>
13347 2238295 1901 14 06 11929 <A(2) 1
13348 2238296 1900 14 06 11928 <D(2) 2 1
13349 2240224 -28 14 06 <D(2) 21929 1
13350 2240225 -29 14 05 <A(2) 21930 1
13351 2240227 -27 14 04 1 (2)B> 21930 1
13352 2242157 1903 14 04 1 21930 (2)B> 1
13353 2242158 1904 14 04 1 21931 (2)C>
13354 2242160 1902 14 04 1 21931 <B(0) 1
13355 2242164 1904 14 04 1 21930 1 (1)C> 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 12+V(2) 2 11+V(1) (1)C> 1
1 1 1 12+V(2) 2 12+V(1) (0)C>
2 3 -1 12+V(2) 2 12+V(1) <A(2) 1
3 4 -2 12+V(2) 2 11+V(1) <D(2) 2 1
4 5+V(1) -3+-1*V(1) 12+V(2) 2 <D(2) 22+V(1) 1
5 6+V(1) -4+-1*V(1) 12+V(2) <B(0) 23+V(1) 1
6 12+V(1)+3*V(2) -6+-1*V(1)+-1*V(2) <B(0) 12+V(2) 23+V(1) 1
7 13+V(1)+3*V(2) -7+-1*V(1)+-1*V(2) <C(2) 0 12+V(2) 23+V(1) 1
8 14+V(1)+3*V(2) -8+-1*V(1)+-1*V(2) <D(1) 2 0 12+V(2) 23+V(1) 1
9 15+V(1)+3*V(2) -9+-1*V(1)+-1*V(2) <A(2) 1 2 0 12+V(2) 23+V(1) 1
10 17+V(1)+3*V(2) -7+-1*V(1)+-1*V(2) 1 (2)B> 1 2 0 12+V(2) 23+V(1) 1
11 18+V(1)+3*V(2) -6+-1*V(1)+-1*V(2) 1 2 (2)C> 2 0 12+V(2) 23+V(1) 1
12 19+V(1)+3*V(2) -5+-1*V(1)+-1*V(2) 1 22 (1)C> 0 12+V(2) 23+V(1) 1
13 21+V(1)+3*V(2) -7+-1*V(1)+-1*V(2) 1 22 <D(2) 13+V(2) 23+V(1) 1
14 22+V(1)+3*V(2) -8+-1*V(1)+-1*V(2) 1 2 <B(0) 2 13+V(2) 23+V(1) 1
15 26+V(1)+3*V(2) -6+-1*V(1)+-1*V(2) 12 (1)C> 2 13+V(2) 23+V(1) 1
16 27+V(1)+3*V(2) -5+-1*V(1)+-1*V(2) 13 (1)C> 13+V(2) 23+V(1) 1
17 28+V(1)+3*V(2) -4+-1*V(1)+-1*V(2) 14 (0)C> 12+V(2) 23+V(1) 1
18 30+V(1)+4*V(2) -2+-1*V(1) 14 02+V(2) (0)C> 23+V(1) 1
19 31+V(1)+4*V(2) -1+-1*V(1) 14 03+V(2) (1)C> 22+V(1) 1
20 33+2*V(1)+4*V(2) 1 14 03+V(2) 12+V(1) (1)C> 1
21 34+2*V(1)+4*V(2) 2 14 03+V(2) 13+V(1) (0)C>
22 36+2*V(1)+4*V(2) 0 14 03+V(2) 13+V(1) <A(2) 1
23 37+2*V(1)+4*V(2) -1 14 03+V(2) 12+V(1) <D(2) 2 1
24 39+3*V(1)+4*V(2) -3+-1*V(1) 14 03+V(2) <D(2) 23+V(1) 1
25 40+3*V(1)+4*V(2) -4+-1*V(1) 14 02+V(2) <A(2) 24+V(1) 1
26 42+3*V(1)+4*V(2) -2+-1*V(1) 14 01+V(2) 1 (2)B> 24+V(1) 1
27 46+4*V(1)+4*V(2) 2 14 01+V(2) 1 24+V(1) (2)B> 1
28 47+4*V(1)+4*V(2) 3 14 01+V(2) 1 25+V(1) (2)C>
29 49+4*V(1)+4*V(2) 1 14 01+V(2) 1 25+V(1) <B(0) 1
30 53+4*V(1)+4*V(2) 3 14 01+V(2) 1 24+V(1) 1 (1)C> 1
<< Success! ==> defined new CTR 6 (PPA)
13355 2242164 1904 14 04 1 21930 1 (1)C> 1
== Executing PA-CTR 4, V(1)=0, V(2)=1927, repcount=964, factor=3/2
20103 5039692 2868 14 04 1 22 12893 (1)C> 1
20104 5039693 2869 14 04 1 22 12894 (0)C>
20105 5039695 2867 14 04 1 22 12894 <A(2) 1
20106 5039696 2866 14 04 1 22 12893 <D(2) 2 1
20107 5042589 -27 14 04 1 22 <D(2) 22894 1
20108 5042590 -28 14 04 1 2 <B(0) 22895 1
20109 5042594 -26 14 04 12 (1)C> 22895 1
20110 5045489 2869 14 04 12897 (1)C> 1
20111 5045490 2870 14 04 12898 (0)C>
20112 5045492 2868 14 04 12898 <A(2) 1
20113 5045493 2867 14 04 12897 <D(2) 2 1
20114 5048390 -30 14 04 <D(2) 22898 1
20115 5048391 -31 14 03 <A(2) 22899 1
20116 5048393 -29 14 02 1 (2)B> 22899 1
20117 5051292 2870 14 02 1 22899 (2)B> 1
20118 5051293 2871 14 02 1 22900 (2)C>
20119 5051295 2869 14 02 1 22900 <B(0) 1
20120 5051299 2871 14 02 1 22899 1 (1)C> 1
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 [*]* 03+V(3) 11+V(2) 22 11+V(1) (1)C> 1
1 1 1 [*]* 03+V(3) 11+V(2) 22 12+V(1) (0)C>
2 3 -1 [*]* 03+V(3) 11+V(2) 22 12+V(1) <A(2) 1
3 4 -2 [*]* 03+V(3) 11+V(2) 22 11+V(1) <D(2) 2 1
4 5+V(1) -3+-1*V(1) [*]* 03+V(3) 11+V(2) 22 <D(2) 22+V(1) 1
5 6+V(1) -4+-1*V(1) [*]* 03+V(3) 11+V(2) 2 <B(0) 23+V(1) 1
6 10+V(1) -2+-1*V(1) [*]* 03+V(3) 12+V(2) (1)C> 23+V(1) 1
7 13+2*V(1) 1 [*]* 03+V(3) 15+V(1)+V(2) (1)C> 1
8 14+2*V(1) 2 [*]* 03+V(3) 16+V(1)+V(2) (0)C>
9 16+2*V(1) 0 [*]* 03+V(3) 16+V(1)+V(2) <A(2) 1
10 17+2*V(1) -1 [*]* 03+V(3) 15+V(1)+V(2) <D(2) 2 1
11 22+3*V(1)+V(2) -6+-1*V(1)+-1*V(2) [*]* 03+V(3) <D(2) 26+V(1)+V(2) 1
12 23+3*V(1)+V(2) -7+-1*V(1)+-1*V(2) [*]* 02+V(3) <A(2) 27+V(1)+V(2) 1
13 25+3*V(1)+V(2) -5+-1*V(1)+-1*V(2) [*]* 01+V(3) 1 (2)B> 27+V(1)+V(2) 1
14 32+4*V(1)+2*V(2) 2 [*]* 01+V(3) 1 27+V(1)+V(2) (2)B> 1
15 33+4*V(1)+2*V(2) 3 [*]* 01+V(3) 1 28+V(1)+V(2) (2)C>
16 35+4*V(1)+2*V(2) 1 [*]* 01+V(3) 1 28+V(1)+V(2) <B(0) 1
17 39+4*V(1)+2*V(2) 3 [*]* 01+V(3) 1 27+V(1)+V(2) 1 (1)C> 1
<< Success! ==> defined new CTR 7 (PPA)
20120 5051299 2871 14 02 1 22899 1 (1)C> 1
== Executing PA-CTR 4, V(1)=0, V(2)=2896, repcount=1449, factor=3/2
30263 11364592 4320 14 02 1 2 14348 (1)C> 1
30264 11364593 4321 14 02 1 2 14349 (0)C>
30265 11364595 4319 14 02 1 2 14349 <A(2) 1
30266 11364596 4318 14 02 1 2 14348 <D(2) 2 1
30267 11368944 -30 14 02 1 2 <D(2) 24349 1
30268 11368945 -31 14 02 1 <B(0) 24350 1
30269 11368948 -32 14 02 <B(0) 1 24350 1
30270 11368949 -33 14 0 <C(2) 0 1 24350 1
30271 11368950 -34 14 <D(1) 2 0 1 24350 1
30272 11368951 -35 13 <D(2) 1 2 0 1 24350 1
30273 11368954 -38 <D(2) 23 1 2 0 1 24350 1
30274 11368955 -39 <A(2) 24 1 2 0 1 24350 1
30275 11368957 -37 1 (2)B> 24 1 2 0 1 24350 1
30276 11368961 -33 1 24 (2)B> 1 2 0 1 24350 1
30277 11368962 -32 1 25 (2)C> 2 0 1 24350 1
30278 11368963 -31 1 26 (1)C> 0 1 24350 1
30279 11368965 -33 1 26 <D(2) 12 24350 1
30280 11368966 -34 1 25 <B(0) 2 12 24350 1
30281 11368970 -32 1 24 1 (1)C> 2 12 24350 1
30282 11368971 -31 1 24 12 (1)C> 12 24350 1
30283 11368972 -30 1 24 13 (0)C> 1 24350 1
30284 11368973 -29 1 24 13 0 (0)C> 24350 1
30285 11368974 -28 1 24 13 02 (1)C> 24349 1
30286 11373323 4321 1 24 13 02 14349 (1)C> 1
30287 11373324 4322 1 24 13 02 14350 (0)C>
30288 11373326 4320 1 24 13 02 14350 <A(2) 1
30289 11373327 4319 1 24 13 02 14349 <D(2) 2 1
30290 11377676 -30 1 24 13 02 <D(2) 24350 1
30291 11377677 -31 1 24 13 0 <A(2) 24351 1
30292 11377679 -29 1 24 14 (2)B> 24351 1
30293 11382030 4322 1 24 14 24351 (2)B> 1
30294 11382031 4323 1 24 14 24352 (2)C>
30295 11382033 4321 1 24 14 24352 <B(0) 1
30296 11382037 4323 1 24 14 24351 1 (1)C> 1
>> Try to prove a PPA-CTR with 2 Vars...
0 0 0 12+V(2) 02 1 2 11+V(1) (1)C> 1
1 1 1 12+V(2) 02 1 2 12+V(1) (0)C>
2 3 -1 12+V(2) 02 1 2 12+V(1) <A(2) 1
3 4 -2 12+V(2) 02 1 2 11+V(1) <D(2) 2 1
4 5+V(1) -3+-1*V(1) 12+V(2) 02 1 2 <D(2) 22+V(1) 1
5 6+V(1) -4+-1*V(1) 12+V(2) 02 1 <B(0) 23+V(1) 1
6 9+V(1) -5+-1*V(1) 12+V(2) 02 <B(0) 1 23+V(1) 1
7 10+V(1) -6+-1*V(1) 12+V(2) 0 <C(2) 0 1 23+V(1) 1
8 11+V(1) -7+-1*V(1) 12+V(2) <D(1) 2 0 1 23+V(1) 1
9 12+V(1) -8+-1*V(1) 11+V(2) <D(2) 1 2 0 1 23+V(1) 1
10 13+V(1)+V(2) -9+-1*V(1)+-1*V(2) <D(2) 21+V(2) 1 2 0 1 23+V(1) 1
11 14+V(1)+V(2) -10+-1*V(1)+-1*V(2) <A(2) 22+V(2) 1 2 0 1 23+V(1) 1
12 16+V(1)+V(2) -8+-1*V(1)+-1*V(2) 1 (2)B> 22+V(2) 1 2 0 1 23+V(1) 1
13 18+V(1)+2*V(2) -6+-1*V(1) 1 22+V(2) (2)B> 1 2 0 1 23+V(1) 1
14 19+V(1)+2*V(2) -5+-1*V(1) 1 23+V(2) (2)C> 2 0 1 23+V(1) 1
15 20+V(1)+2*V(2) -4+-1*V(1) 1 24+V(2) (1)C> 0 1 23+V(1) 1
16 22+V(1)+2*V(2) -6+-1*V(1) 1 24+V(2) <D(2) 12 23+V(1) 1
17 23+V(1)+2*V(2) -7+-1*V(1) 1 23+V(2) <B(0) 2 12 23+V(1) 1
18 27+V(1)+2*V(2) -5+-1*V(1) 1 22+V(2) 1 (1)C> 2 12 23+V(1) 1
19 28+V(1)+2*V(2) -4+-1*V(1) 1 22+V(2) 12 (1)C> 12 23+V(1) 1
20 29+V(1)+2*V(2) -3+-1*V(1) 1 22+V(2) 13 (0)C> 1 23+V(1) 1
21 30+V(1)+2*V(2) -2+-1*V(1) 1 22+V(2) 13 0 (0)C> 23+V(1) 1
22 31+V(1)+2*V(2) -1+-1*V(1) 1 22+V(2) 13 02 (1)C> 22+V(1) 1
23 33+2*V(1)+2*V(2) 1 1 22+V(2) 13 02 12+V(1) (1)C> 1
24 34+2*V(1)+2*V(2) 2 1 22+V(2) 13 02 13+V(1) (0)C>
25 36+2*V(1)+2*V(2) 0 1 22+V(2) 13 02 13+V(1) <A(2) 1
26 37+2*V(1)+2*V(2) -1 1 22+V(2) 13 02 12+V(1) <D(2) 2 1
27 39+3*V(1)+2*V(2) -3+-1*V(1) 1 22+V(2) 13 02 <D(2) 23+V(1) 1
28 40+3*V(1)+2*V(2) -4+-1*V(1) 1 22+V(2) 13 0 <A(2) 24+V(1) 1
29 42+3*V(1)+2*V(2) -2+-1*V(1) 1 22+V(2) 14 (2)B> 24+V(1) 1
30 46+4*V(1)+2*V(2) 2 1 22+V(2) 14 24+V(1) (2)B> 1
31 47+4*V(1)+2*V(2) 3 1 22+V(2) 14 25+V(1) (2)C>
32 49+4*V(1)+2*V(2) 1 1 22+V(2) 14 25+V(1) <B(0) 1
33 53+4*V(1)+2*V(2) 3 1 22+V(2) 14 24+V(1) 1 (1)C> 1
<< Success! ==> defined new CTR 8 (PPA)
30296 11382037 4323 1 24 14 24351 1 (1)C> 1
== Executing PA-CTR 4, V(1)=0, V(2)=4348, repcount=2175, factor=3/2
45521 25595662 6498 1 24 14 2 16526 (1)C> 1
45522 25595663 6499 1 24 14 2 16527 (0)C>
45523 25595665 6497 1 24 14 2 16527 <A(2) 1
45524 25595666 6496 1 24 14 2 16526 <D(2) 2 1
45525 25602192 -30 1 24 14 2 <D(2) 26527 1
45526 25602193 -31 1 24 14 <B(0) 26528 1
45527 25602205 -35 1 24 <B(0) 14 26528 1
45528 25602209 -33 1 23 1 (1)C> 14 26528 1
45529 25602210 -32 1 23 12 (0)C> 13 26528 1
45530 25602213 -29 1 23 12 03 (0)C> 26528 1
45531 25602214 -28 1 23 12 04 (1)C> 26527 1
45532 25608741 6499 1 23 12 04 16527 (1)C> 1
45533 25608742 6500 1 23 12 04 16528 (0)C>
45534 25608744 6498 1 23 12 04 16528 <A(2) 1
45535 25608745 6497 1 23 12 04 16527 <D(2) 2 1
45536 25615272 -30 1 23 12 04 <D(2) 26528 1
45537 25615273 -31 1 23 12 03 <A(2) 26529 1
45538 25615275 -29 1 23 12 02 1 (2)B> 26529 1
45539 25621804 6500 1 23 12 02 1 26529 (2)B> 1
45540 25621805 6501 1 23 12 02 1 26530 (2)C>
45541 25621807 6499 1 23 12 02 1 26530 <B(0) 1
45542 25621811 6501 1 23 12 02 1 26529 1 (1)C> 1
45543 25621812 6502 1 23 12 02 1 26529 12 (0)C>
45544 25621814 6500 1 23 12 02 1 26529 12 <A(2) 1
45545 25621815 6499 1 23 12 02 1 26529 1 <D(2) 2 1
45546 25621816 6498 1 23 12 02 1 26529 <D(2) 22 1
45547 25621817 6497 1 23 12 02 1 26528 <B(0) 23 1
45548 25621821 6499 1 23 12 02 1 26527 1 (1)C> 23 1
45549 25621824 6502 1 23 12 02 1 26527 14 (1)C> 1
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* [*]* [*]* [*]* [*]* 23+V(2) 11+V(1) (1)C> 1
1 1 1 [*]* [*]* [*]* [*]* [*]* 23+V(2) 12+V(1) (0)C>
2 3 -1 [*]* [*]* [*]* [*]* [*]* 23+V(2) 12+V(1) <A(2) 1
3 4 -2 [*]* [*]* [*]* [*]* [*]* 23+V(2) 11+V(1) <D(2) 2 1
4 5+V(1) -3+-1*V(1) [*]* [*]* [*]* [*]* [*]* 23+V(2) <D(2) 22+V(1) 1
5 6+V(1) -4+-1*V(1) [*]* [*]* [*]* [*]* [*]* 22+V(2) <B(0) 23+V(1) 1
6 10+V(1) -2+-1*V(1) [*]* [*]* [*]* [*]* [*]* 21+V(2) 1 (1)C> 23+V(1) 1
7 13+2*V(1) 1 [*]* [*]* [*]* [*]* [*]* 21+V(2) 14+V(1) (1)C> 1
<< Success! ==> defined new CTR 9 (PA)
45549 25621824 6502 1 23 12 02 1 26527 14 (1)C> 1
== Executing PA-CTR 9, V(1)=3, V(2)=6524, repcount=3263, factor=3/2
68390 57615539 9765 1 23 12 02 1 2 19793 (1)C> 1
68391 57615540 9766 1 23 12 02 1 2 19794 (0)C>
68392 57615542 9764 1 23 12 02 1 2 19794 <A(2) 1
68393 57615543 9763 1 23 12 02 1 2 19793 <D(2) 2 1
68394 57625336 -30 1 23 12 02 1 2 <D(2) 29794 1
68395 57625337 -31 1 23 12 02 1 <B(0) 29795 1
68396 57625340 -32 1 23 12 02 <B(0) 1 29795 1
68397 57625341 -33 1 23 12 0 <C(2) 0 1 29795 1
68398 57625342 -34 1 23 12 <D(1) 2 0 1 29795 1
68399 57625343 -35 1 23 1 <D(2) 1 2 0 1 29795 1
68400 57625344 -36 1 23 <D(2) 2 1 2 0 1 29795 1
68401 57625345 -37 1 22 <B(0) 22 1 2 0 1 29795 1
68402 57625349 -35 1 2 1 (1)C> 22 1 2 0 1 29795 1
68403 57625351 -33 1 2 13 (1)C> 1 2 0 1 29795 1
68404 57625352 -32 1 2 14 (0)C> 2 0 1 29795 1
68405 57625353 -31 1 2 14 0 (1)C> 0 1 29795 1
68406 57625355 -33 1 2 14 0 <D(2) 12 29795 1
68407 57625356 -34 1 2 14 <A(2) 2 12 29795 1
68408 57625357 -35 1 2 13 <D(2) 22 12 29795 1
68409 57625360 -38 1 2 <D(2) 25 12 29795 1
68410 57625361 -39 1 <B(0) 26 12 29795 1
68411 57625364 -40 <B(0) 1 26 12 29795 1
68412 57625365 -41 <C(2) 0 1 26 12 29795 1
68413 57625366 -42 <D(1) 2 0 1 26 12 29795 1
68414 57625367 -43 <A(2) 1 2 0 1 26 12 29795 1
68415 57625369 -41 1 (2)B> 1 2 0 1 26 12 29795 1
68416 57625370 -40 1 2 (2)C> 2 0 1 26 12 29795 1
68417 57625371 -39 1 22 (1)C> 0 1 26 12 29795 1
68418 57625373 -41 1 22 <D(2) 12 26 12 29795 1
68419 57625374 -42 1 2 <B(0) 2 12 26 12 29795 1
68420 57625378 -40 12 (1)C> 2 12 26 12 29795 1
68421 57625379 -39 13 (1)C> 12 26 12 29795 1
68422 57625380 -38 14 (0)C> 1 26 12 29795 1
68423 57625381 -37 14 0 (0)C> 26 12 29795 1
68424 57625382 -36 14 02 (1)C> 25 12 29795 1
68425 57625387 -31 14 02 15 (1)C> 12 29795 1
68426 57625388 -30 14 02 16 (0)C> 1 29795 1
68427 57625389 -29 14 02 16 0 (0)C> 29795 1
68428 57625390 -28 14 02 16 02 (1)C> 29794 1
68429 57635184 9766 14 02 16 02 19794 (1)C> 1
68430 57635185 9767 14 02 16 02 19795 (0)C>
68431 57635187 9765 14 02 16 02 19795 <A(2) 1
68432 57635188 9764 14 02 16 02 19794 <D(2) 2 1
68433 57644982 -30 14 02 16 02 <D(2) 29795 1
68434 57644983 -31 14 02 16 0 <A(2) 29796 1
68435 57644985 -29 14 02 17 (2)B> 29796 1
68436 57654781 9767 14 02 17 29796 (2)B> 1
68437 57654782 9768 14 02 17 29797 (2)C>
68438 57654784 9766 14 02 17 29797 <B(0) 1
68439 57654788 9768 14 02 17 29796 1 (1)C> 1
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 11+V(3) 23 12+V(2) 02 1 2 11+V(1) (1)C> 1
1 1 1 11+V(3) 23 12+V(2) 02 1 2 12+V(1) (0)C>
2 3 -1 11+V(3) 23 12+V(2) 02 1 2 12+V(1) <A(2) 1
3 4 -2 11+V(3) 23 12+V(2) 02 1 2 11+V(1) <D(2) 2 1
4 5+V(1) -3+-1*V(1) 11+V(3) 23 12+V(2) 02 1 2 <D(2) 22+V(1) 1
5 6+V(1) -4+-1*V(1) 11+V(3) 23 12+V(2) 02 1 <B(0) 23+V(1) 1
6 9+V(1) -5+-1*V(1) 11+V(3) 23 12+V(2) 02 <B(0) 1 23+V(1) 1
7 10+V(1) -6+-1*V(1) 11+V(3) 23 12+V(2) 0 <C(2) 0 1 23+V(1) 1
8 11+V(1) -7+-1*V(1) 11+V(3) 23 12+V(2) <D(1) 2 0 1 23+V(1) 1
9 12+V(1) -8+-1*V(1) 11+V(3) 23 11+V(2) <D(2) 1 2 0 1 23+V(1) 1
10 13+V(1)+V(2) -9+-1*V(1)+-1*V(2) 11+V(3) 23 <D(2) 21+V(2) 1 2 0 1 23+V(1) 1
11 14+V(1)+V(2) -10+-1*V(1)+-1*V(2) 11+V(3) 22 <B(0) 22+V(2) 1 2 0 1 23+V(1) 1
12 18+V(1)+V(2) -8+-1*V(1)+-1*V(2) 11+V(3) 2 1 (1)C> 22+V(2) 1 2 0 1 23+V(1) 1
13 20+V(1)+2*V(2) -6+-1*V(1) 11+V(3) 2 13+V(2) (1)C> 1 2 0 1 23+V(1) 1
14 21+V(1)+2*V(2) -5+-1*V(1) 11+V(3) 2 14+V(2) (0)C> 2 0 1 23+V(1) 1
15 22+V(1)+2*V(2) -4+-1*V(1) 11+V(3) 2 14+V(2) 0 (1)C> 0 1 23+V(1) 1
16 24+V(1)+2*V(2) -6+-1*V(1) 11+V(3) 2 14+V(2) 0 <D(2) 12 23+V(1) 1
17 25+V(1)+2*V(2) -7+-1*V(1) 11+V(3) 2 14+V(2) <A(2) 2 12 23+V(1) 1
18 26+V(1)+2*V(2) -8+-1*V(1) 11+V(3) 2 13+V(2) <D(2) 22 12 23+V(1) 1
19 29+V(1)+3*V(2) -11+-1*V(1)+-1*V(2) 11+V(3) 2 <D(2) 25+V(2) 12 23+V(1) 1
20 30+V(1)+3*V(2) -12+-1*V(1)+-1*V(2) 11+V(3) <B(0) 26+V(2) 12 23+V(1) 1
21 33+V(1)+3*V(2)+3*V(3) -13+-1*V(1)+-1*V(2)+-1*V(3) <B(0) 11+V(3) 26+V(2) 12 23+V(1) 1
22 34+V(1)+3*V(2)+3*V(3) -14+-1*V(1)+-1*V(2)+-1*V(3) <C(2) 0 11+V(3) 26+V(2) 12 23+V(1) 1
23 35+V(1)+3*V(2)+3*V(3) -15+-1*V(1)+-1*V(2)+-1*V(3) <D(1) 2 0 11+V(3) 26+V(2) 12 23+V(1) 1
24 36+V(1)+3*V(2)+3*V(3) -16+-1*V(1)+-1*V(2)+-1*V(3) <A(2) 1 2 0 11+V(3) 26+V(2) 12 23+V(1) 1
25 38+V(1)+3*V(2)+3*V(3) -14+-1*V(1)+-1*V(2)+-1*V(3) 1 (2)B> 1 2 0 11+V(3) 26+V(2) 12 23+V(1) 1
26 39+V(1)+3*V(2)+3*V(3) -13+-1*V(1)+-1*V(2)+-1*V(3) 1 2 (2)C> 2 0 11+V(3) 26+V(2) 12 23+V(1) 1
27 40+V(1)+3*V(2)+3*V(3) -12+-1*V(1)+-1*V(2)+-1*V(3) 1 22 (1)C> 0 11+V(3) 26+V(2) 12 23+V(1) 1
28 42+V(1)+3*V(2)+3*V(3) -14+-1*V(1)+-1*V(2)+-1*V(3) 1 22 <D(2) 12+V(3) 26+V(2) 12 23+V(1) 1
29 43+V(1)+3*V(2)+3*V(3) -15+-1*V(1)+-1*V(2)+-1*V(3) 1 2 <B(0) 2 12+V(3) 26+V(2) 12 23+V(1) 1
30 47+V(1)+3*V(2)+3*V(3) -13+-1*V(1)+-1*V(2)+-1*V(3) 12 (1)C> 2 12+V(3) 26+V(2) 12 23+V(1) 1
31 48+V(1)+3*V(2)+3*V(3) -12+-1*V(1)+-1*V(2)+-1*V(3) 13 (1)C> 12+V(3) 26+V(2) 12 23+V(1) 1
32 49+V(1)+3*V(2)+3*V(3) -11+-1*V(1)+-1*V(2)+-1*V(3) 14 (0)C> 11+V(3) 26+V(2) 12 23+V(1) 1
33 50+V(1)+3*V(2)+4*V(3) -10+-1*V(1)+-1*V(2) 14 01+V(3) (0)C> 26+V(2) 12 23+V(1) 1
34 51+V(1)+3*V(2)+4*V(3) -9+-1*V(1)+-1*V(2) 14 02+V(3) (1)C> 25+V(2) 12 23+V(1) 1
35 56+V(1)+4*V(2)+4*V(3) -4+-1*V(1) 14 02+V(3) 15+V(2) (1)C> 12 23+V(1) 1
36 57+V(1)+4*V(2)+4*V(3) -3+-1*V(1) 14 02+V(3) 16+V(2) (0)C> 1 23+V(1) 1
37 58+V(1)+4*V(2)+4*V(3) -2+-1*V(1) 14 02+V(3) 16+V(2) 0 (0)C> 23+V(1) 1
38 59+V(1)+4*V(2)+4*V(3) -1+-1*V(1) 14 02+V(3) 16+V(2) 02 (1)C> 22+V(1) 1
39 61+2*V(1)+4*V(2)+4*V(3) 1 14 02+V(3) 16+V(2) 02 12+V(1) (1)C> 1
40 62+2*V(1)+4*V(2)+4*V(3) 2 14 02+V(3) 16+V(2) 02 13+V(1) (0)C>
41 64+2*V(1)+4*V(2)+4*V(3) 0 14 02+V(3) 16+V(2) 02 13+V(1) <A(2) 1
42 65+2*V(1)+4*V(2)+4*V(3) -1 14 02+V(3) 16+V(2) 02 12+V(1) <D(2) 2 1
43 67+3*V(1)+4*V(2)+4*V(3) -3+-1*V(1) 14 02+V(3) 16+V(2) 02 <D(2) 23+V(1) 1
44 68+3*V(1)+4*V(2)+4*V(3) -4+-1*V(1) 14 02+V(3) 16+V(2) 0 <A(2) 24+V(1) 1
45 70+3*V(1)+4*V(2)+4*V(3) -2+-1*V(1) 14 02+V(3) 17+V(2) (2)B> 24+V(1) 1
46 74+4*V(1)+4*V(2)+4*V(3) 2 14 02+V(3) 17+V(2) 24+V(1) (2)B> 1
47 75+4*V(1)+4*V(2)+4*V(3) 3 14 02+V(3) 17+V(2) 25+V(1) (2)C>
48 77+4*V(1)+4*V(2)+4*V(3) 1 14 02+V(3) 17+V(2) 25+V(1) <B(0) 1
49 81+4*V(1)+4*V(2)+4*V(3) 3 14 02+V(3) 17+V(2) 24+V(1) 1 (1)C> 1
<< Success! ==> defined new CTR 10 (PPA)
68439 57654788 9768 14 02 17 29796 1 (1)C> 1
== Executing PA-CTR 4, V(1)=0, V(2)=9793, repcount=4897, factor=3/2
102718 129645585 14665 14 02 17 22 114692 (1)C> 1
102719 129645586 14666 14 02 17 22 114693 (0)C>
102720 129645588 14664 14 02 17 22 114693 <A(2) 1
102721 129645589 14663 14 02 17 22 114692 <D(2) 2 1
102722 129660281 -29 14 02 17 22 <D(2) 214693 1
102723 129660282 -30 14 02 17 2 <B(0) 214694 1
102724 129660286 -28 14 02 18 (1)C> 214694 1
102725 129674980 14666 14 02 114702 (1)C> 1
102726 129674981 14667 14 02 114703 (0)C>
102727 129674983 14665 14 02 114703 <A(2) 1
102728 129674984 14664 14 02 114702 <D(2) 2 1
102729 129689686 -38 14 02 <D(2) 214703 1
102730 129689687 -39 14 0 <A(2) 214704 1
102731 129689689 -37 15 (2)B> 214704 1
102732 129704393 14667 15 214704 (2)B> 1
102733 129704394 14668 15 214705 (2)C>
102734 129704396 14666 15 214705 <B(0) 1
102735 129704400 14668 15 214704 1 (1)C> 1
>> Try to prove a PPA-CTR with 3 Vars...
0 0 0 11+V(3) 02 11+V(2) 22 11+V(1) (1)C> 1
1 1 1 11+V(3) 02 11+V(2) 22 12+V(1) (0)C>
2 3 -1 11+V(3) 02 11+V(2) 22 12+V(1) <A(2) 1
3 4 -2 11+V(3) 02 11+V(2) 22 11+V(1) <D(2) 2 1
4 5+V(1) -3+-1*V(1) 11+V(3) 02 11+V(2) 22 <D(2) 22+V(1) 1
5 6+V(1) -4+-1*V(1) 11+V(3) 02 11+V(2) 2 <B(0) 23+V(1) 1
6 10+V(1) -2+-1*V(1) 11+V(3) 02 12+V(2) (1)C> 23+V(1) 1
7 13+2*V(1) 1 11+V(3) 02 15+V(1)+V(2) (1)C> 1
8 14+2*V(1) 2 11+V(3) 02 16+V(1)+V(2) (0)C>
9 16+2*V(1) 0 11+V(3) 02 16+V(1)+V(2) <A(2) 1
10 17+2*V(1) -1 11+V(3) 02 15+V(1)+V(2) <D(2) 2 1
11 22+3*V(1)+V(2) -6+-1*V(1)+-1*V(2) 11+V(3) 02 <D(2) 26+V(1)+V(2) 1
12 23+3*V(1)+V(2) -7+-1*V(1)+-1*V(2) 11+V(3) 0 <A(2) 27+V(1)+V(2) 1
13 25+3*V(1)+V(2) -5+-1*V(1)+-1*V(2) 12+V(3) (2)B> 27+V(1)+V(2) 1
14 32+4*V(1)+2*V(2) 2 12+V(3) 27+V(1)+V(2) (2)B> 1
15 33+4*V(1)+2*V(2) 3 12+V(3) 28+V(1)+V(2) (2)C>
16 35+4*V(1)+2*V(2) 1 12+V(3) 28+V(1)+V(2) <B(0) 1
17 39+4*V(1)+2*V(2) 3 12+V(3) 27+V(1)+V(2) 1 (1)C> 1
<< Success! ==> defined new CTR 11 (PPA)
102735 129704400 14668 15 214704 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=14701, repcount=7351, factor=3/2
154192 291889513 22019 15 22 122054 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=22053, V(2)=4
154209 291977772 22022 1 222064 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=22061, repcount=11031, factor=3/2
231426 657136965 33053 1 22 133094 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=33093, V(2)=0
231443 657269376 33056 1 233100 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=33097, repcount=16549, factor=3/2
347286 1479043069 49605 1 22 149648 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=49647, V(2)=0
347303 1479241696 49608 1 249654 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=49651, repcount=24826, factor=3/2
521085 3328480784 74434 1 22 174479 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=74478, V(2)=0
521102 3328778735 74437 1 274485 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=74482, repcount=37242, factor=3/2
781796 7490050847 111679 1 2 1111727 (1)C> 1
== Executing PPA-CTR 3 (once), V(1)=111726
781826 7490497800 111682 15 2111730 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=111727, repcount=55864, factor=3/2
1172874 16853415928 167546 15 22 1167593 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=167592, V(2)=4
1172891 16854086343 167549 1 2167603 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=167600, repcount=83801, factor=3/2
1759498 37922747156 251350 1 2 1251404 (1)C> 1
== Executing PPA-CTR 3 (once), V(1)=251403
1759528 37923752817 251353 15 2251407 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=251404, repcount=125703, factor=3/2
2639449 85328742474 377056 15 2 1377110 (1)C> 1
== Executing PPA-CTR 6 (once), V(1)=377109, V(2)=3
2639479 85330250975 377059 14 04 1 2377113 1 (1)C> 1
== Executing PA-CTR 4, V(1)=0, V(2)=377110, repcount=188556, factor=3/2
3959371 191992231943 565615 14 04 1 2 1565669 (1)C> 1
== Executing PPA-CTR 5 (once), V(1)=565668, V(2)=3
3959401 191994494664 565618 19 2565672 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=565669, repcount=282835, factor=3/2
5939246 431984234689 848453 19 22 1848506 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=848505, V(2)=8
5939263 431987628764 848456 1 2848520 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=848517, repcount=424259, factor=3/2
8909076 971978968597 1272715 1 22 11272778 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=1272777, V(2)=0
8909093 971984059744 1272718 1 21272784 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=1272781, repcount=636391, factor=3/2
13363830 2186970938297 1909109 1 22 11909174 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=1909173, V(2)=0
13363847 2186978575028 1909112 1 21909180 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=1909177, repcount=954589, factor=3/2
20045970 4920708597681 2863701 1 22 12863768 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=2863767, V(2)=0
20045987 4920720052788 2863704 1 22863774 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=2863771, repcount=1431886, factor=3/2
30069189 11071626922636 4295590 1 22 14295659 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=4295658, V(2)=0
30069206 11071644105307 4295593 1 24295665 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=4295662, repcount=2147832, factor=3/2
45104030 24911212484299 6443425 1 2 16443497 (1)C> 1
== Executing PPA-CTR 3 (once), V(1)=6443496
45104060 24911238258332 6443428 15 26443500 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=6443497, repcount=3221749, factor=3/2
67656303 56050270332825 9665177 15 22 19665248 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=9665247, V(2)=4
67656320 56050308993860 9665180 1 29665258 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=9665255, repcount=4832628, factor=3/2
101484716 126113237479292 14497808 1 22 114497885 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=14497884, V(2)=0
101484733 126113295470867 14497811 1 214497891 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=14497888, repcount=7248945, factor=3/2
152227348 283754978799392 21746756 1 2 121746836 (1)C> 1
== Executing PPA-CTR 3 (once), V(1)=21746835
152227378 283755065786781 21746759 15 221746839 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=21746836, repcount=10873419, factor=3/2
228341311 638448896769654 32620178 15 2 132620258 (1)C> 1
== Executing PPA-CTR 6 (once), V(1)=32620257, V(2)=3
228341341 638449027250747 32620181 14 04 1 232620261 1 (1)C> 1
== Executing PA-CTR 4, V(1)=0, V(2)=32620258, repcount=16310130, factor=3/2
342512251 1436510212202747 48930311 14 04 1 2 148930391 (1)C> 1
== Executing PPA-CTR 5 (once), V(1)=48930390, V(2)=3
342512281 1436510407924356 48930314 19 248930394 1 (1)C> 1
== Executing PA-CTR 1, V(1)=0, V(2)=48930391, repcount=24465196, factor=3/2
513768653 3232148098531564 73395510 19 22 173395589 (1)C> 1
== Executing PPA-CTR 2 (once), V(1)=73395588, V(2)=8
513768670 3232148392113971 73395513 1 273395603 1 (1)C> 1
Lines: 400
Top steps: 399
Macro steps: 513768670
Basic steps: 3232148392113971
Tape index: 73395513
nonzeros: 73395607
log10(nonzeros): 7.866
log10(steps ): 15.509
Input to awk program:
gohalt 1
nbs 3
T 4-state 3-symbol #f (T.J. & S. Ligocki)
: >2.5x10^4561 >3.9x10^9122
5T 1RB 2LD 1RH 2LC 2RC 2RB 1LD 0RC 1RC 2LA 2LD 0LB
L 10
M 400
pref sim
machv Lig43_f just simple
machv Lig43_f-r with repetitions reduced
machv Lig43_f-1 with tape symbol exponents
machv Lig43_f-m as 1-bck-macro machine
machv Lig43_f-a as 1-bck-macro machine with pure additive config-TRs
iam Lig43_f-a
mtype 1 0
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:14:12 CEST 2010
edate Tue Jul 6 22:14:13 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:14:12 CEST 2010