"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"m2 = read_csv('tm-m2.csv')\n",
"m2"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This machine converts to a 2-tag system with 450 rules. The rules look like CFG rules, but they work differently. (Match the first symbol with a rule's left-hand side, remove the first *two* symbols, and append the right-hand side.)"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"('A',_0,_1) -> ('C',_0,_1) x ('c',_0,_1) x\r\n",
"('α',_0,_1) -> ('c',_0,_1) x ('c',_0,_1) x\r\n",
"('B',_0,_1) -> ('S',_0,_1)\r\n",
"('β',_0,_1) -> ('s',_0,_1)\r\n",
"('C',_0,_1) -> ('D',_(0,_'read1'),_1) ('D',_(0,_'read1'),_0)\r\n",
"('c',_0,_1) -> ('d',_(0,_'read1'),_1) ('d',_(0,_'read1'),_0)\r\n",
"('S',_0,_1) -> ('T',_(0,_'read1'),_1) ('T',_(0,_'read1'),_0)\r\n",
"('s',_0,_1) -> ('t',_(0,_'read1'),_1) ('t',_(0,_'read1'),_0)\r\n",
"('D',_0,_1) -> ('A',_0,_1) x\r\n",
"('d',_0,_1) -> ('α',_0,_1) x\r\n",
"('T',_0,_1) -> ('B',_0,_1) x\r\n",
"('t',_0,_1) -> ('β',_0,_1) x\r\n",
"('D',_(0,_'read1'),_0) -> x ('A',_(0,_'read1'),_0) x\r\n",
"('d',_(0,_'read1'),_0) -> ('α',_(0,_'read1'),_0) x\r\n",
"('T',_(0,_'read1'),_0) -> ('B',_(0,_'read1'),_0) x\r\n",
"('t',_(0,_'read1'),_0) -> ('β',_(0,_'read1'),_0) x\r\n",
"('A',_(0,_'write0',_'move+2'),_1) -> ('C',_(0,_'write0',_'move+2'),_1) x\r\n",
"('α',_(0,_'write0',_'move+2'),_1) -> ('c',_(0,_'write0',_'move+2'),_1) x ('c',_(0,_'write0',_'move+2'),_1) x\r\n",
"('B',_(0,_'write0',_'move+2'),_1) -> ('S',_(0,_'write0',_'move+2'),_1)\r\n",
"('β',_(0,_'write0',_'move+2'),_1) -> ('s',_(0,_'write0',_'move+2'),_1)\r\n",
"('C',_(0,_'write0',_'move+2'),_1) -> ('D',_(0,_'move+1'),_1) ('D',_(0,_'move+1'),_0)\r\n",
"('c',_(0,_'write0',_'move+2'),_1) -> ('d',_(0,_'move+1'),_1) ('d',_(0,_'move+1'),_0)\r\n",
"('S',_(0,_'write0',_'move+2'),_1) -> ('T',_(0,_'move+1'),_1) ('T',_(0,_'move+1'),_0)\r\n",
"('s',_(0,_'write0',_'move+2'),_1) -> ('t',_(0,_'move+1'),_1) ('t',_(0,_'move+1'),_0)\r\n",
"('D',_(0,_'write0',_'move+2'),_1) -> ('A',_(0,_'write0',_'move+2'),_1) x\r\n",
"('d',_(0,_'write0',_'move+2'),_1) -> ('α',_(0,_'write0',_'move+2'),_1) x\r\n",
"('T',_(0,_'write0',_'move+2'),_1) -> ('B',_(0,_'write0',_'move+2'),_1) x\r\n",
"('t',_(0,_'write0',_'move+2'),_1) -> ('β',_(0,_'write0',_'move+2'),_1) x\r\n",
"('A',_(0,_'move+1'),_0) -> ('C',_(0,_'move+1'),_0) x\r\n",
"('α',_(0,_'move+1'),_0) -> ('c',_(0,_'move+1'),_0) x ('c',_(0,_'move+1'),_0) x\r\n",
"('B',_(0,_'move+1'),_0) -> ('S',_(0,_'move+1'),_0)\r\n",
"('β',_(0,_'move+1'),_0) -> ('s',_(0,_'move+1'),_0)\r\n",
"('C',_(0,_'move+1'),_0) -> ('D',_1,_1) ('D',_1,_0)\r\n",
"('c',_(0,_'move+1'),_0) -> ('d',_1,_1) ('d',_1,_0)\r\n",
"('S',_(0,_'move+1'),_0) -> ('T',_1,_1) ('T',_1,_0)\r\n",
"('s',_(0,_'move+1'),_0) -> ('t',_1,_1) ('t',_1,_0)\r\n",
"('D',_(0,_'move+1'),_0) -> x ('A',_(0,_'move+1'),_0) x\r\n",
"('d',_(0,_'move+1'),_0) -> ('α',_(0,_'move+1'),_0) x\r\n",
"('T',_(0,_'move+1'),_0) -> ('B',_(0,_'move+1'),_0) x\r\n",
"('t',_(0,_'move+1'),_0) -> ('β',_(0,_'move+1'),_0) x\r\n",
"('A',_1,_0) -> ('C',_1,_0) x\r\n",
"('α',_1,_0) -> ('c',_1,_0) x ('c',_1,_0) x\r\n",
"('B',_1,_0) -> ('S',_1,_0)\r\n",
"('β',_1,_0) -> ('s',_1,_0)\r\n",
"('C',_1,_0) -> ('D',_(1,_'read0'),_1) ('D',_(1,_'read0'),_0)\r\n",
"('c',_1,_0) -> ('d',_(1,_'read0'),_1) ('d',_(1,_'read0'),_0)\r\n",
"('S',_1,_0) -> ('T',_(1,_'read0'),_1) ('T',_(1,_'read0'),_0)\r\n",
"('s',_1,_0) -> ('t',_(1,_'read0'),_1) ('t',_(1,_'read0'),_0)\r\n",
"('D',_1,_0) -> x ('A',_1,_0) x\r\n",
"('d',_1,_0) -> ('α',_1,_0) x\r\n",
"('T',_1,_0) -> ('B',_1,_0) x\r\n",
"('t',_1,_0) -> ('β',_1,_0) x\r\n",
"('A',_(1,_'read0'),_0) -> ('C',_(1,_'read0'),_0) x\r\n",
"('α',_(1,_'read0'),_0) -> ('c',_(1,_'read0'),_0) x ('c',_(1,_'read0'),_0) x\r\n",
"('B',_(1,_'read0'),_0) -> ('S',_(1,_'read0'),_0)\r\n",
"('β',_(1,_'read0'),_0) -> ('s',_(1,_'read0'),_0)\r\n",
"('C',_(1,_'read0'),_0) -> H H\r\n",
"('c',_(1,_'read0'),_0) -> ('d',_-1,_1) ('d',_-1,_0)\r\n",
"('S',_(1,_'read0'),_0) -> ('T',_-1,_1) ('T',_-1,_0)\r\n",
"('s',_(1,_'read0'),_0) -> ('t',_-1,_1) ('t',_-1,_0)\r\n",
"('D',_(1,_'read0'),_0) -> x ('A',_(1,_'read0'),_0) x\r\n",
"('d',_(1,_'read0'),_0) -> ('α',_(1,_'read0'),_0) x\r\n",
"('T',_(1,_'read0'),_0) -> ('B',_(1,_'read0'),_0) x\r\n",
"('t',_(1,_'read0'),_0) -> ('β',_(1,_'read0'),_0) x\r\n",
"('A',_(1,_'read0'),_1) -> ('C',_(1,_'read0'),_1) x ('c',_(1,_'read0'),_1) x\r\n",
"('α',_(1,_'read0'),_1) -> ('c',_(1,_'read0'),_1) x ('c',_(1,_'read0'),_1) x\r\n",
"('B',_(1,_'read0'),_1) -> ('S',_(1,_'read0'),_1)\r\n",
"('β',_(1,_'read0'),_1) -> ('s',_(1,_'read0'),_1)\r\n",
"('C',_(1,_'read0'),_1) -> ('D',_1,_1) ('D',_1,_0)\r\n",
"('c',_(1,_'read0'),_1) -> ('d',_1,_1) ('d',_1,_0)\r\n",
"('S',_(1,_'read0'),_1) -> ('T',_1,_1) ('T',_1,_0)\r\n",
"('s',_(1,_'read0'),_1) -> ('t',_1,_1) ('t',_1,_0)\r\n",
"('D',_(1,_'read0'),_1) -> ('A',_(1,_'read0'),_1) x\r\n",
"('d',_(1,_'read0'),_1) -> ('α',_(1,_'read0'),_1) x\r\n",
"('T',_(1,_'read0'),_1) -> ('B',_(1,_'read0'),_1) x\r\n",
"('t',_(1,_'read0'),_1) -> ('β',_(1,_'read0'),_1) x\r\n",
"('A',_1,_1) -> ('C',_1,_1) x ('c',_1,_1) x\r\n",
"('α',_1,_1) -> ('c',_1,_1) x ('c',_1,_1) x\r\n",
"('B',_1,_1) -> ('S',_1,_1)\r\n",
"('β',_1,_1) -> ('s',_1,_1)\r\n",
"('C',_1,_1) -> ('D',_(1,_'read1'),_1) ('D',_(1,_'read1'),_0)\r\n",
"('c',_1,_1) -> ('d',_(1,_'read1'),_1) ('d',_(1,_'read1'),_0)\r\n",
"('S',_1,_1) -> ('T',_(1,_'read1'),_1) ('T',_(1,_'read1'),_0)\r\n",
"('s',_1,_1) -> ('t',_(1,_'read1'),_1) ('t',_(1,_'read1'),_0)\r\n",
"('D',_1,_1) -> ('A',_1,_1) x\r\n",
"('d',_1,_1) -> ('α',_1,_1) x\r\n",
"('T',_1,_1) -> ('B',_1,_1) x\r\n",
"('t',_1,_1) -> ('β',_1,_1) x\r\n",
"('D',_(1,_'read1'),_0) -> x ('A',_(1,_'read1'),_0) x\r\n",
"('d',_(1,_'read1'),_0) -> ('α',_(1,_'read1'),_0) x\r\n",
"('T',_(1,_'read1'),_0) -> ('B',_(1,_'read1'),_0) x\r\n",
"('t',_(1,_'read1'),_0) -> ('β',_(1,_'read1'),_0) x\r\n",
"('A',_(1,_'write0',_'move+2'),_1) -> ('C',_(1,_'write0',_'move+2'),_1) x\r\n",
"('α',_(1,_'write0',_'move+2'),_1) -> ('c',_(1,_'write0',_'move+2'),_1) x ('c',_(1,_'write0',_'move+2'),_1) x\r\n",
"('B',_(1,_'write0',_'move+2'),_1) -> ('S',_(1,_'write0',_'move+2'),_1)\r\n",
"('β',_(1,_'write0',_'move+2'),_1) -> ('s',_(1,_'write0',_'move+2'),_1)\r\n",
"('C',_(1,_'write0',_'move+2'),_1) -> ('D',_(1,_'move+1'),_1) ('D',_(1,_'move+1'),_0)\r\n",
"('c',_(1,_'write0',_'move+2'),_1) -> ('d',_(1,_'move+1'),_1) ('d',_(1,_'move+1'),_0)\r\n",
"('S',_(1,_'write0',_'move+2'),_1) -> ('T',_(1,_'move+1'),_1) ('T',_(1,_'move+1'),_0)\r\n",
"('s',_(1,_'write0',_'move+2'),_1) -> ('t',_(1,_'move+1'),_1) ('t',_(1,_'move+1'),_0)\r\n",
"('D',_(1,_'write0',_'move+2'),_1) -> ('A',_(1,_'write0',_'move+2'),_1) x\r\n",
"('d',_(1,_'write0',_'move+2'),_1) -> ('α',_(1,_'write0',_'move+2'),_1) x\r\n",
"('T',_(1,_'write0',_'move+2'),_1) -> ('B',_(1,_'write0',_'move+2'),_1) x\r\n",
"('t',_(1,_'write0',_'move+2'),_1) -> ('β',_(1,_'write0',_'move+2'),_1) x\r\n",
"('A',_(1,_'move+1'),_1) -> ('C',_(1,_'move+1'),_1) x ('c',_(1,_'move+1'),_1) x\r\n",
"('α',_(1,_'move+1'),_1) -> ('c',_(1,_'move+1'),_1) x ('c',_(1,_'move+1'),_1) x\r\n",
"('B',_(1,_'move+1'),_1) -> ('S',_(1,_'move+1'),_1)\r\n",
"('β',_(1,_'move+1'),_1) -> ('s',_(1,_'move+1'),_1)\r\n",
"('C',_(1,_'move+1'),_1) -> ('D',_2,_1) ('D',_2,_0)\r\n",
"('c',_(1,_'move+1'),_1) -> ('d',_2,_1) ('d',_2,_0)\r\n",
"('S',_(1,_'move+1'),_1) -> ('T',_2,_1) ('T',_2,_0)\r\n",
"('s',_(1,_'move+1'),_1) -> ('t',_2,_1) ('t',_2,_0)\r\n",
"('D',_(1,_'move+1'),_1) -> ('A',_(1,_'move+1'),_1) x\r\n",
"('d',_(1,_'move+1'),_1) -> ('α',_(1,_'move+1'),_1) x\r\n",
"('T',_(1,_'move+1'),_1) -> ('B',_(1,_'move+1'),_1) x\r\n",
"('t',_(1,_'move+1'),_1) -> ('β',_(1,_'move+1'),_1) x\r\n",
"('A',_2,_0) -> ('C',_2,_0) x\r\n",
"('α',_2,_0) -> ('c',_2,_0) x ('c',_2,_0) x\r\n",
"('B',_2,_0) -> ('S',_2,_0)\r\n",
"('β',_2,_0) -> ('s',_2,_0)\r\n",
"('C',_2,_0) -> ('D',_(2,_'read0'),_1) ('D',_(2,_'read0'),_0)\r\n",
"('c',_2,_0) -> ('d',_(2,_'read0'),_1) ('d',_(2,_'read0'),_0)\r\n",
"('S',_2,_0) -> ('T',_(2,_'read0'),_1) ('T',_(2,_'read0'),_0)\r\n",
"('s',_2,_0) -> ('t',_(2,_'read0'),_1) ('t',_(2,_'read0'),_0)\r\n",
"('D',_2,_0) -> x ('A',_2,_0) x\r\n",
"('d',_2,_0) -> ('α',_2,_0) x\r\n",
"('T',_2,_0) -> ('B',_2,_0) x\r\n",
"('t',_2,_0) -> ('β',_2,_0) x\r\n",
"('D',_(2,_'read0'),_0) -> x ('A',_(2,_'read0'),_0) x\r\n",
"('d',_(2,_'read0'),_0) -> ('α',_(2,_'read0'),_0) x\r\n",
"('T',_(2,_'read0'),_0) -> ('B',_(2,_'read0'),_0) x\r\n",
"('t',_(2,_'read0'),_0) -> ('β',_(2,_'read0'),_0) x\r\n",
"('D',_(2,_'write0',_'move-2'),_0) -> x ('A',_(2,_'write0',_'move-2'),_0) x\r\n",
"('d',_(2,_'write0',_'move-2'),_0) -> ('α',_(2,_'write0',_'move-2'),_0) x\r\n",
"('T',_(2,_'write0',_'move-2'),_0) -> ('B',_(2,_'write0',_'move-2'),_0) x\r\n",
"('t',_(2,_'write0',_'move-2'),_0) -> ('β',_(2,_'write0',_'move-2'),_0) x\r\n",
"('D',_(2,_'move-1'),_0) -> x ('A',_(2,_'move-1'),_0) x\r\n",
"('d',_(2,_'move-1'),_0) -> ('α',_(2,_'move-1'),_0) x\r\n",
"('T',_(2,_'move-1'),_0) -> ('B',_(2,_'move-1'),_0) x\r\n",
"('t',_(2,_'move-1'),_0) -> ('β',_(2,_'move-1'),_0) x\r\n",
"('D',_(2,_'move-1'),_1) -> ('A',_(2,_'move-1'),_1) x\r\n",
"('d',_(2,_'move-1'),_1) -> ('α',_(2,_'move-1'),_1) x\r\n",
"('T',_(2,_'move-1'),_1) -> ('B',_(2,_'move-1'),_1) x\r\n",
"('t',_(2,_'move-1'),_1) -> ('β',_(2,_'move-1'),_1) x\r\n",
"('A',_(2,_'read0'),_1) -> ('C',_(2,_'read0'),_1) x ('c',_(2,_'read0'),_1) x\r\n",
"('α',_(2,_'read0'),_1) -> ('c',_(2,_'read0'),_1) x ('c',_(2,_'read0'),_1) x\r\n",
"('B',_(2,_'read0'),_1) -> ('S',_(2,_'read0'),_1)\r\n",
"('β',_(2,_'read0'),_1) -> ('s',_(2,_'read0'),_1)\r\n",
"('C',_(2,_'read0'),_1) -> ('D',_2,_1) ('D',_2,_0)\r\n",
"('c',_(2,_'read0'),_1) -> ('d',_2,_1) ('d',_2,_0)\r\n",
"('S',_(2,_'read0'),_1) -> ('T',_2,_1) ('T',_2,_0)\r\n",
"('s',_(2,_'read0'),_1) -> ('t',_2,_1) ('t',_2,_0)\r\n",
"('D',_(2,_'read0'),_1) -> ('A',_(2,_'read0'),_1) x\r\n",
"('d',_(2,_'read0'),_1) -> ('α',_(2,_'read0'),_1) x\r\n",
"('T',_(2,_'read0'),_1) -> ('B',_(2,_'read0'),_1) x\r\n",
"('t',_(2,_'read0'),_1) -> ('β',_(2,_'read0'),_1) x\r\n",
"('A',_2,_1) -> ('C',_2,_1) x ('c',_2,_1) x\r\n",
"('α',_2,_1) -> ('c',_2,_1) x ('c',_2,_1) x\r\n",
"('B',_2,_1) -> ('S',_2,_1)\r\n",
"('β',_2,_1) -> ('s',_2,_1)\r\n",
"('C',_2,_1) -> ('D',_(2,_'read1'),_1) ('D',_(2,_'read1'),_0)\r\n",
"('c',_2,_1) -> ('d',_(2,_'read1'),_1) ('d',_(2,_'read1'),_0)\r\n",
"('S',_2,_1) -> ('T',_(2,_'read1'),_1) ('T',_(2,_'read1'),_0)\r\n",
"('s',_2,_1) -> ('t',_(2,_'read1'),_1) ('t',_(2,_'read1'),_0)\r\n",
"('D',_2,_1) -> ('A',_2,_1) x\r\n",
"('d',_2,_1) -> ('α',_2,_1) x\r\n",
"('T',_2,_1) -> ('B',_2,_1) x\r\n",
"('t',_2,_1) -> ('β',_2,_1) x\r\n",
"('A',_(2,_'read1'),_0) -> ('C',_(2,_'read1'),_0) x\r\n",
"('α',_(2,_'read1'),_0) -> ('c',_(2,_'read1'),_0) x ('c',_(2,_'read1'),_0) x\r\n",
"('B',_(2,_'read1'),_0) -> ('S',_(2,_'read1'),_0)\r\n",
"('β',_(2,_'read1'),_0) -> ('s',_(2,_'read1'),_0)\r\n",
"('C',_(2,_'read1'),_0) -> ('D',_3,_1) ('D',_3,_0)\r\n",
"('c',_(2,_'read1'),_0) -> ('d',_3,_1) ('d',_3,_0)\r\n",
"('S',_(2,_'read1'),_0) -> ('T',_3,_1) ('T',_3,_0)\r\n",
"('s',_(2,_'read1'),_0) -> ('t',_3,_1) ('t',_3,_0)\r\n",
"('D',_(2,_'read1'),_0) -> x ('A',_(2,_'read1'),_0) x\r\n",
"('d',_(2,_'read1'),_0) -> ('α',_(2,_'read1'),_0) x\r\n",
"('T',_(2,_'read1'),_0) -> ('B',_(2,_'read1'),_0) x\r\n",
"('t',_(2,_'read1'),_0) -> ('β',_(2,_'read1'),_0) x\r\n",
"('A',_3,_0) -> ('C',_3,_0) x\r\n",
"('α',_3,_0) -> ('c',_3,_0) x ('c',_3,_0) x\r\n",
"('B',_3,_0) -> ('S',_3,_0)\r\n",
"('β',_3,_0) -> ('s',_3,_0)\r\n",
"('C',_3,_0) -> ('D',_(3,_'read0'),_1) ('D',_(3,_'read0'),_0)\r\n",
"('c',_3,_0) -> ('d',_(3,_'read0'),_1) ('d',_(3,_'read0'),_0)\r\n",
"('S',_3,_0) -> ('T',_(3,_'read0'),_1) ('T',_(3,_'read0'),_0)\r\n",
"('s',_3,_0) -> ('t',_(3,_'read0'),_1) ('t',_(3,_'read0'),_0)\r\n",
"('D',_3,_0) -> x ('A',_3,_0) x\r\n",
"('d',_3,_0) -> ('α',_3,_0) x\r\n",
"('T',_3,_0) -> ('B',_3,_0) x\r\n",
"('t',_3,_0) -> ('β',_3,_0) x\r\n",
"('A',_(3,_'read0'),_1) -> ('C',_(3,_'read0'),_1) x ('c',_(3,_'read0'),_1) x\r\n",
"('α',_(3,_'read0'),_1) -> ('c',_(3,_'read0'),_1) x ('c',_(3,_'read0'),_1) x\r\n",
"('B',_(3,_'read0'),_1) -> ('S',_(3,_'read0'),_1)\r\n",
"('β',_(3,_'read0'),_1) -> ('s',_(3,_'read0'),_1)\r\n",
"('C',_(3,_'read0'),_1) -> ('D',_3,_1) ('D',_3,_0)\r\n",
"('c',_(3,_'read0'),_1) -> ('d',_3,_1) ('d',_3,_0)\r\n",
"('S',_(3,_'read0'),_1) -> ('T',_3,_1) ('T',_3,_0)\r\n",
"('s',_(3,_'read0'),_1) -> ('t',_3,_1) ('t',_3,_0)\r\n",
"('D',_(3,_'read0'),_1) -> ('A',_(3,_'read0'),_1) x\r\n",
"('d',_(3,_'read0'),_1) -> ('α',_(3,_'read0'),_1) x\r\n",
"('T',_(3,_'read0'),_1) -> ('B',_(3,_'read0'),_1) x\r\n",
"('t',_(3,_'read0'),_1) -> ('β',_(3,_'read0'),_1) x\r\n",
"('A',_3,_1) -> ('C',_3,_1) x ('c',_3,_1) x\r\n",
"('α',_3,_1) -> ('c',_3,_1) x ('c',_3,_1) x\r\n",
"('B',_3,_1) -> ('S',_3,_1)\r\n",
"('β',_3,_1) -> ('s',_3,_1)\r\n",
"('C',_3,_1) -> ('D',_(3,_'read1'),_1) ('D',_(3,_'read1'),_0)\r\n",
"('c',_3,_1) -> ('d',_(3,_'read1'),_1) ('d',_(3,_'read1'),_0)\r\n",
"('S',_3,_1) -> ('T',_(3,_'read1'),_1) ('T',_(3,_'read1'),_0)\r\n",
"('s',_3,_1) -> ('t',_(3,_'read1'),_1) ('t',_(3,_'read1'),_0)\r\n",
"('D',_3,_1) -> ('A',_3,_1) x\r\n",
"('d',_3,_1) -> ('α',_3,_1) x\r\n",
"('T',_3,_1) -> ('B',_3,_1) x\r\n",
"('t',_3,_1) -> ('β',_3,_1) x\r\n",
"('D',_(3,_'read1'),_0) -> x ('A',_(3,_'read1'),_0) x\r\n",
"('d',_(3,_'read1'),_0) -> ('α',_(3,_'read1'),_0) x\r\n",
"('T',_(3,_'read1'),_0) -> ('B',_(3,_'read1'),_0) x\r\n",
"('t',_(3,_'read1'),_0) -> ('β',_(3,_'read1'),_0) x\r\n",
"('A',_(3,_'write0',_'move+2'),_1) -> ('C',_(3,_'write0',_'move+2'),_1) x\r\n",
"('α',_(3,_'write0',_'move+2'),_1) -> ('c',_(3,_'write0',_'move+2'),_1) x ('c',_(3,_'write0',_'move+2'),_1) x\r\n",
"('B',_(3,_'write0',_'move+2'),_1) -> ('S',_(3,_'write0',_'move+2'),_1)\r\n",
"('β',_(3,_'write0',_'move+2'),_1) -> ('s',_(3,_'write0',_'move+2'),_1)\r\n",
"('C',_(3,_'write0',_'move+2'),_1) -> ('D',_(3,_'move+1'),_1) ('D',_(3,_'move+1'),_0)\r\n",
"('c',_(3,_'write0',_'move+2'),_1) -> ('d',_(3,_'move+1'),_1) ('d',_(3,_'move+1'),_0)\r\n",
"('S',_(3,_'write0',_'move+2'),_1) -> ('T',_(3,_'move+1'),_1) ('T',_(3,_'move+1'),_0)\r\n",
"('s',_(3,_'write0',_'move+2'),_1) -> ('t',_(3,_'move+1'),_1) ('t',_(3,_'move+1'),_0)\r\n",
"('D',_(3,_'write0',_'move+2'),_1) -> ('A',_(3,_'write0',_'move+2'),_1) x\r\n",
"('d',_(3,_'write0',_'move+2'),_1) -> ('α',_(3,_'write0',_'move+2'),_1) x\r\n",
"('T',_(3,_'write0',_'move+2'),_1) -> ('B',_(3,_'write0',_'move+2'),_1) x\r\n",
"('t',_(3,_'write0',_'move+2'),_1) -> ('β',_(3,_'write0',_'move+2'),_1) x\r\n",
"('A',_(3,_'move+1'),_1) -> ('C',_(3,_'move+1'),_1) x ('c',_(3,_'move+1'),_1) x\r\n",
"('α',_(3,_'move+1'),_1) -> ('c',_(3,_'move+1'),_1) x ('c',_(3,_'move+1'),_1) x\r\n",
"('B',_(3,_'move+1'),_1) -> ('S',_(3,_'move+1'),_1)\r\n",
"('β',_(3,_'move+1'),_1) -> ('s',_(3,_'move+1'),_1)\r\n",
"('C',_(3,_'move+1'),_1) -> ('D',_2,_1) ('D',_2,_0)\r\n",
"('c',_(3,_'move+1'),_1) -> ('d',_2,_1) ('d',_2,_0)\r\n",
"('S',_(3,_'move+1'),_1) -> ('T',_2,_1) ('T',_2,_0)\r\n",
"('s',_(3,_'move+1'),_1) -> ('t',_2,_1) ('t',_2,_0)\r\n",
"('D',_(3,_'move+1'),_1) -> ('A',_(3,_'move+1'),_1) x\r\n",
"('d',_(3,_'move+1'),_1) -> ('α',_(3,_'move+1'),_1) x\r\n",
"('T',_(3,_'move+1'),_1) -> ('B',_(3,_'move+1'),_1) x\r\n",
"('t',_(3,_'move+1'),_1) -> ('β',_(3,_'move+1'),_1) x\r\n",
"('A',_4,_0) -> ('C',_4,_0) x\r\n",
"('α',_4,_0) -> ('c',_4,_0) x ('c',_4,_0) x\r\n",
"('B',_4,_0) -> ('S',_4,_0)\r\n",
"('β',_4,_0) -> ('s',_4,_0)\r\n",
"('C',_4,_0) -> ('D',_(4,_'read0'),_1) ('D',_(4,_'read0'),_0)\r\n",
"('c',_4,_0) -> ('d',_(4,_'read0'),_1) ('d',_(4,_'read0'),_0)\r\n",
"('S',_4,_0) -> ('T',_(4,_'read0'),_1) ('T',_(4,_'read0'),_0)\r\n",
"('s',_4,_0) -> ('t',_(4,_'read0'),_1) ('t',_(4,_'read0'),_0)\r\n",
"('D',_4,_0) -> x ('A',_4,_0) x\r\n",
"('d',_4,_0) -> ('α',_4,_0) x\r\n",
"('T',_4,_0) -> ('B',_4,_0) x\r\n",
"('t',_4,_0) -> ('β',_4,_0) x\r\n",
"('A',_(4,_'read0'),_0) -> ('C',_(4,_'read0'),_0) x\r\n",
"('α',_(4,_'read0'),_0) -> ('c',_(4,_'read0'),_0) x ('c',_(4,_'read0'),_0) x\r\n",
"('B',_(4,_'read0'),_0) -> ('S',_(4,_'read0'),_0)\r\n",
"('β',_(4,_'read0'),_0) -> ('s',_(4,_'read0'),_0)\r\n",
"('C',_(4,_'read0'),_0) -> ('D',_1,_1) ('D',_1,_0)\r\n",
"('c',_(4,_'read0'),_0) -> ('d',_1,_1) ('d',_1,_0)\r\n",
"('S',_(4,_'read0'),_0) -> ('T',_1,_1) ('T',_1,_0)\r\n",
"('s',_(4,_'read0'),_0) -> ('t',_1,_1) ('t',_1,_0)\r\n",
"('D',_(4,_'read0'),_0) -> x ('A',_(4,_'read0'),_0) x\r\n",
"('d',_(4,_'read0'),_0) -> ('α',_(4,_'read0'),_0) x\r\n",
"('T',_(4,_'read0'),_0) -> ('B',_(4,_'read0'),_0) x\r\n",
"('t',_(4,_'read0'),_0) -> ('β',_(4,_'read0'),_0) x\r\n",
"('D',_(4,_'read0'),_1) -> ('A',_(4,_'read0'),_1) x\r\n",
"('d',_(4,_'read0'),_1) -> ('α',_(4,_'read0'),_1) x\r\n",
"('T',_(4,_'read0'),_1) -> ('B',_(4,_'read0'),_1) x\r\n",
"('t',_(4,_'read0'),_1) -> ('β',_(4,_'read0'),_1) x\r\n",
"('D',_(4,_'write0',_'move-2'),_0) -> x ('A',_(4,_'write0',_'move-2'),_0) x\r\n",
"('d',_(4,_'write0',_'move-2'),_0) -> ('α',_(4,_'write0',_'move-2'),_0) x\r\n",
"('T',_(4,_'write0',_'move-2'),_0) -> ('B',_(4,_'write0',_'move-2'),_0) x\r\n",
"('t',_(4,_'write0',_'move-2'),_0) -> ('β',_(4,_'write0',_'move-2'),_0) x\r\n",
"('D',_(4,_'move-1'),_0) -> x ('A',_(4,_'move-1'),_0) x\r\n",
"('d',_(4,_'move-1'),_0) -> ('α',_(4,_'move-1'),_0) x\r\n",
"('T',_(4,_'move-1'),_0) -> ('B',_(4,_'move-1'),_0) x\r\n",
"('t',_(4,_'move-1'),_0) -> ('β',_(4,_'move-1'),_0) x\r\n",
"('D',_(4,_'move-1'),_1) -> ('A',_(4,_'move-1'),_1) x\r\n",
"('d',_(4,_'move-1'),_1) -> ('α',_(4,_'move-1'),_1) x\r\n",
"('T',_(4,_'move-1'),_1) -> ('B',_(4,_'move-1'),_1) x\r\n",
"('t',_(4,_'move-1'),_1) -> ('β',_(4,_'move-1'),_1) x\r\n",
"('A',_4,_1) -> ('C',_4,_1) x ('c',_4,_1) x\r\n",
"('α',_4,_1) -> ('c',_4,_1) x ('c',_4,_1) x\r\n",
"('B',_4,_1) -> ('S',_4,_1)\r\n",
"('β',_4,_1) -> ('s',_4,_1)\r\n",
"('C',_4,_1) -> ('D',_(4,_'read1'),_1) ('D',_(4,_'read1'),_0)\r\n",
"('c',_4,_1) -> ('d',_(4,_'read1'),_1) ('d',_(4,_'read1'),_0)\r\n",
"('S',_4,_1) -> ('T',_(4,_'read1'),_1) ('T',_(4,_'read1'),_0)\r\n",
"('s',_4,_1) -> ('t',_(4,_'read1'),_1) ('t',_(4,_'read1'),_0)\r\n",
"('D',_4,_1) -> ('A',_4,_1) x\r\n",
"('d',_4,_1) -> ('α',_4,_1) x\r\n",
"('T',_4,_1) -> ('B',_4,_1) x\r\n",
"('t',_4,_1) -> ('β',_4,_1) x\r\n",
"('D',_(4,_'read1'),_0) -> x ('A',_(4,_'read1'),_0) x\r\n",
"('d',_(4,_'read1'),_0) -> ('α',_(4,_'read1'),_0) x\r\n",
"('T',_(4,_'read1'),_0) -> ('B',_(4,_'read1'),_0) x\r\n",
"('t',_(4,_'read1'),_0) -> ('β',_(4,_'read1'),_0) x\r\n",
"('D',_(4,_'write1',_'move-2'),_1) -> ('A',_(4,_'write1',_'move-2'),_1) x\r\n",
"('d',_(4,_'write1',_'move-2'),_1) -> ('α',_(4,_'write1',_'move-2'),_1) x\r\n",
"('T',_(4,_'write1',_'move-2'),_1) -> ('B',_(4,_'write1',_'move-2'),_1) x\r\n",
"('t',_(4,_'write1',_'move-2'),_1) -> ('β',_(4,_'write1',_'move-2'),_1) x\r\n",
"(\"S'\",_0,_1) -> ('B',_0,_1) x\r\n",
"(\"s'\",_0,_1) -> ('β',_0,_1) x\r\n",
"('A',_(0,_'read1'),_0) -> ('C',_(0,_'read1'),_0)\r\n",
"('α',_(0,_'read1'),_0) -> ('c',_(0,_'read1'),_0)\r\n",
"('B',_(0,_'read1'),_0) -> (\"S'\",_(0,_'write0',_'move+2'),_1) (\"S'\",_(0,_'write0',_'move+2'),_0)\r\n",
"('β',_(0,_'read1'),_0) -> (\"s'\",_(0,_'write0',_'move+2'),_1) (\"s'\",_(0,_'write0',_'move+2'),_0) (\"s'\",_(0,_'write0',_'move+2'),_1) (\"s'\",_(0,_'write0',_'move+2'),_0)\r\n",
"('C',_(0,_'read1'),_0) -> ('A',_(0,_'write0',_'move+2'),_1) ('A',_(0,_'write0',_'move+2'),_0)\r\n",
"('c',_(0,_'read1'),_0) -> ('α',_(0,_'write0',_'move+2'),_1) ('α',_(0,_'write0',_'move+2'),_0)\r\n",
"(\"S'\",_(0,_'read1'),_0) -> x ('B',_(0,_'read1'),_0) x\r\n",
"(\"s'\",_(0,_'read1'),_0) -> ('β',_(0,_'read1'),_0) x\r\n",
"(\"S'\",_(0,_'write0',_'move+2'),_1) -> ('B',_(0,_'write0',_'move+2'),_1) x\r\n",
"(\"s'\",_(0,_'write0',_'move+2'),_1) -> ('β',_(0,_'write0',_'move+2'),_1) x\r\n",
"(\"S'\",_(0,_'move+1'),_0) -> x ('B',_(0,_'move+1'),_0) x\r\n",
"(\"s'\",_(0,_'move+1'),_0) -> ('β',_(0,_'move+1'),_0) x\r\n",
"(\"S'\",_1,_0) -> x ('B',_1,_0) x\r\n",
"(\"s'\",_1,_0) -> ('β',_1,_0) x\r\n",
"(\"S'\",_(1,_'read0'),_0) -> x ('B',_(1,_'read0'),_0) x\r\n",
"(\"s'\",_(1,_'read0'),_0) -> ('β',_(1,_'read0'),_0) x\r\n",
"(\"S'\",_(1,_'read0'),_1) -> ('B',_(1,_'read0'),_1) x\r\n",
"(\"s'\",_(1,_'read0'),_1) -> ('β',_(1,_'read0'),_1) x\r\n",
"(\"S'\",_1,_1) -> ('B',_1,_1) x\r\n",
"(\"s'\",_1,_1) -> ('β',_1,_1) x\r\n",
"('A',_(1,_'read1'),_0) -> ('C',_(1,_'read1'),_0)\r\n",
"('α',_(1,_'read1'),_0) -> ('c',_(1,_'read1'),_0)\r\n",
"('B',_(1,_'read1'),_0) -> (\"S'\",_(1,_'write0',_'move+2'),_1) (\"S'\",_(1,_'write0',_'move+2'),_0) (\"s'\",_(1,_'write0',_'move+2'),_1) (\"s'\",_(1,_'write0',_'move+2'),_0)\r\n",
"('β',_(1,_'read1'),_0) -> (\"s'\",_(1,_'write0',_'move+2'),_1) (\"s'\",_(1,_'write0',_'move+2'),_0) (\"s'\",_(1,_'write0',_'move+2'),_1) (\"s'\",_(1,_'write0',_'move+2'),_0)\r\n",
"('C',_(1,_'read1'),_0) -> ('A',_(1,_'write0',_'move+2'),_1) ('A',_(1,_'write0',_'move+2'),_0)\r\n",
"('c',_(1,_'read1'),_0) -> ('α',_(1,_'write0',_'move+2'),_1) ('α',_(1,_'write0',_'move+2'),_0)\r\n",
"(\"S'\",_(1,_'read1'),_0) -> x ('B',_(1,_'read1'),_0) x\r\n",
"(\"s'\",_(1,_'read1'),_0) -> ('β',_(1,_'read1'),_0) x\r\n",
"(\"S'\",_(1,_'write0',_'move+2'),_1) -> ('B',_(1,_'write0',_'move+2'),_1) x\r\n",
"(\"s'\",_(1,_'write0',_'move+2'),_1) -> ('β',_(1,_'write0',_'move+2'),_1) x\r\n",
"(\"S'\",_(1,_'move+1'),_1) -> ('B',_(1,_'move+1'),_1) x\r\n",
"(\"s'\",_(1,_'move+1'),_1) -> ('β',_(1,_'move+1'),_1) x\r\n",
"(\"S'\",_2,_0) -> x ('B',_2,_0) x\r\n",
"(\"s'\",_2,_0) -> ('β',_2,_0) x\r\n",
"('A',_(2,_'read0'),_0) -> ('C',_(2,_'read0'),_0)\r\n",
"('α',_(2,_'read0'),_0) -> ('c',_(2,_'read0'),_0)\r\n",
"('B',_(2,_'read0'),_0) -> (\"S'\",_(2,_'write0',_'move-2'),_1) (\"S'\",_(2,_'write0',_'move-2'),_0)\r\n",
"('β',_(2,_'read0'),_0) -> (\"s'\",_(2,_'write0',_'move-2'),_1) (\"s'\",_(2,_'write0',_'move-2'),_0) (\"s'\",_(2,_'write0',_'move-2'),_1) (\"s'\",_(2,_'write0',_'move-2'),_0)\r\n",
"('C',_(2,_'read0'),_0) -> ('A',_(2,_'write0',_'move-2'),_1) ('A',_(2,_'write0',_'move-2'),_0)\r\n",
"('c',_(2,_'read0'),_0) -> ('α',_(2,_'write0',_'move-2'),_1) ('α',_(2,_'write0',_'move-2'),_0)\r\n",
"(\"S'\",_(2,_'read0'),_0) -> x ('B',_(2,_'read0'),_0) x\r\n",
"(\"s'\",_(2,_'read0'),_0) -> ('β',_(2,_'read0'),_0) x\r\n",
"('A',_(2,_'write0',_'move-2'),_0) -> ('C',_(2,_'write0',_'move-2'),_0)\r\n",
"('α',_(2,_'write0',_'move-2'),_0) -> ('c',_(2,_'write0',_'move-2'),_0)\r\n",
"('B',_(2,_'write0',_'move-2'),_0) -> (\"S'\",_(2,_'move-1'),_1) (\"S'\",_(2,_'move-1'),_0)\r\n",
"('β',_(2,_'write0',_'move-2'),_0) -> (\"s'\",_(2,_'move-1'),_1) (\"s'\",_(2,_'move-1'),_0) (\"s'\",_(2,_'move-1'),_1) (\"s'\",_(2,_'move-1'),_0)\r\n",
"('C',_(2,_'write0',_'move-2'),_0) -> ('A',_(2,_'move-1'),_1) ('A',_(2,_'move-1'),_0)\r\n",
"('c',_(2,_'write0',_'move-2'),_0) -> ('α',_(2,_'move-1'),_1) ('α',_(2,_'move-1'),_0)\r\n",
"(\"S'\",_(2,_'write0',_'move-2'),_0) -> x ('B',_(2,_'write0',_'move-2'),_0) x\r\n",
"(\"s'\",_(2,_'write0',_'move-2'),_0) -> ('β',_(2,_'write0',_'move-2'),_0) x\r\n",
"('A',_(2,_'move-1'),_0) -> ('C',_(2,_'move-1'),_0)\r\n",
"('α',_(2,_'move-1'),_0) -> ('c',_(2,_'move-1'),_0)\r\n",
"('B',_(2,_'move-1'),_0) -> (\"S'\",_4,_1) (\"S'\",_4,_0)\r\n",
"('β',_(2,_'move-1'),_0) -> (\"s'\",_4,_1) (\"s'\",_4,_0) (\"s'\",_4,_1) (\"s'\",_4,_0)\r\n",
"('C',_(2,_'move-1'),_0) -> ('A',_4,_1) ('A',_4,_0)\r\n",
"('c',_(2,_'move-1'),_0) -> ('α',_4,_1) ('α',_4,_0)\r\n",
"(\"S'\",_(2,_'move-1'),_0) -> x ('B',_(2,_'move-1'),_0) x\r\n",
"(\"s'\",_(2,_'move-1'),_0) -> ('β',_(2,_'move-1'),_0) x\r\n",
"('A',_(2,_'move-1'),_1) -> ('C',_(2,_'move-1'),_1)\r\n",
"('α',_(2,_'move-1'),_1) -> ('c',_(2,_'move-1'),_1)\r\n",
"('B',_(2,_'move-1'),_1) -> (\"S'\",_4,_1) (\"S'\",_4,_0) (\"s'\",_4,_1) (\"s'\",_4,_0)\r\n",
"('β',_(2,_'move-1'),_1) -> (\"s'\",_4,_1) (\"s'\",_4,_0) (\"s'\",_4,_1) (\"s'\",_4,_0)\r\n",
"('C',_(2,_'move-1'),_1) -> ('A',_4,_1) ('A',_4,_0)\r\n",
"('c',_(2,_'move-1'),_1) -> ('α',_4,_1) ('α',_4,_0)\r\n",
"(\"S'\",_(2,_'move-1'),_1) -> ('B',_(2,_'move-1'),_1) x\r\n",
"(\"s'\",_(2,_'move-1'),_1) -> ('β',_(2,_'move-1'),_1) x\r\n",
"(\"S'\",_(2,_'read0'),_1) -> ('B',_(2,_'read0'),_1) x\r\n",
"(\"s'\",_(2,_'read0'),_1) -> ('β',_(2,_'read0'),_1) x\r\n",
"(\"S'\",_2,_1) -> ('B',_2,_1) x\r\n",
"(\"s'\",_2,_1) -> ('β',_2,_1) x\r\n",
"(\"S'\",_(2,_'read1'),_0) -> x ('B',_(2,_'read1'),_0) x\r\n",
"(\"s'\",_(2,_'read1'),_0) -> ('β',_(2,_'read1'),_0) x\r\n",
"(\"S'\",_3,_0) -> x ('B',_3,_0) x\r\n",
"(\"s'\",_3,_0) -> ('β',_3,_0) x\r\n",
"(\"S'\",_(3,_'read0'),_1) -> ('B',_(3,_'read0'),_1) x\r\n",
"(\"s'\",_(3,_'read0'),_1) -> ('β',_(3,_'read0'),_1) x\r\n",
"(\"S'\",_3,_1) -> ('B',_3,_1) x\r\n",
"(\"s'\",_3,_1) -> ('β',_3,_1) x\r\n",
"('A',_(3,_'read1'),_0) -> ('C',_(3,_'read1'),_0)\r\n",
"('α',_(3,_'read1'),_0) -> ('c',_(3,_'read1'),_0)\r\n",
"('B',_(3,_'read1'),_0) -> (\"S'\",_(3,_'write0',_'move+2'),_1) (\"S'\",_(3,_'write0',_'move+2'),_0) (\"s'\",_(3,_'write0',_'move+2'),_1) (\"s'\",_(3,_'write0',_'move+2'),_0)\r\n",
"('β',_(3,_'read1'),_0) -> (\"s'\",_(3,_'write0',_'move+2'),_1) (\"s'\",_(3,_'write0',_'move+2'),_0) (\"s'\",_(3,_'write0',_'move+2'),_1) (\"s'\",_(3,_'write0',_'move+2'),_0)\r\n",
"('C',_(3,_'read1'),_0) -> ('A',_(3,_'write0',_'move+2'),_1) ('A',_(3,_'write0',_'move+2'),_0)\r\n",
"('c',_(3,_'read1'),_0) -> ('α',_(3,_'write0',_'move+2'),_1) ('α',_(3,_'write0',_'move+2'),_0)\r\n",
"(\"S'\",_(3,_'read1'),_0) -> x ('B',_(3,_'read1'),_0) x\r\n",
"(\"s'\",_(3,_'read1'),_0) -> ('β',_(3,_'read1'),_0) x\r\n",
"(\"S'\",_(3,_'write0',_'move+2'),_1) -> ('B',_(3,_'write0',_'move+2'),_1) x\r\n",
"(\"s'\",_(3,_'write0',_'move+2'),_1) -> ('β',_(3,_'write0',_'move+2'),_1) x\r\n",
"(\"S'\",_(3,_'move+1'),_1) -> ('B',_(3,_'move+1'),_1) x\r\n",
"(\"s'\",_(3,_'move+1'),_1) -> ('β',_(3,_'move+1'),_1) x\r\n",
"(\"S'\",_4,_0) -> x ('B',_4,_0) x\r\n",
"(\"s'\",_4,_0) -> ('β',_4,_0) x\r\n",
"(\"S'\",_(4,_'read0'),_0) -> x ('B',_(4,_'read0'),_0) x\r\n",
"(\"s'\",_(4,_'read0'),_0) -> ('β',_(4,_'read0'),_0) x\r\n",
"('A',_(4,_'read0'),_1) -> ('C',_(4,_'read0'),_1)\r\n",
"('α',_(4,_'read0'),_1) -> ('c',_(4,_'read0'),_1)\r\n",
"('B',_(4,_'read0'),_1) -> (\"S'\",_(4,_'write0',_'move-2'),_1) (\"S'\",_(4,_'write0',_'move-2'),_0) (\"s'\",_(4,_'write0',_'move-2'),_1) (\"s'\",_(4,_'write0',_'move-2'),_0)\r\n",
"('β',_(4,_'read0'),_1) -> (\"s'\",_(4,_'write0',_'move-2'),_1) (\"s'\",_(4,_'write0',_'move-2'),_0) (\"s'\",_(4,_'write0',_'move-2'),_1) (\"s'\",_(4,_'write0',_'move-2'),_0)\r\n",
"('C',_(4,_'read0'),_1) -> ('A',_(4,_'write0',_'move-2'),_1) ('A',_(4,_'write0',_'move-2'),_0)\r\n",
"('c',_(4,_'read0'),_1) -> ('α',_(4,_'write0',_'move-2'),_1) ('α',_(4,_'write0',_'move-2'),_0)\r\n",
"(\"S'\",_(4,_'read0'),_1) -> ('B',_(4,_'read0'),_1) x\r\n",
"(\"s'\",_(4,_'read0'),_1) -> ('β',_(4,_'read0'),_1) x\r\n",
"('A',_(4,_'write0',_'move-2'),_0) -> ('C',_(4,_'write0',_'move-2'),_0)\r\n",
"('α',_(4,_'write0',_'move-2'),_0) -> ('c',_(4,_'write0',_'move-2'),_0)\r\n",
"('B',_(4,_'write0',_'move-2'),_0) -> (\"S'\",_(4,_'move-1'),_1) (\"S'\",_(4,_'move-1'),_0)\r\n",
"('β',_(4,_'write0',_'move-2'),_0) -> (\"s'\",_(4,_'move-1'),_1) (\"s'\",_(4,_'move-1'),_0) (\"s'\",_(4,_'move-1'),_1) (\"s'\",_(4,_'move-1'),_0)\r\n",
"('C',_(4,_'write0',_'move-2'),_0) -> ('A',_(4,_'move-1'),_1) ('A',_(4,_'move-1'),_0)\r\n",
"('c',_(4,_'write0',_'move-2'),_0) -> ('α',_(4,_'move-1'),_1) ('α',_(4,_'move-1'),_0)\r\n",
"(\"S'\",_(4,_'write0',_'move-2'),_0) -> x ('B',_(4,_'write0',_'move-2'),_0) x\r\n",
"(\"s'\",_(4,_'write0',_'move-2'),_0) -> ('β',_(4,_'write0',_'move-2'),_0) x\r\n",
"('A',_(4,_'move-1'),_0) -> ('C',_(4,_'move-1'),_0)\r\n",
"('α',_(4,_'move-1'),_0) -> ('c',_(4,_'move-1'),_0)\r\n",
"('B',_(4,_'move-1'),_0) -> (\"S'\",_4,_1) (\"S'\",_4,_0)\r\n",
"('β',_(4,_'move-1'),_0) -> (\"s'\",_4,_1) (\"s'\",_4,_0) (\"s'\",_4,_1) (\"s'\",_4,_0)\r\n",
"('C',_(4,_'move-1'),_0) -> ('A',_4,_1) ('A',_4,_0)\r\n",
"('c',_(4,_'move-1'),_0) -> ('α',_4,_1) ('α',_4,_0)\r\n",
"(\"S'\",_(4,_'move-1'),_0) -> x ('B',_(4,_'move-1'),_0) x\r\n",
"(\"s'\",_(4,_'move-1'),_0) -> ('β',_(4,_'move-1'),_0) x\r\n",
"('A',_(4,_'move-1'),_1) -> ('C',_(4,_'move-1'),_1)\r\n",
"('α',_(4,_'move-1'),_1) -> ('c',_(4,_'move-1'),_1)\r\n",
"('B',_(4,_'move-1'),_1) -> (\"S'\",_4,_1) (\"S'\",_4,_0) (\"s'\",_4,_1) (\"s'\",_4,_0)\r\n",
"('β',_(4,_'move-1'),_1) -> (\"s'\",_4,_1) (\"s'\",_4,_0) (\"s'\",_4,_1) (\"s'\",_4,_0)\r\n",
"('C',_(4,_'move-1'),_1) -> ('A',_4,_1) ('A',_4,_0)\r\n",
"('c',_(4,_'move-1'),_1) -> ('α',_4,_1) ('α',_4,_0)\r\n",
"(\"S'\",_(4,_'move-1'),_1) -> ('B',_(4,_'move-1'),_1) x\r\n",
"(\"s'\",_(4,_'move-1'),_1) -> ('β',_(4,_'move-1'),_1) x\r\n",
"(\"S'\",_4,_1) -> ('B',_4,_1) x\r\n",
"(\"s'\",_4,_1) -> ('β',_4,_1) x\r\n",
"('A',_(4,_'read1'),_0) -> ('C',_(4,_'read1'),_0)\r\n",
"('α',_(4,_'read1'),_0) -> ('c',_(4,_'read1'),_0)\r\n",
"('B',_(4,_'read1'),_0) -> (\"S'\",_(4,_'write1',_'move-2'),_1) (\"S'\",_(4,_'write1',_'move-2'),_0)\r\n",
"('β',_(4,_'read1'),_0) -> (\"s'\",_(4,_'write1',_'move-2'),_1) (\"s'\",_(4,_'write1',_'move-2'),_0) (\"s'\",_(4,_'write1',_'move-2'),_1) (\"s'\",_(4,_'write1',_'move-2'),_0)\r\n",
"('C',_(4,_'read1'),_0) -> ('A',_(4,_'write1',_'move-2'),_1) ('A',_(4,_'write1',_'move-2'),_0)\r\n",
"('c',_(4,_'read1'),_0) -> ('α',_(4,_'write1',_'move-2'),_1) ('α',_(4,_'write1',_'move-2'),_0)\r\n",
"(\"S'\",_(4,_'read1'),_0) -> x ('B',_(4,_'read1'),_0) x\r\n",
"(\"s'\",_(4,_'read1'),_0) -> ('β',_(4,_'read1'),_0) x\r\n",
"('A',_(4,_'write1',_'move-2'),_1) -> ('C',_(4,_'write1',_'move-2'),_1)\r\n",
"('α',_(4,_'write1',_'move-2'),_1) -> ('c',_(4,_'write1',_'move-2'),_1)\r\n",
"('B',_(4,_'write1',_'move-2'),_1) -> (\"S'\",_(4,_'move-1'),_1) (\"S'\",_(4,_'move-1'),_0) (\"s'\",_(4,_'move-1'),_1) (\"s'\",_(4,_'move-1'),_0)\r\n",
"('β',_(4,_'write1',_'move-2'),_1) -> (\"s'\",_(4,_'move-1'),_1) (\"s'\",_(4,_'move-1'),_0) (\"s'\",_(4,_'move-1'),_1) (\"s'\",_(4,_'move-1'),_0)\r\n",
"('C',_(4,_'write1',_'move-2'),_1) -> ('A',_(4,_'move-1'),_1) ('A',_(4,_'move-1'),_0)\r\n",
"('c',_(4,_'write1',_'move-2'),_1) -> ('α',_(4,_'move-1'),_1) ('α',_(4,_'move-1'),_0)\r\n",
"(\"S'\",_(4,_'write1',_'move-2'),_1) -> ('B',_(4,_'write1',_'move-2'),_1) x\r\n",
"(\"s'\",_(4,_'write1',_'move-2'),_1) -> ('β',_(4,_'write1',_'move-2'),_1) x\r\n"
]
}
],
"source": [
"%cat tm-m2.tag"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This 2-tag system, together with the input string $\\texttt{0}$, are encoded into a string with 6.5 million symbols. Running the UTM is very slow. I had to write a special simulator that enables it to \"fast-forward\" in certain cases, and found that it accepts after **46 trillion moves**."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"### The real numbers are uncountable\n",
"\n",
"Now we shift for the moment to a totally different topic, the uncountability of the real numbers. The concept of an uncountable infinity, and the associated proof technique of diagonalization, was discovered by Georg Cantor. Unfortunately, it also drove him crazy.\n",
"\n",
"\n",
"
Read subsection \"The Diagonalization Method,\" from page 202 to the table at the top of page 206.
\n",
"
Watch W9E2: Diagonalization.
\n",
"
\n",
"
Read: If the above isn't clear, try the book's proof on pages 207–209.
\n",
"
\n",
"
Read the subsection \"A Turing-Unrecognizable Language.\"
\n",
"
\n",
"
Read pages 215–217, up to \"via the diagonalization method.\"
\n",
"