Comment: This TM produces 15828 nonzeros in 493,600,387 steps.
| State | on 0 |
on 1 |
on 2 |
on 3 |
on 4 |
on 5 |
on 0 | on 1 | on 2 | on 3 | on 4 | on 5 | ||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Move | Goto | Move | Goto | Move | Goto | Move | Goto | Move | Goto | Move | Goto | |||||||||||||
| A | 1RB | 4LA | 1RA | 5LB | 1RA | 3LB | 1 | right | B | 4 | left | A | 1 | right | A | 5 | left | B | 1 | right | A | 3 | left | B |
| B | 1LB | 1LA | 5LA | 2LA | 2RB | 1RH | 1 | left | B | 1 | left | A | 5 | left | A | 2 | left | A | 2 | right | B | 1 | right | H |
The same TM just simple.
The same TM with repetitions reduced.
The same TM with tape symbol exponents.
The same TM as bck-2-macro machine.
Simulation is done as bck-2-macro machine with pure additive config-TRs.
Pushing initial machine.
Pushing BCK machine.
Pushing macro factor 2.
Steps BasSteps BasTpos Tape contents
0 0 0 (0)A>
1 6 -2 <A(4) 11
2 8 0 01 (2)B> 11
3 12 -2 01 <A(4) 41
4 16 0 12 (2)B> 41
5 24 2 12 11 (1)A>
6 28 0 12 11 <A(4) 11
7 30 -2 12 <A(4) 44 11
8 32 0 11 (1)A> 44 11
9 34 2 112 (1)A> 11
10 36 0 112 <A(4) 41
11 40 -4 <A(4) 442 41
12 42 -2 01 (2)B> 442 41
13 46 2 01 222 (2)B> 41
14 54 4 01 222 11 (1)A>
15 58 2 01 222 11 <A(4) 11
16 60 0 01 222 <A(4) 44 11
17 62 2 01 22 21 (1)A> 44 11
18 64 4 01 22 21 11 (1)A> 11
19 66 2 01 22 21 11 <A(4) 41
20 68 0 01 22 21 <A(4) 44 41
21 72 2 01 22 11 (1)A> 44 41
22 74 4 01 22 112 (1)A> 41
23 78 2 01 22 112 <A(4) 44
24 82 -2 01 22 <A(4) 443
25 84 0 01 21 (1)A> 443
26 90 6 01 21 113 (1)A>
27 94 4 01 21 113 <A(4) 11
28 100 -2 01 21 <A(4) 443 11
29 104 0 01 11 (1)A> 443 11
30 110 6 01 114 (1)A> 11
31 112 4 01 114 <A(4) 41
32 120 -4 01 <A(4) 444 41
33 124 -2 12 (2)B> 444 41
34 132 6 12 224 (2)B> 41
35 140 8 12 224 11 (1)A>
36 144 6 12 224 11 <A(4) 11
37 146 4 12 224 <A(4) 44 11
38 148 6 12 223 21 (1)A> 44 11
39 150 8 12 223 21 11 (1)A> 11
40 152 6 12 223 21 11 <A(4) 41
41 154 4 12 223 21 <A(4) 44 41
42 158 6 12 223 11 (1)A> 44 41
43 160 8 12 223 112 (1)A> 41
44 164 6 12 223 112 <A(4) 44
45 168 2 12 223 <A(4) 443
46 170 4 12 222 21 (1)A> 443
47 176 10 12 222 21 113 (1)A>
48 180 8 12 222 21 113 <A(4) 11
49 186 2 12 222 21 <A(4) 443 11
50 190 4 12 222 11 (1)A> 443 11
51 196 10 12 222 114 (1)A> 11
52 198 8 12 222 114 <A(4) 41
53 206 0 12 222 <A(4) 444 41
54 208 2 12 22 21 (1)A> 444 41
55 216 10 12 22 21 114 (1)A> 41
56 220 8 12 22 21 114 <A(4) 44
57 228 0 12 22 21 <A(4) 445
58 232 2 12 22 11 (1)A> 445
59 242 12 12 22 116 (1)A>
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 224+V(2) 111+V(1) (1)A>
1 4 -2 [*]* 224+V(2) 111+V(1) <A(4) 11
2 6+2*V(1) -4+-2*V(1) [*]* 224+V(2) <A(4) 441+V(1) 11
3 8+2*V(1) -2+-2*V(1) [*]* 223+V(2) 21 (1)A> 441+V(1) 11
4 10+4*V(1) 0 [*]* 223+V(2) 21 111+V(1) (1)A> 11
5 12+4*V(1) -2 [*]* 223+V(2) 21 111+V(1) <A(4) 41
6 14+6*V(1) -4+-2*V(1) [*]* 223+V(2) 21 <A(4) 441+V(1) 41
7 18+6*V(1) -2+-2*V(1) [*]* 223+V(2) 11 (1)A> 441+V(1) 41
8 20+8*V(1) 0 [*]* 223+V(2) 112+V(1) (1)A> 41
9 24+8*V(1) -2 [*]* 223+V(2) 112+V(1) <A(4) 44
10 28+10*V(1) -6+-2*V(1) [*]* 223+V(2) <A(4) 443+V(1)
11 30+10*V(1) -4+-2*V(1) [*]* 222+V(2) 21 (1)A> 443+V(1)
12 36+12*V(1) 2 [*]* 222+V(2) 21 113+V(1) (1)A>
13 40+12*V(1) 0 [*]* 222+V(2) 21 113+V(1) <A(4) 11
14 46+14*V(1) -6+-2*V(1) [*]* 222+V(2) 21 <A(4) 443+V(1) 11
15 50+14*V(1) -4+-2*V(1) [*]* 222+V(2) 11 (1)A> 443+V(1) 11
16 56+16*V(1) 2 [*]* 222+V(2) 114+V(1) (1)A> 11
17 58+16*V(1) 0 [*]* 222+V(2) 114+V(1) <A(4) 41
18 66+18*V(1) -8+-2*V(1) [*]* 222+V(2) <A(4) 444+V(1) 41
19 68+18*V(1) -6+-2*V(1) [*]* 221+V(2) 21 (1)A> 444+V(1) 41
20 76+20*V(1) 2 [*]* 221+V(2) 21 114+V(1) (1)A> 41
21 80+20*V(1) 0 [*]* 221+V(2) 21 114+V(1) <A(4) 44
22 88+22*V(1) -8+-2*V(1) [*]* 221+V(2) 21 <A(4) 445+V(1)
23 92+22*V(1) -6+-2*V(1) [*]* 221+V(2) 11 (1)A> 445+V(1)
24 102+24*V(1) 4 [*]* 221+V(2) 116+V(1) (1)A>
<< Success! ==> defined new CTR 1 (PA)
60 246 10 12 22 116 <A(4) 11
61 258 -2 12 22 <A(4) 446 11
62 260 0 12 21 (1)A> 446 11
63 272 12 12 21 116 (1)A> 11
64 274 10 12 21 116 <A(4) 41
65 286 -2 12 21 <A(4) 446 41
66 290 0 12 11 (1)A> 446 41
67 302 12 12 117 (1)A> 41
68 306 10 12 117 <A(4) 44
69 320 -4 12 <A(4) 448
70 322 -2 11 (1)A> 448
71 338 14 119 (1)A>
72 342 12 119 <A(4) 11
73 360 -6 <A(4) 449 11
74 362 -4 01 (2)B> 449 11
75 380 14 01 229 (2)B> 11
76 384 12 01 229 <A(4) 41
77 386 14 01 228 21 (1)A> 41
78 390 12 01 228 21 <A(4) 44
79 394 14 01 228 11 (1)A> 44
80 396 16 01 228 112 (1)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 12 22 112+V(1) (1)A>
1 4 -2 12 22 112+V(1) <A(4) 11
2 8+2*V(1) -6+-2*V(1) 12 22 <A(4) 442+V(1) 11
3 10+2*V(1) -4+-2*V(1) 12 21 (1)A> 442+V(1) 11
4 14+4*V(1) 0 12 21 112+V(1) (1)A> 11
5 16+4*V(1) -2 12 21 112+V(1) <A(4) 41
6 20+6*V(1) -6+-2*V(1) 12 21 <A(4) 442+V(1) 41
7 24+6*V(1) -4+-2*V(1) 12 11 (1)A> 442+V(1) 41
8 28+8*V(1) 0 12 113+V(1) (1)A> 41
9 32+8*V(1) -2 12 113+V(1) <A(4) 44
10 38+10*V(1) -8+-2*V(1) 12 <A(4) 444+V(1)
11 40+10*V(1) -6+-2*V(1) 11 (1)A> 444+V(1)
12 48+12*V(1) 2 115+V(1) (1)A>
13 52+12*V(1) 0 115+V(1) <A(4) 11
14 62+14*V(1) -10+-2*V(1) <A(4) 445+V(1) 11
15 64+14*V(1) -8+-2*V(1) 01 (2)B> 445+V(1) 11
16 74+16*V(1) 2 01 225+V(1) (2)B> 11
17 78+16*V(1) 0 01 225+V(1) <A(4) 41
18 80+16*V(1) 2 01 224+V(1) 21 (1)A> 41
19 84+16*V(1) 0 01 224+V(1) 21 <A(4) 44
20 88+16*V(1) 2 01 224+V(1) 11 (1)A> 44
21 90+16*V(1) 4 01 224+V(1) 112 (1)A>
<< Success! ==> defined new CTR 2 (PPA)
80 396 16 01 228 112 (1)A>
== Executing PA-CTR 1, V(1)=1, V(2)=4, repcount=2, factor=5/3
128 768 24 01 222 1112 (1)A>
129 772 22 01 222 1112 <A(4) 11
130 796 -2 01 222 <A(4) 4412 11
131 798 0 01 22 21 (1)A> 4412 11
132 822 24 01 22 21 1112 (1)A> 11
133 824 22 01 22 21 1112 <A(4) 41
134 848 -2 01 22 21 <A(4) 4412 41
135 852 0 01 22 11 (1)A> 4412 41
136 876 24 01 22 1113 (1)A> 41
137 880 22 01 22 1113 <A(4) 44
138 906 -4 01 22 <A(4) 4414
139 908 -2 01 21 (1)A> 4414
140 936 26 01 21 1114 (1)A>
141 940 24 01 21 1114 <A(4) 11
142 968 -4 01 21 <A(4) 4414 11
143 972 -2 01 11 (1)A> 4414 11
144 1000 26 01 1115 (1)A> 11
145 1002 24 01 1115 <A(4) 41
146 1032 -6 01 <A(4) 4415 41
147 1036 -4 12 (2)B> 4415 41
148 1066 26 12 2215 (2)B> 41
149 1074 28 12 2215 11 (1)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 222 111+V(1) (1)A>
1 4 -2 01 222 111+V(1) <A(4) 11
2 6+2*V(1) -4+-2*V(1) 01 222 <A(4) 441+V(1) 11
3 8+2*V(1) -2+-2*V(1) 01 22 21 (1)A> 441+V(1) 11
4 10+4*V(1) 0 01 22 21 111+V(1) (1)A> 11
5 12+4*V(1) -2 01 22 21 111+V(1) <A(4) 41
6 14+6*V(1) -4+-2*V(1) 01 22 21 <A(4) 441+V(1) 41
7 18+6*V(1) -2+-2*V(1) 01 22 11 (1)A> 441+V(1) 41
8 20+8*V(1) 0 01 22 112+V(1) (1)A> 41
9 24+8*V(1) -2 01 22 112+V(1) <A(4) 44
10 28+10*V(1) -6+-2*V(1) 01 22 <A(4) 443+V(1)
11 30+10*V(1) -4+-2*V(1) 01 21 (1)A> 443+V(1)
12 36+12*V(1) 2 01 21 113+V(1) (1)A>
13 40+12*V(1) 0 01 21 113+V(1) <A(4) 11
14 46+14*V(1) -6+-2*V(1) 01 21 <A(4) 443+V(1) 11
15 50+14*V(1) -4+-2*V(1) 01 11 (1)A> 443+V(1) 11
16 56+16*V(1) 2 01 114+V(1) (1)A> 11
17 58+16*V(1) 0 01 114+V(1) <A(4) 41
18 66+18*V(1) -8+-2*V(1) 01 <A(4) 444+V(1) 41
19 70+18*V(1) -6+-2*V(1) 12 (2)B> 444+V(1) 41
20 78+20*V(1) 2 12 224+V(1) (2)B> 41
21 86+20*V(1) 4 12 224+V(1) 11 (1)A>
<< Success! ==> defined new CTR 3 (PPA)
149 1074 28 12 2215 11 (1)A>
== Executing PA-CTR 1, V(1)=0, V(2)=11, repcount=4, factor=5/3
245 2202 44 12 223 1121 (1)A>
246 2206 42 12 223 1121 <A(4) 11
247 2248 0 12 223 <A(4) 4421 11
248 2250 2 12 222 21 (1)A> 4421 11
249 2292 44 12 222 21 1121 (1)A> 11
250 2294 42 12 222 21 1121 <A(4) 41
251 2336 0 12 222 21 <A(4) 4421 41
252 2340 2 12 222 11 (1)A> 4421 41
253 2382 44 12 222 1122 (1)A> 41
254 2386 42 12 222 1122 <A(4) 44
255 2430 -2 12 222 <A(4) 4423
256 2432 0 12 22 21 (1)A> 4423
257 2478 46 12 22 21 1123 (1)A>
258 2482 44 12 22 21 1123 <A(4) 11
259 2528 -2 12 22 21 <A(4) 4423 11
260 2532 0 12 22 11 (1)A> 4423 11
261 2578 46 12 22 1124 (1)A> 11
262 2580 44 12 22 1124 <A(4) 41
263 2628 -4 12 22 <A(4) 4424 41
264 2630 -2 12 21 (1)A> 4424 41
265 2678 46 12 21 1124 (1)A> 41
266 2682 44 12 21 1124 <A(4) 44
267 2730 -4 12 21 <A(4) 4425
268 2734 -2 12 11 (1)A> 4425
269 2784 48 12 1126 (1)A>
270 2788 46 12 1126 <A(4) 11
271 2840 -6 12 <A(4) 4426 11
272 2842 -4 11 (1)A> 4426 11
273 2894 48 1127 (1)A> 11
274 2896 46 1127 <A(4) 41
275 2950 -8 <A(4) 4427 41
276 2952 -6 01 (2)B> 4427 41
277 3006 48 01 2227 (2)B> 41
278 3014 50 01 2227 11 (1)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 12 223 111+V(1) (1)A>
1 4 -2 12 223 111+V(1) <A(4) 11
2 6+2*V(1) -4+-2*V(1) 12 223 <A(4) 441+V(1) 11
3 8+2*V(1) -2+-2*V(1) 12 222 21 (1)A> 441+V(1) 11
4 10+4*V(1) 0 12 222 21 111+V(1) (1)A> 11
5 12+4*V(1) -2 12 222 21 111+V(1) <A(4) 41
6 14+6*V(1) -4+-2*V(1) 12 222 21 <A(4) 441+V(1) 41
7 18+6*V(1) -2+-2*V(1) 12 222 11 (1)A> 441+V(1) 41
8 20+8*V(1) 0 12 222 112+V(1) (1)A> 41
9 24+8*V(1) -2 12 222 112+V(1) <A(4) 44
10 28+10*V(1) -6+-2*V(1) 12 222 <A(4) 443+V(1)
11 30+10*V(1) -4+-2*V(1) 12 22 21 (1)A> 443+V(1)
12 36+12*V(1) 2 12 22 21 113+V(1) (1)A>
13 40+12*V(1) 0 12 22 21 113+V(1) <A(4) 11
14 46+14*V(1) -6+-2*V(1) 12 22 21 <A(4) 443+V(1) 11
15 50+14*V(1) -4+-2*V(1) 12 22 11 (1)A> 443+V(1) 11
16 56+16*V(1) 2 12 22 114+V(1) (1)A> 11
17 58+16*V(1) 0 12 22 114+V(1) <A(4) 41
18 66+18*V(1) -8+-2*V(1) 12 22 <A(4) 444+V(1) 41
19 68+18*V(1) -6+-2*V(1) 12 21 (1)A> 444+V(1) 41
20 76+20*V(1) 2 12 21 114+V(1) (1)A> 41
21 80+20*V(1) 0 12 21 114+V(1) <A(4) 44
22 88+22*V(1) -8+-2*V(1) 12 21 <A(4) 445+V(1)
23 92+22*V(1) -6+-2*V(1) 12 11 (1)A> 445+V(1)
24 102+24*V(1) 4 12 116+V(1) (1)A>
25 106+24*V(1) 2 12 116+V(1) <A(4) 11
26 118+26*V(1) -10+-2*V(1) 12 <A(4) 446+V(1) 11
27 120+26*V(1) -8+-2*V(1) 11 (1)A> 446+V(1) 11
28 132+28*V(1) 4 117+V(1) (1)A> 11
29 134+28*V(1) 2 117+V(1) <A(4) 41
30 148+30*V(1) -12+-2*V(1) <A(4) 447+V(1) 41
31 150+30*V(1) -10+-2*V(1) 01 (2)B> 447+V(1) 41
32 164+32*V(1) 4 01 227+V(1) (2)B> 41
33 172+32*V(1) 6 01 227+V(1) 11 (1)A>
<< Success! ==> defined new CTR 4 (PPA)
278 3014 50 01 2227 11 (1)A>
== Executing PA-CTR 1, V(1)=0, V(2)=23, repcount=8, factor=5/3
470 7190 82 01 223 1141 (1)A>
471 7194 80 01 223 1141 <A(4) 11
472 7276 -2 01 223 <A(4) 4441 11
473 7278 0 01 222 21 (1)A> 4441 11
474 7360 82 01 222 21 1141 (1)A> 11
475 7362 80 01 222 21 1141 <A(4) 41
476 7444 -2 01 222 21 <A(4) 4441 41
477 7448 0 01 222 11 (1)A> 4441 41
478 7530 82 01 222 1142 (1)A> 41
479 7534 80 01 222 1142 <A(4) 44
480 7618 -4 01 222 <A(4) 4443
481 7620 -2 01 22 21 (1)A> 4443
482 7706 84 01 22 21 1143 (1)A>
483 7710 82 01 22 21 1143 <A(4) 11
484 7796 -4 01 22 21 <A(4) 4443 11
485 7800 -2 01 22 11 (1)A> 4443 11
486 7886 84 01 22 1144 (1)A> 11
487 7888 82 01 22 1144 <A(4) 41
488 7976 -6 01 22 <A(4) 4444 41
489 7978 -4 01 21 (1)A> 4444 41
490 8066 84 01 21 1144 (1)A> 41
491 8070 82 01 21 1144 <A(4) 44
492 8158 -6 01 21 <A(4) 4445
493 8162 -4 01 11 (1)A> 4445
494 8252 86 01 1146 (1)A>
495 8256 84 01 1146 <A(4) 11
496 8348 -8 01 <A(4) 4446 11
497 8352 -6 12 (2)B> 4446 11
498 8444 86 12 2246 (2)B> 11
499 8448 84 12 2246 <A(4) 41
500 8450 86 12 2245 21 (1)A> 41
501 8454 84 12 2245 21 <A(4) 44
502 8458 86 12 2245 11 (1)A> 44
503 8460 88 12 2245 112 (1)A>
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 223 111+V(1) (1)A>
1 4 -2 01 223 111+V(1) <A(4) 11
2 6+2*V(1) -4+-2*V(1) 01 223 <A(4) 441+V(1) 11
3 8+2*V(1) -2+-2*V(1) 01 222 21 (1)A> 441+V(1) 11
4 10+4*V(1) 0 01 222 21 111+V(1) (1)A> 11
5 12+4*V(1) -2 01 222 21 111+V(1) <A(4) 41
6 14+6*V(1) -4+-2*V(1) 01 222 21 <A(4) 441+V(1) 41
7 18+6*V(1) -2+-2*V(1) 01 222 11 (1)A> 441+V(1) 41
8 20+8*V(1) 0 01 222 112+V(1) (1)A> 41
9 24+8*V(1) -2 01 222 112+V(1) <A(4) 44
10 28+10*V(1) -6+-2*V(1) 01 222 <A(4) 443+V(1)
11 30+10*V(1) -4+-2*V(1) 01 22 21 (1)A> 443+V(1)
12 36+12*V(1) 2 01 22 21 113+V(1) (1)A>
13 40+12*V(1) 0 01 22 21 113+V(1) <A(4) 11
14 46+14*V(1) -6+-2*V(1) 01 22 21 <A(4) 443+V(1) 11
15 50+14*V(1) -4+-2*V(1) 01 22 11 (1)A> 443+V(1) 11
16 56+16*V(1) 2 01 22 114+V(1) (1)A> 11
17 58+16*V(1) 0 01 22 114+V(1) <A(4) 41
18 66+18*V(1) -8+-2*V(1) 01 22 <A(4) 444+V(1) 41
19 68+18*V(1) -6+-2*V(1) 01 21 (1)A> 444+V(1) 41
20 76+20*V(1) 2 01 21 114+V(1) (1)A> 41
21 80+20*V(1) 0 01 21 114+V(1) <A(4) 44
22 88+22*V(1) -8+-2*V(1) 01 21 <A(4) 445+V(1)
23 92+22*V(1) -6+-2*V(1) 01 11 (1)A> 445+V(1)
24 102+24*V(1) 4 01 116+V(1) (1)A>
25 106+24*V(1) 2 01 116+V(1) <A(4) 11
26 118+26*V(1) -10+-2*V(1) 01 <A(4) 446+V(1) 11
27 122+26*V(1) -8+-2*V(1) 12 (2)B> 446+V(1) 11
28 134+28*V(1) 4 12 226+V(1) (2)B> 11
29 138+28*V(1) 2 12 226+V(1) <A(4) 41
30 140+28*V(1) 4 12 225+V(1) 21 (1)A> 41
31 144+28*V(1) 2 12 225+V(1) 21 <A(4) 44
32 148+28*V(1) 4 12 225+V(1) 11 (1)A> 44
33 150+28*V(1) 6 12 225+V(1) 112 (1)A>
<< Success! ==> defined new CTR 5 (PPA)
503 8460 88 12 2245 112 (1)A>
== Executing PA-CTR 1, V(1)=1, V(2)=41, repcount=14, factor=5/3
839 21144 144 12 223 1172 (1)A>
== Executing PPA-CTR 4 (once), V(1)=71
872 23588 150 01 2278 11 (1)A>
== Executing PA-CTR 1, V(1)=0, V(2)=74, repcount=25, factor=5/3
1472 62138 250 01 223 11126 (1)A>
== Executing PPA-CTR 5 (once), V(1)=125
1505 65788 256 12 22130 112 (1)A>
== Executing PA-CTR 1, V(1)=1, V(2)=126, repcount=43, factor=5/3
2537 179566 428 12 22 11217 (1)A>
== Executing PPA-CTR 2 (once), V(1)=215
2558 183096 432 01 22219 112 (1)A>
== Executing PA-CTR 1, V(1)=1, V(2)=215, repcount=72, factor=5/3
4286 498888 720 01 223 11362 (1)A>
== Executing PPA-CTR 5 (once), V(1)=361
4319 509146 726 12 22366 112 (1)A>
== Executing PA-CTR 1, V(1)=1, V(2)=362, repcount=121, factor=5/3
7223 1395592 1210 12 223 11607 (1)A>
== Executing PPA-CTR 4 (once), V(1)=606
7256 1415156 1216 01 22613 11 (1)A>
== Executing PA-CTR 1, V(1)=0, V(2)=609, repcount=204, factor=5/3
12152 3920684 2032 01 22 111021 (1)A>
12153 3920688 2030 01 22 111021 <A(4) 11
12154 3922730 -12 01 22 <A(4) 441021 11
12155 3922732 -10 01 21 (1)A> 441021 11
12156 3924774 2032 01 21 111021 (1)A> 11
12157 3924776 2030 01 21 111021 <A(4) 41
12158 3926818 -12 01 21 <A(4) 441021 41
12159 3926822 -10 01 11 (1)A> 441021 41
12160 3928864 2032 01 111022 (1)A> 41
12161 3928868 2030 01 111022 <A(4) 44
12162 3930912 -14 01 <A(4) 441023
12163 3930916 -12 12 (2)B> 441023
12164 3932962 2034 12 221023 (2)B>
12165 3932964 2032 12 221023 <A(5) 10
12166 3932970 2030 12 221022 <A(4) 43 10
12167 3932972 2032 12 221021 21 (1)A> 43 10
12168 3932976 2030 12 221021 21 <A(4) 15 10
12169 3932980 2032 12 221021 11 (1)A> 15 10
12170 3932982 2030 12 221021 11 <A(4) 45 10
12171 3932984 2028 12 221021 <A(4) 44 45 10
12172 3932986 2030 12 221020 21 (1)A> 44 45 10
12173 3932988 2032 12 221020 21 11 (1)A> 45 10
12174 3932992 2030 12 221020 21 11 <A(4) 13 10
12175 3932994 2028 12 221020 21 <A(4) 44 13 10
12176 3932998 2030 12 221020 11 (1)A> 44 13 10
12177 3933000 2032 12 221020 112 (1)A> 13 10
12178 3933002 2030 12 221020 112 <A(4) 43 10
12179 3933006 2026 12 221020 <A(4) 442 43 10
12180 3933008 2028 12 221019 21 (1)A> 442 43 10
12181 3933012 2032 12 221019 21 112 (1)A> 43 10
12182 3933016 2030 12 221019 21 112 <A(4) 15 10
12183 3933020 2026 12 221019 21 <A(4) 442 15 10
12184 3933024 2028 12 221019 11 (1)A> 442 15 10
12185 3933028 2032 12 221019 113 (1)A> 15 10
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 223+V(2) 111+V(1) (1)A> 15 [*]*
1 2 -2 [*]* 223+V(2) 111+V(1) <A(4) 45 [*]*
2 4+2*V(1) -4+-2*V(1) [*]* 223+V(2) <A(4) 441+V(1) 45 [*]*
3 6+2*V(1) -2+-2*V(1) [*]* 222+V(2) 21 (1)A> 441+V(1) 45 [*]*
4 8+4*V(1) 0 [*]* 222+V(2) 21 111+V(1) (1)A> 45 [*]*
5 12+4*V(1) -2 [*]* 222+V(2) 21 111+V(1) <A(4) 13 [*]*
6 14+6*V(1) -4+-2*V(1) [*]* 222+V(2) 21 <A(4) 441+V(1) 13 [*]*
7 18+6*V(1) -2+-2*V(1) [*]* 222+V(2) 11 (1)A> 441+V(1) 13 [*]*
8 20+8*V(1) 0 [*]* 222+V(2) 112+V(1) (1)A> 13 [*]*
9 22+8*V(1) -2 [*]* 222+V(2) 112+V(1) <A(4) 43 [*]*
10 26+10*V(1) -6+-2*V(1) [*]* 222+V(2) <A(4) 442+V(1) 43 [*]*
11 28+10*V(1) -4+-2*V(1) [*]* 221+V(2) 21 (1)A> 442+V(1) 43 [*]*
12 32+12*V(1) 0 [*]* 221+V(2) 21 112+V(1) (1)A> 43 [*]*
13 36+12*V(1) -2 [*]* 221+V(2) 21 112+V(1) <A(4) 15 [*]*
14 40+14*V(1) -6+-2*V(1) [*]* 221+V(2) 21 <A(4) 442+V(1) 15 [*]*
15 44+14*V(1) -4+-2*V(1) [*]* 221+V(2) 11 (1)A> 442+V(1) 15 [*]*
16 48+16*V(1) 0 [*]* 221+V(2) 113+V(1) (1)A> 15 [*]*
<< Success! ==> defined new CTR 6 (PA)
12185 3933028 2032 12 221019 113 (1)A> 15 10
== Executing PA-CTR 6, V(1)=2, V(2)=1016, repcount=509, factor=2/2
20329 8110900 2032 12 22 111021 (1)A> 15 10
20330 8110902 2030 12 22 111021 <A(4) 45 10
20331 8112944 -12 12 22 <A(4) 441021 45 10
20332 8112946 -10 12 21 (1)A> 441021 45 10
20333 8114988 2032 12 21 111021 (1)A> 45 10
20334 8114992 2030 12 21 111021 <A(4) 13 10
20335 8117034 -12 12 21 <A(4) 441021 13 10
20336 8117038 -10 12 11 (1)A> 441021 13 10
20337 8119080 2032 12 111022 (1)A> 13 10
20338 8119082 2030 12 111022 <A(4) 43 10
20339 8121126 -14 12 <A(4) 441022 43 10
20340 8121128 -12 11 (1)A> 441022 43 10
20341 8123172 2032 111023 (1)A> 43 10
20342 8123176 2030 111023 <A(4) 15 10
20343 8125222 -16 <A(4) 441023 15 10
20344 8125224 -14 01 (2)B> 441023 15 10
20345 8127270 2032 01 221023 (2)B> 15 10
20346 8127274 2030 01 221023 <A(4) 45 10
20347 8127276 2032 01 221022 21 (1)A> 45 10
20348 8127280 2030 01 221022 21 <A(4) 13 10
20349 8127284 2032 01 221022 11 (1)A> 13 10
20350 8127286 2030 01 221022 11 <A(4) 43 10
20351 8127288 2028 01 221022 <A(4) 44 43 10
20352 8127290 2030 01 221021 21 (1)A> 44 43 10
20353 8127292 2032 01 221021 21 11 (1)A> 43 10
20354 8127296 2030 01 221021 21 11 <A(4) 15 10
20355 8127298 2028 01 221021 21 <A(4) 44 15 10
20356 8127302 2030 01 221021 11 (1)A> 44 15 10
20357 8127304 2032 01 221021 112 (1)A> 15 10
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 12 22 113+V(1) (1)A> 15 [*]*
1 2 -2 12 22 113+V(1) <A(4) 45 [*]*
2 8+2*V(1) -8+-2*V(1) 12 22 <A(4) 443+V(1) 45 [*]*
3 10+2*V(1) -6+-2*V(1) 12 21 (1)A> 443+V(1) 45 [*]*
4 16+4*V(1) 0 12 21 113+V(1) (1)A> 45 [*]*
5 20+4*V(1) -2 12 21 113+V(1) <A(4) 13 [*]*
6 26+6*V(1) -8+-2*V(1) 12 21 <A(4) 443+V(1) 13 [*]*
7 30+6*V(1) -6+-2*V(1) 12 11 (1)A> 443+V(1) 13 [*]*
8 36+8*V(1) 0 12 114+V(1) (1)A> 13 [*]*
9 38+8*V(1) -2 12 114+V(1) <A(4) 43 [*]*
10 46+10*V(1) -10+-2*V(1) 12 <A(4) 444+V(1) 43 [*]*
11 48+10*V(1) -8+-2*V(1) 11 (1)A> 444+V(1) 43 [*]*
12 56+12*V(1) 0 115+V(1) (1)A> 43 [*]*
13 60+12*V(1) -2 115+V(1) <A(4) 15 [*]*
14 70+14*V(1) -12+-2*V(1) <A(4) 445+V(1) 15 [*]*
15 72+14*V(1) -10+-2*V(1) 01 (2)B> 445+V(1) 15 [*]*
16 82+16*V(1) 0 01 225+V(1) (2)B> 15 [*]*
17 86+16*V(1) -2 01 225+V(1) <A(4) 45 [*]*
18 88+16*V(1) 0 01 224+V(1) 21 (1)A> 45 [*]*
19 92+16*V(1) -2 01 224+V(1) 21 <A(4) 13 [*]*
20 96+16*V(1) 0 01 224+V(1) 11 (1)A> 13 [*]*
21 98+16*V(1) -2 01 224+V(1) 11 <A(4) 43 [*]*
22 100+16*V(1) -4 01 224+V(1) <A(4) 44 43 [*]*
23 102+16*V(1) -2 01 223+V(1) 21 (1)A> 44 43 [*]*
24 104+16*V(1) 0 01 223+V(1) 21 11 (1)A> 43 [*]*
25 108+16*V(1) -2 01 223+V(1) 21 11 <A(4) 15 [*]*
26 110+16*V(1) -4 01 223+V(1) 21 <A(4) 44 15 [*]*
27 114+16*V(1) -2 01 223+V(1) 11 (1)A> 44 15 [*]*
28 116+16*V(1) 0 01 223+V(1) 112 (1)A> 15 [*]*
<< Success! ==> defined new CTR 7 (PPA)
20357 8127304 2032 01 221021 112 (1)A> 15 10
== Executing PA-CTR 6, V(1)=1, V(2)=1018, repcount=510, factor=2/2
28517 12313384 2032 01 22 111022 (1)A> 15 10
28518 12313386 2030 01 22 111022 <A(4) 45 10
28519 12315430 -14 01 22 <A(4) 441022 45 10
28520 12315432 -12 01 21 (1)A> 441022 45 10
28521 12317476 2032 01 21 111022 (1)A> 45 10
28522 12317480 2030 01 21 111022 <A(4) 13 10
28523 12319524 -14 01 21 <A(4) 441022 13 10
28524 12319528 -12 01 11 (1)A> 441022 13 10
28525 12321572 2032 01 111023 (1)A> 13 10
28526 12321574 2030 01 111023 <A(4) 43 10
28527 12323620 -16 01 <A(4) 441023 43 10
28528 12323624 -14 12 (2)B> 441023 43 10
28529 12325670 2032 12 221023 (2)B> 43 10
28530 12325674 2034 12 221023 21 (1)A> 10
28531 12325676 2032 12 221023 21 <A(4) 40
28532 12325680 2034 12 221023 11 (1)A> 40
28533 12325682 2036 12 221023 112 (1)B>
28534 12325684 2034 12 221023 112 <A(1) 10
28535 12325686 2032 12 221023 11 <A(4) 41 10
28536 12325688 2030 12 221023 <A(4) 44 41 10
28537 12325690 2032 12 221022 21 (1)A> 44 41 10
28538 12325692 2034 12 221022 21 11 (1)A> 41 10
28539 12325696 2032 12 221022 21 11 <A(4) 44 10
28540 12325698 2030 12 221022 21 <A(4) 442 10
28541 12325702 2032 12 221022 11 (1)A> 442 10
28542 12325706 2036 12 221022 113 (1)A> 10
28543 12325708 2034 12 221022 113 <A(4) 40
28544 12325714 2028 12 221022 <A(4) 443 40
28545 12325716 2030 12 221021 21 (1)A> 443 40
28546 12325722 2036 12 221021 21 113 (1)A> 40
28547 12325724 2038 12 221021 21 114 (1)B>
28548 12325726 2036 12 221021 21 114 <A(1) 10
28549 12325728 2034 12 221021 21 113 <A(4) 41 10
28550 12325734 2028 12 221021 21 <A(4) 443 41 10
28551 12325738 2030 12 221021 11 (1)A> 443 41 10
28552 12325744 2036 12 221021 114 (1)A> 41 10
28553 12325748 2034 12 221021 114 <A(4) 44 10
28554 12325756 2026 12 221021 <A(4) 445 10
28555 12325758 2028 12 221020 21 (1)A> 445 10
28556 12325768 2038 12 221020 21 115 (1)A> 10
28557 12325770 2036 12 221020 21 115 <A(4) 40
28558 12325780 2026 12 221020 21 <A(4) 445 40
28559 12325784 2028 12 221020 11 (1)A> 445 40
28560 12325794 2038 12 221020 116 (1)A> 40
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 224+V(2) 111+V(1) (1)A> 40
1 2 2 [*]* 224+V(2) 112+V(1) (1)B>
2 4 0 [*]* 224+V(2) 112+V(1) <A(1) 10
3 6 -2 [*]* 224+V(2) 111+V(1) <A(4) 41 10
4 8+2*V(1) -4+-2*V(1) [*]* 224+V(2) <A(4) 441+V(1) 41 10
5 10+2*V(1) -2+-2*V(1) [*]* 223+V(2) 21 (1)A> 441+V(1) 41 10
6 12+4*V(1) 0 [*]* 223+V(2) 21 111+V(1) (1)A> 41 10
7 16+4*V(1) -2 [*]* 223+V(2) 21 111+V(1) <A(4) 44 10
8 18+6*V(1) -4+-2*V(1) [*]* 223+V(2) 21 <A(4) 442+V(1) 10
9 22+6*V(1) -2+-2*V(1) [*]* 223+V(2) 11 (1)A> 442+V(1) 10
10 26+8*V(1) 2 [*]* 223+V(2) 113+V(1) (1)A> 10
11 28+8*V(1) 0 [*]* 223+V(2) 113+V(1) <A(4) 40
12 34+10*V(1) -6+-2*V(1) [*]* 223+V(2) <A(4) 443+V(1) 40
13 36+10*V(1) -4+-2*V(1) [*]* 222+V(2) 21 (1)A> 443+V(1) 40
14 42+12*V(1) 2 [*]* 222+V(2) 21 113+V(1) (1)A> 40
15 44+12*V(1) 4 [*]* 222+V(2) 21 114+V(1) (1)B>
16 46+12*V(1) 2 [*]* 222+V(2) 21 114+V(1) <A(1) 10
17 48+12*V(1) 0 [*]* 222+V(2) 21 113+V(1) <A(4) 41 10
18 54+14*V(1) -6+-2*V(1) [*]* 222+V(2) 21 <A(4) 443+V(1) 41 10
19 58+14*V(1) -4+-2*V(1) [*]* 222+V(2) 11 (1)A> 443+V(1) 41 10
20 64+16*V(1) 2 [*]* 222+V(2) 114+V(1) (1)A> 41 10
21 68+16*V(1) 0 [*]* 222+V(2) 114+V(1) <A(4) 44 10
22 76+18*V(1) -8+-2*V(1) [*]* 222+V(2) <A(4) 445+V(1) 10
23 78+18*V(1) -6+-2*V(1) [*]* 221+V(2) 21 (1)A> 445+V(1) 10
24 88+20*V(1) 4 [*]* 221+V(2) 21 115+V(1) (1)A> 10
25 90+20*V(1) 2 [*]* 221+V(2) 21 115+V(1) <A(4) 40
26 100+22*V(1) -8+-2*V(1) [*]* 221+V(2) 21 <A(4) 445+V(1) 40
27 104+22*V(1) -6+-2*V(1) [*]* 221+V(2) 11 (1)A> 445+V(1) 40
28 114+24*V(1) 4 [*]* 221+V(2) 116+V(1) (1)A> 40
<< Success! ==> defined new CTR 8 (PA)
28560 12325794 2038 12 221020 116 (1)A> 40
== Executing PA-CTR 8, V(1)=5, V(2)=1016, repcount=339, factor=5/3
38052 19280040 3394 12 223 111701 (1)A> 40
38053 19280042 3396 12 223 111702 (1)B>
38054 19280044 3394 12 223 111702 <A(1) 10
38055 19280046 3392 12 223 111701 <A(4) 41 10
38056 19283448 -10 12 223 <A(4) 441701 41 10
38057 19283450 -8 12 222 21 (1)A> 441701 41 10
38058 19286852 3394 12 222 21 111701 (1)A> 41 10
38059 19286856 3392 12 222 21 111701 <A(4) 44 10
38060 19290258 -10 12 222 21 <A(4) 441702 10
38061 19290262 -8 12 222 11 (1)A> 441702 10
38062 19293666 3396 12 222 111703 (1)A> 10
38063 19293668 3394 12 222 111703 <A(4) 40
38064 19297074 -12 12 222 <A(4) 441703 40
38065 19297076 -10 12 22 21 (1)A> 441703 40
38066 19300482 3396 12 22 21 111703 (1)A> 40
38067 19300484 3398 12 22 21 111704 (1)B>
38068 19300486 3396 12 22 21 111704 <A(1) 10
38069 19300488 3394 12 22 21 111703 <A(4) 41 10
38070 19303894 -12 12 22 21 <A(4) 441703 41 10
38071 19303898 -10 12 22 11 (1)A> 441703 41 10
38072 19307304 3396 12 22 111704 (1)A> 41 10
38073 19307308 3394 12 22 111704 <A(4) 44 10
38074 19310716 -14 12 22 <A(4) 441705 10
38075 19310718 -12 12 21 (1)A> 441705 10
38076 19314128 3398 12 21 111705 (1)A> 10
38077 19314130 3396 12 21 111705 <A(4) 40
38078 19317540 -14 12 21 <A(4) 441705 40
38079 19317544 -12 12 11 (1)A> 441705 40
38080 19320954 3398 12 111706 (1)A> 40
38081 19320956 3400 12 111707 (1)B>
38082 19320958 3398 12 111707 <A(1) 10
38083 19320960 3396 12 111706 <A(4) 41 10
38084 19324372 -16 12 <A(4) 441706 41 10
38085 19324374 -14 11 (1)A> 441706 41 10
38086 19327786 3398 111707 (1)A> 41 10
38087 19327790 3396 111707 <A(4) 44 10
38088 19331204 -18 <A(4) 441708 10
38089 19331206 -16 01 (2)B> 441708 10
38090 19334622 3400 01 221708 (2)B> 10
38091 19334626 3398 01 221708 <A(4) 40
38092 19334628 3400 01 221707 21 (1)A> 40
38093 19334630 3402 01 221707 21 11 (1)B>
38094 19334632 3400 01 221707 21 11 <A(1) 10
38095 19334634 3398 01 221707 21 <A(4) 41 10
38096 19334638 3400 01 221707 11 (1)A> 41 10
38097 19334642 3398 01 221707 11 <A(4) 44 10
38098 19334644 3396 01 221707 <A(4) 442 10
38099 19334646 3398 01 221706 21 (1)A> 442 10
38100 19334650 3402 01 221706 21 112 (1)A> 10
38101 19334652 3400 01 221706 21 112 <A(4) 40
38102 19334656 3396 01 221706 21 <A(4) 442 40
38103 19334660 3398 01 221706 11 (1)A> 442 40
38104 19334664 3402 01 221706 113 (1)A> 40
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 12 223 111+V(1) (1)A> 40
1 2 2 12 223 112+V(1) (1)B>
2 4 0 12 223 112+V(1) <A(1) 10
3 6 -2 12 223 111+V(1) <A(4) 41 10
4 8+2*V(1) -4+-2*V(1) 12 223 <A(4) 441+V(1) 41 10
5 10+2*V(1) -2+-2*V(1) 12 222 21 (1)A> 441+V(1) 41 10
6 12+4*V(1) 0 12 222 21 111+V(1) (1)A> 41 10
7 16+4*V(1) -2 12 222 21 111+V(1) <A(4) 44 10
8 18+6*V(1) -4+-2*V(1) 12 222 21 <A(4) 442+V(1) 10
9 22+6*V(1) -2+-2*V(1) 12 222 11 (1)A> 442+V(1) 10
10 26+8*V(1) 2 12 222 113+V(1) (1)A> 10
11 28+8*V(1) 0 12 222 113+V(1) <A(4) 40
12 34+10*V(1) -6+-2*V(1) 12 222 <A(4) 443+V(1) 40
13 36+10*V(1) -4+-2*V(1) 12 22 21 (1)A> 443+V(1) 40
14 42+12*V(1) 2 12 22 21 113+V(1) (1)A> 40
15 44+12*V(1) 4 12 22 21 114+V(1) (1)B>
16 46+12*V(1) 2 12 22 21 114+V(1) <A(1) 10
17 48+12*V(1) 0 12 22 21 113+V(1) <A(4) 41 10
18 54+14*V(1) -6+-2*V(1) 12 22 21 <A(4) 443+V(1) 41 10
19 58+14*V(1) -4+-2*V(1) 12 22 11 (1)A> 443+V(1) 41 10
20 64+16*V(1) 2 12 22 114+V(1) (1)A> 41 10
21 68+16*V(1) 0 12 22 114+V(1) <A(4) 44 10
22 76+18*V(1) -8+-2*V(1) 12 22 <A(4) 445+V(1) 10
23 78+18*V(1) -6+-2*V(1) 12 21 (1)A> 445+V(1) 10
24 88+20*V(1) 4 12 21 115+V(1) (1)A> 10
25 90+20*V(1) 2 12 21 115+V(1) <A(4) 40
26 100+22*V(1) -8+-2*V(1) 12 21 <A(4) 445+V(1) 40
27 104+22*V(1) -6+-2*V(1) 12 11 (1)A> 445+V(1) 40
28 114+24*V(1) 4 12 116+V(1) (1)A> 40
29 116+24*V(1) 6 12 117+V(1) (1)B>
30 118+24*V(1) 4 12 117+V(1) <A(1) 10
31 120+24*V(1) 2 12 116+V(1) <A(4) 41 10
32 132+26*V(1) -10+-2*V(1) 12 <A(4) 446+V(1) 41 10
33 134+26*V(1) -8+-2*V(1) 11 (1)A> 446+V(1) 41 10
34 146+28*V(1) 4 117+V(1) (1)A> 41 10
35 150+28*V(1) 2 117+V(1) <A(4) 44 10
36 164+30*V(1) -12+-2*V(1) <A(4) 448+V(1) 10
37 166+30*V(1) -10+-2*V(1) 01 (2)B> 448+V(1) 10
38 182+32*V(1) 6 01 228+V(1) (2)B> 10
39 186+32*V(1) 4 01 228+V(1) <A(4) 40
40 188+32*V(1) 6 01 227+V(1) 21 (1)A> 40
41 190+32*V(1) 8 01 227+V(1) 21 11 (1)B>
42 192+32*V(1) 6 01 227+V(1) 21 11 <A(1) 10
43 194+32*V(1) 4 01 227+V(1) 21 <A(4) 41 10
44 198+32*V(1) 6 01 227+V(1) 11 (1)A> 41 10
45 202+32*V(1) 4 01 227+V(1) 11 <A(4) 44 10
46 204+32*V(1) 2 01 227+V(1) <A(4) 442 10
47 206+32*V(1) 4 01 226+V(1) 21 (1)A> 442 10
48 210+32*V(1) 8 01 226+V(1) 21 112 (1)A> 10
49 212+32*V(1) 6 01 226+V(1) 21 112 <A(4) 40
50 216+32*V(1) 2 01 226+V(1) 21 <A(4) 442 40
51 220+32*V(1) 4 01 226+V(1) 11 (1)A> 442 40
52 224+32*V(1) 8 01 226+V(1) 113 (1)A> 40
<< Success! ==> defined new CTR 9 (PPA)
38104 19334664 3402 01 221706 113 (1)A> 40
== Executing PA-CTR 8, V(1)=2, V(2)=1702, repcount=568, factor=5/3
54008 38750040 5674 01 222 112843 (1)A> 40
54009 38750042 5676 01 222 112844 (1)B>
54010 38750044 5674 01 222 112844 <A(1) 10
54011 38750046 5672 01 222 112843 <A(4) 41 10
54012 38755732 -14 01 222 <A(4) 442843 41 10
54013 38755734 -12 01 22 21 (1)A> 442843 41 10
54014 38761420 5674 01 22 21 112843 (1)A> 41 10
54015 38761424 5672 01 22 21 112843 <A(4) 44 10
54016 38767110 -14 01 22 21 <A(4) 442844 10
54017 38767114 -12 01 22 11 (1)A> 442844 10
54018 38772802 5676 01 22 112845 (1)A> 10
54019 38772804 5674 01 22 112845 <A(4) 40
54020 38778494 -16 01 22 <A(4) 442845 40
54021 38778496 -14 01 21 (1)A> 442845 40
54022 38784186 5676 01 21 112845 (1)A> 40
54023 38784188 5678 01 21 112846 (1)B>
54024 38784190 5676 01 21 112846 <A(1) 10
54025 38784192 5674 01 21 112845 <A(4) 41 10
54026 38789882 -16 01 21 <A(4) 442845 41 10
54027 38789886 -14 01 11 (1)A> 442845 41 10
54028 38795576 5676 01 112846 (1)A> 41 10
54029 38795580 5674 01 112846 <A(4) 44 10
54030 38801272 -18 01 <A(4) 442847 10
54031 38801276 -16 12 (2)B> 442847 10
54032 38806970 5678 12 222847 (2)B> 10
54033 38806974 5676 12 222847 <A(4) 40
54034 38806976 5678 12 222846 21 (1)A> 40
54035 38806978 5680 12 222846 21 11 (1)B>
54036 38806980 5678 12 222846 21 11 <A(1) 10
54037 38806982 5676 12 222846 21 <A(4) 41 10
54038 38806986 5678 12 222846 11 (1)A> 41 10
54039 38806990 5676 12 222846 11 <A(4) 44 10
54040 38806992 5674 12 222846 <A(4) 442 10
54041 38806994 5676 12 222845 21 (1)A> 442 10
54042 38806998 5680 12 222845 21 112 (1)A> 10
54043 38807000 5678 12 222845 21 112 <A(4) 40
54044 38807004 5674 12 222845 21 <A(4) 442 40
54045 38807008 5676 12 222845 11 (1)A> 442 40
54046 38807012 5680 12 222845 113 (1)A> 40
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 01 222 112+V(1) (1)A> 40
1 2 2 01 222 113+V(1) (1)B>
2 4 0 01 222 113+V(1) <A(1) 10
3 6 -2 01 222 112+V(1) <A(4) 41 10
4 10+2*V(1) -6+-2*V(1) 01 222 <A(4) 442+V(1) 41 10
5 12+2*V(1) -4+-2*V(1) 01 22 21 (1)A> 442+V(1) 41 10
6 16+4*V(1) 0 01 22 21 112+V(1) (1)A> 41 10
7 20+4*V(1) -2 01 22 21 112+V(1) <A(4) 44 10
8 24+6*V(1) -6+-2*V(1) 01 22 21 <A(4) 443+V(1) 10
9 28+6*V(1) -4+-2*V(1) 01 22 11 (1)A> 443+V(1) 10
10 34+8*V(1) 2 01 22 114+V(1) (1)A> 10
11 36+8*V(1) 0 01 22 114+V(1) <A(4) 40
12 44+10*V(1) -8+-2*V(1) 01 22 <A(4) 444+V(1) 40
13 46+10*V(1) -6+-2*V(1) 01 21 (1)A> 444+V(1) 40
14 54+12*V(1) 2 01 21 114+V(1) (1)A> 40
15 56+12*V(1) 4 01 21 115+V(1) (1)B>
16 58+12*V(1) 2 01 21 115+V(1) <A(1) 10
17 60+12*V(1) 0 01 21 114+V(1) <A(4) 41 10
18 68+14*V(1) -8+-2*V(1) 01 21 <A(4) 444+V(1) 41 10
19 72+14*V(1) -6+-2*V(1) 01 11 (1)A> 444+V(1) 41 10
20 80+16*V(1) 2 01 115+V(1) (1)A> 41 10
21 84+16*V(1) 0 01 115+V(1) <A(4) 44 10
22 94+18*V(1) -10+-2*V(1) 01 <A(4) 446+V(1) 10
23 98+18*V(1) -8+-2*V(1) 12 (2)B> 446+V(1) 10
24 110+20*V(1) 4 12 226+V(1) (2)B> 10
25 114+20*V(1) 2 12 226+V(1) <A(4) 40
26 116+20*V(1) 4 12 225+V(1) 21 (1)A> 40
27 118+20*V(1) 6 12 225+V(1) 21 11 (1)B>
28 120+20*V(1) 4 12 225+V(1) 21 11 <A(1) 10
29 122+20*V(1) 2 12 225+V(1) 21 <A(4) 41 10
30 126+20*V(1) 4 12 225+V(1) 11 (1)A> 41 10
31 130+20*V(1) 2 12 225+V(1) 11 <A(4) 44 10
32 132+20*V(1) 0 12 225+V(1) <A(4) 442 10
33 134+20*V(1) 2 12 224+V(1) 21 (1)A> 442 10
34 138+20*V(1) 6 12 224+V(1) 21 112 (1)A> 10
35 140+20*V(1) 4 12 224+V(1) 21 112 <A(4) 40
36 144+20*V(1) 0 12 224+V(1) 21 <A(4) 442 40
37 148+20*V(1) 2 12 224+V(1) 11 (1)A> 442 40
38 152+20*V(1) 6 12 224+V(1) 113 (1)A> 40
<< Success! ==> defined new CTR 10 (PPA)
54046 38807012 5680 12 222845 113 (1)A> 40
== Executing PA-CTR 8, V(1)=2, V(2)=2841, repcount=948, factor=5/3
80590 92825948 9472 12 22 114743 (1)A> 40
80591 92825950 9474 12 22 114744 (1)B>
80592 92825952 9472 12 22 114744 <A(1) 10
80593 92825954 9470 12 22 114743 <A(4) 41 10
80594 92835440 -16 12 22 <A(4) 444743 41 10
80595 92835442 -14 12 21 (1)A> 444743 41 10
80596 92844928 9472 12 21 114743 (1)A> 41 10
80597 92844932 9470 12 21 114743 <A(4) 44 10
80598 92854418 -16 12 21 <A(4) 444744 10
80599 92854422 -14 12 11 (1)A> 444744 10
80600 92863910 9474 12 114745 (1)A> 10
80601 92863912 9472 12 114745 <A(4) 40
80602 92873402 -18 12 <A(4) 444745 40
80603 92873404 -16 11 (1)A> 444745 40
80604 92882894 9474 114746 (1)A> 40
80605 92882896 9476 114747 (1)B>
80606 92882898 9474 114747 <A(1) 10
80607 92882900 9472 114746 <A(4) 41 10
80608 92892392 -20 <A(4) 444746 41 10
80609 92892394 -18 01 (2)B> 444746 41 10
80610 92901886 9474 01 224746 (2)B> 41 10
80611 92901894 9476 01 224746 11 (1)A> 10
80612 92901896 9474 01 224746 11 <A(4) 40
80613 92901898 9472 01 224746 <A(4) 44 40
80614 92901900 9474 01 224745 21 (1)A> 44 40
80615 92901902 9476 01 224745 21 11 (1)A> 40
80616 92901904 9478 01 224745 21 112 (1)B>
80617 92901906 9476 01 224745 21 112 <A(1) 10
80618 92901908 9474 01 224745 21 11 <A(4) 41 10
80619 92901910 9472 01 224745 21 <A(4) 44 41 10
80620 92901914 9474 01 224745 11 (1)A> 44 41 10
80621 92901916 9476 01 224745 112 (1)A> 41 10
80622 92901920 9474 01 224745 112 <A(4) 44 10
80623 92901924 9470 01 224745 <A(4) 443 10
80624 92901926 9472 01 224744 21 (1)A> 443 10
80625 92901932 9478 01 224744 21 113 (1)A> 10
80626 92901934 9476 01 224744 21 113 <A(4) 40
80627 92901940 9470 01 224744 21 <A(4) 443 40
80628 92901944 9472 01 224744 11 (1)A> 443 40
80629 92901950 9478 01 224744 114 (1)A> 40
>> Try to prove a PPA-CTR with 1 Vars...
0 0 0 12 22 113+V(1) (1)A> 40
1 2 2 12 22 114+V(1) (1)B>
2 4 0 12 22 114+V(1) <A(1) 10
3 6 -2 12 22 113+V(1) <A(4) 41 10
4 12+2*V(1) -8+-2*V(1) 12 22 <A(4) 443+V(1) 41 10
5 14+2*V(1) -6+-2*V(1) 12 21 (1)A> 443+V(1) 41 10
6 20+4*V(1) 0 12 21 113+V(1) (1)A> 41 10
7 24+4*V(1) -2 12 21 113+V(1) <A(4) 44 10
8 30+6*V(1) -8+-2*V(1) 12 21 <A(4) 444+V(1) 10
9 34+6*V(1) -6+-2*V(1) 12 11 (1)A> 444+V(1) 10
10 42+8*V(1) 2 12 115+V(1) (1)A> 10
11 44+8*V(1) 0 12 115+V(1) <A(4) 40
12 54+10*V(1) -10+-2*V(1) 12 <A(4) 445+V(1) 40
13 56+10*V(1) -8+-2*V(1) 11 (1)A> 445+V(1) 40
14 66+12*V(1) 2 116+V(1) (1)A> 40
15 68+12*V(1) 4 117+V(1) (1)B>
16 70+12*V(1) 2 117+V(1) <A(1) 10
17 72+12*V(1) 0 116+V(1) <A(4) 41 10
18 84+14*V(1) -12+-2*V(1) <A(4) 446+V(1) 41 10
19 86+14*V(1) -10+-2*V(1) 01 (2)B> 446+V(1) 41 10
20 98+16*V(1) 2 01 226+V(1) (2)B> 41 10
21 106+16*V(1) 4 01 226+V(1) 11 (1)A> 10
22 108+16*V(1) 2 01 226+V(1) 11 <A(4) 40
23 110+16*V(1) 0 01 226+V(1) <A(4) 44 40
24 112+16*V(1) 2 01 225+V(1) 21 (1)A> 44 40
25 114+16*V(1) 4 01 225+V(1) 21 11 (1)A> 40
26 116+16*V(1) 6 01 225+V(1) 21 112 (1)B>
27 118+16*V(1) 4 01 225+V(1) 21 112 <A(1) 10
28 120+16*V(1) 2 01 225+V(1) 21 11 <A(4) 41 10
29 122+16*V(1) 0 01 225+V(1) 21 <A(4) 44 41 10
30 126+16*V(1) 2 01 225+V(1) 11 (1)A> 44 41 10
31 128+16*V(1) 4 01 225+V(1) 112 (1)A> 41 10
32 132+16*V(1) 2 01 225+V(1) 112 <A(4) 44 10
33 136+16*V(1) -2 01 225+V(1) <A(4) 443 10
34 138+16*V(1) 0 01 224+V(1) 21 (1)A> 443 10
35 144+16*V(1) 6 01 224+V(1) 21 113 (1)A> 10
36 146+16*V(1) 4 01 224+V(1) 21 113 <A(4) 40
37 152+16*V(1) -2 01 224+V(1) 21 <A(4) 443 40
38 156+16*V(1) 0 01 224+V(1) 11 (1)A> 443 40
39 162+16*V(1) 6 01 224+V(1) 114 (1)A> 40
<< Success! ==> defined new CTR 11 (PPA)
80629 92901950 9478 01 224744 114 (1)A> 40
== Executing PA-CTR 8, V(1)=3, V(2)=4740, repcount=1581, factor=5/3
124897 243074816 15802 01 22 117909 (1)A> 40
124898 243074818 15804 01 22 117910 (1)B>
124899 243074820 15802 01 22 117910 <A(1) 10
124900 243074822 15800 01 22 117909 <A(4) 41 10
124901 243090640 -18 01 22 <A(4) 447909 41 10
124902 243090642 -16 01 21 (1)A> 447909 41 10
124903 243106460 15802 01 21 117909 (1)A> 41 10
124904 243106464 15800 01 21 117909 <A(4) 44 10
124905 243122282 -18 01 21 <A(4) 447910 10
124906 243122286 -16 01 11 (1)A> 447910 10
124907 243138106 15804 01 117911 (1)A> 10
124908 243138108 15802 01 117911 <A(4) 40
124909 243153930 -20 01 <A(4) 447911 40
124910 243153934 -18 12 (2)B> 447911 40
124911 243169756 15804 12 227911 (2)B> 40
124912 243169762 15802 12 227911 <A(1) 31
124913 243169768 15804 12 227910 11 (1)A> 31
124914 243169770 15802 12 227910 11 <A(1) 51
124915 243169772 15800 12 227910 <A(4) 41 51
124916 243169774 15802 12 227909 21 (1)A> 41 51
124917 243169778 15800 12 227909 21 <A(4) 44 51
124918 243169782 15802 12 227909 11 (1)A> 44 51
124919 243169784 15804 12 227909 112 (1)A> 51
124920 243169786 15802 12 227909 112 <A(1) 31
124921 243169788 15800 12 227909 11 <A(4) 41 31
124922 243169790 15798 12 227909 <A(4) 44 41 31
124923 243169792 15800 12 227908 21 (1)A> 44 41 31
124924 243169794 15802 12 227908 21 11 (1)A> 41 31
124925 243169798 15800 12 227908 21 11 <A(4) 44 31
124926 243169800 15798 12 227908 21 <A(4) 442 31
124927 243169804 15800 12 227908 11 (1)A> 442 31
124928 243169808 15804 12 227908 113 (1)A> 31
124929 243169810 15802 12 227908 113 <A(1) 51
124930 243169812 15800 12 227908 112 <A(4) 41 51
124931 243169816 15796 12 227908 <A(4) 442 41 51
124932 243169818 15798 12 227907 21 (1)A> 442 41 51
124933 243169822 15802 12 227907 21 112 (1)A> 41 51
124934 243169826 15800 12 227907 21 112 <A(4) 44 51
124935 243169830 15796 12 227907 21 <A(4) 443 51
>> Try to prove a PA-CTR with 2 Vars...
0 0 0 [*]* 223+V(1) 21 <A(4) 441+V(2) 51
1 4 2 [*]* 223+V(1) 11 (1)A> 441+V(2) 51
2 6+2*V(2) 4+2*V(2) [*]* 223+V(1) 112+V(2) (1)A> 51
3 8+2*V(2) 2+2*V(2) [*]* 223+V(1) 112+V(2) <A(1) 31
4 10+2*V(2) 0+2*V(2) [*]* 223+V(1) 111+V(2) <A(4) 41 31
5 12+4*V(2) -2 [*]* 223+V(1) <A(4) 441+V(2) 41 31
6 14+4*V(2) 0 [*]* 222+V(1) 21 (1)A> 441+V(2) 41 31
7 16+6*V(2) 2+2*V(2) [*]* 222+V(1) 21 111+V(2) (1)A> 41 31
8 20+6*V(2) 0+2*V(2) [*]* 222+V(1) 21 111+V(2) <A(4) 44 31
9 22+8*V(2) -2 [*]* 222+V(1) 21 <A(4) 442+V(2) 31
10 26+8*V(2) 0 [*]* 222+V(1) 11 (1)A> 442+V(2) 31
11 30+10*V(2) 4+2*V(2) [*]* 222+V(1) 113+V(2) (1)A> 31
12 32+10*V(2) 2+2*V(2) [*]* 222+V(1) 113+V(2) <A(1) 51
13 34+10*V(2) 0+2*V(2) [*]* 222+V(1) 112+V(2) <A(4) 41 51
14 38+12*V(2) -4 [*]* 222+V(1) <A(4) 442+V(2) 41 51
15 40+12*V(2) -2 [*]* 221+V(1) 21 (1)A> 442+V(2) 41 51
16 44+14*V(2) 2+2*V(2) [*]* 221+V(1) 21 112+V(2) (1)A> 41 51
17 48+14*V(2) 0+2*V(2) [*]* 221+V(1) 21 112+V(2) <A(4) 44 51
18 52+16*V(2) -4 [*]* 221+V(1) 21 <A(4) 443+V(2) 51
<< Success! ==> defined new CTR 12 (PA)
124935 243169830 15796 12 227907 21 <A(4) 443 51
== Executing PA-CTR 12, V(1)=7904, V(2)=2, repcount=3953, factor=2/2
196089 493457978 -16 12 22 21 <A(4) 447909 51
196090 493457982 -14 12 22 11 (1)A> 447909 51
196091 493473800 15804 12 22 117910 (1)A> 51
196092 493473802 15802 12 22 117910 <A(1) 31
196093 493473804 15800 12 22 117909 <A(4) 41 31
196094 493489622 -18 12 22 <A(4) 447909 41 31
196095 493489624 -16 12 21 (1)A> 447909 41 31
196096 493505442 15802 12 21 117909 (1)A> 41 31
196097 493505446 15800 12 21 117909 <A(4) 44 31
196098 493521264 -18 12 21 <A(4) 447910 31
196099 493521268 -16 12 11 (1)A> 447910 31
196100 493537088 15804 12 117911 (1)A> 31
196101 493537090 15802 12 117911 <A(1) 51
196102 493537092 15800 12 117910 <A(4) 41 51
196103 493552912 -20 12 <A(4) 447910 41 51
196104 493552914 -18 11 (1)A> 447910 41 51
196105 493568734 15802 117911 (1)A> 41 51
196106 493568738 15800 117911 <A(4) 44 51
196107 493584560 -22 <A(4) 447912 51
196108 493584562 -20 01 (2)B> 447912 51
196109 493600386 15804 01 227912 (2)B> 51
196110 493600387 15805 01 227912 21 H> 1 [stop]
Lines: 481
Top steps: 480
Macro steps: 196110
Basic steps: 493600387
Tape index: 15805
nonzeros: 15828
log10(nonzeros): 4.199
log10(steps ): 8.693
Run state: stop
Input to awk program:
gohalt 1
nbs 6
T 2-state 6-symbol #c (T.J. & S. Ligocki)
: 15828 493,600,387
5T 1RB 4LA 1RA 5LB 1RA 3LB 1LB 1LA 5LA 2LA 2RB 1RH
L 10
M 500
pref sim
machv Lig26_c just simple
machv Lig26_c-r with repetitions reduced
machv Lig26_c-1 with tape symbol exponents
machv Lig26_c-m as bck-2-macro machine
machv Lig26_c-a as bck-2-macro machine with pure additive config-TRs
iam Lig26_c-a
mtype 0 2
mmtyp 3
r 1
H 1
mac 0
E 2
sympr
HM 1
date Tue Jul 6 22:13:14 CEST 2010
edate Tue Jul 6 22:13:16 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:13:14 CEST 2010