Adding two binary numbers 

> ## Turing machine for adding two numbers in binary format
## Assume that the two inputs have the same length
Q:={q0,q1,q2,q3,qf,
   qn,qn0,qn0L,qn00,qn01,qn1,qn1L,qn10,qn11,qnp,qnp1,qnp2,
   qc,qc0,qc0L,qc00,qc01,qc1,qc1L,qc10,qc11,qcp,qcp1,qcp2,
   qcp3}:
Sig:={0,1,"#",a,b}:
Gam:={0,1,"#",a,b,\Delta}:
F:={qf}:
delta:=table():
delta[(q0,0)]:=[q1,0,'L']:
delta[(q0,1)]:=[q1,1,'L']:
delta[(q1,\Delta)]:=[q2,"#",'R']:
delta[(q2,0)]:=[q2,0,'R']:
delta[(q2,1)]:=[q2,1,'R']:
delta[(q2,a)]:=[q2,a,'R']:
delta[(q2,b)]:=[q2,b,'R']:
delta[(q2,"#")]:=[q2,"#",'R']:
delta[(q2,\Delta)]:=[qn,\Delta,'L']: ## No carry bit
delta[(qn,a)]:=[qn,a,'L']:
delta[(qn,b)]:=[qn,b,'L']:
delta[(qn,0)]:=[qn0,a,'L']: ## Looking for the next number
delta[(qn,1)]:=[qn1,b,'L']:
delta[(qn,"#")]:=[qnp,"#",'R']: # Ready for cleaning-up
delta[(qn0,0)]:=[qn0,0,'L']:
delta[(qn0,1)]:=[qn0,1,'L']:
delta[(qn0,"#")]:=[qn0L,"#",'L']: #Ready to take the 2nd
delta[(qn0L,a)]:=[qn0L,a,'L']:
delta[(qn0L,b)]:=[qn0L,b,'L']:
delta[(qn0L,0)]:=[qn00,a,'L']:
delta[(qn0L,1)]:=[qn01,b,'L']:

delta[(qn00,0)]:=[qn00,0,'L']:
delta[(qn00,1)]:=[qn00,1,'L']:
delta[(qn00,"#")]:=[qn00,"#",'L']: ## Ready to write
delta[(qn00,\Delta)]:=[q2,0,'R']:

delta[(qn01,0)]:=[qn01,0,'L']:
delta[(qn01,1)]:=[qn01,1,'L']:
delta[(qn01,"#")]:=[qn01,"#",'L']: ## Ready to write
delta[(qn01,\Delta)]:=[q2,1,'R']:

delta[(qn1,0)]:=[qn1,0,'L']:
delta[(qn1,1)]:=[qn1,1,'L']:
delta[(qn1,"#")]:=[qn1L,"#",'L']: # Ready to take the 2nd
delta[(qn1L,a)]:=[qn1L,a,'L']:
delta[(qn1L,b)]:=[qn1L,b,'L']:
delta[(qn1L,0)]:=[qn10,a,'L']:
delta[(qn1L,1)]:=[qn11,b,'L']:

delta[(qn10,0)]:=[qn10,0,'L']:
delta[(qn10,1)]:=[qn10,1,'L']:
delta[(qn10,"#")]:=[qn10,"#",'L']: ## Ready to write
delta[(qn10,\Delta)]:=[q2,1,'R']:  ## No carry bit

delta[(qn11,0)]:=[qn11,0,'L']:
delta[(qn11,1)]:=[qn11,1,'L']:
delta[(qn11,"#")]:=[qn11,"#",'L']: ## Ready to write
delta[(qn11,\Delta)]:=[q3,0,'R']:  ## With carry bit

delta[(q3,0)]:=[q3,0,'R']:
delta[(q3,1)]:=[q3,1,'R']:
delta[(q3,a)]:=[q3,a,'R']:
delta[(q3,b)]:=[q3,b,'R']:
delta[(q3,"#")]:=[q3,"#",'R']:
delta[(q3,\Delta)]:=[qc,\Delta,'L']: ## With carry bit
delta[(qc,a)]:=[qc,a,'L']:
delta[(qc,b)]:=[qc,b,'L']:
delta[(qc,0)]:=[qc0,a,'L']: ## Looking for the next number
delta[(qc,1)]:=[qc1,b,'L']:
delta[(qc,"#")]:=[qcp,"#",'R']: # Ready for cleaning-up

delta[(qc0,0)]:=[qc0,0,'L']:
delta[(qc0,1)]:=[qc0,1,'L']:
delta[(qc0,"#")]:=[qc0L,"#",'L']: # Ready to take the 2nd
delta[(qc0L,a)]:=[qc0L,a,'L']:
delta[(qc0L,b)]:=[qc0L,b,'L']:
delta[(qc0L,0)]:=[qc00,a,'L']:
delta[(qc0L,1)]:=[qc01,b,'L']:

delta[(qc00,0)]:=[qc00,0,'L']:
delta[(qc00,1)]:=[qc00,1,'L']:
delta[(qc00,"#")]:=[qc00,"#",'L']: ## Ready to write
delta[(qc00,\Delta)]:=[q2,1,'R']:  ## No carry bit

delta[(qc01,0)]:=[qc01,0,'L']:
delta[(qc01,1)]:=[qc01,1,'L']:
delta[(qc01,"#")]:=[qc01,"#",'L']: ## Ready to write
delta[(qc01,\Delta)]:=[q3,0,'R']:  ## With carry bit

delta[(qc1,0)]:=[qc1,0,'L']:
delta[(qc1,1)]:=[qc1,1,'L']:
delta[(qc1,"#")]:=[qc1L,"#",'L']: # Ready to take the 2nd
delta[(qc1L,a)]:=[qc1L,a,'L']:
delta[(qc1L,b)]:=[qc1L,b,'L']:
delta[(qc1L,0)]:=[qc10,a,'L']:
delta[(qc1L,1)]:=[qc11,b,'L']:

delta[(qc10,0)]:=[qc10,0,'L']:
delta[(qc10,1)]:=[qc10,1,'L']:
delta[(qc10,"#")]:=[qc10,"#",'L']: ## Ready to write
delta[(qc10,\Delta)]:=[q3,0,'R']:  ## With carry bit

delta[(qc11,0)]:=[qc11,0,'L']:
delta[(qc11,1)]:=[qc11,1,'L']:
delta[(qc11,"#")]:=[qc11,"#",'L']: ## Ready to write
delta[(qc11,\Delta)]:=[q3,1,'R']:  ## With carry bit

delta[(qnp,a)]:=[qnp,a,'R']:
delta[(qnp,b)]:=[qnp,b,'R']:
delta[(qnp,\Delta)]:=[qnp1,\Delta,'L']:
delta[(qnp1,a)]:=[qnp1,\Delta,'L']:
delta[(qnp1,b)]:=[qnp1,\Delta,'L']:
delta[(qnp1,"#")]:=[qnp2,\Delta,'L']:
delta[(qnp2,a)]:=[qnp2,\Delta,'L']:
delta[(qnp2,b)]:=[qnp2,\Delta,'L']:
delta[(qnp2,"#")]:=[qf,\Delta,'L']:

delta[(qcp,a)]:=[qcp,a,'R']:
delta[(qcp,b)]:=[qcp,b,'R']:
delta[(qcp,\Delta)]:=[qcp1,\Delta,'L']:
delta[(qcp1,a)]:=[qcp1,\Delta,'L']:  ## a&b at 1st number
delta[(qcp1,b)]:=[qcp1,\Delta,'L']:
delta[(qcp1,"#")]:=[qcp2,\Delta,'L']:## a&b at 2nd number
delta[(qcp2,a)]:=[qcp2,\Delta,'L']:
delta[(qcp2,b)]:=[qcp2,\Delta,'L']:
delta[(qcp2,"#")]:=[qcp3,\Delta,'L']:## 0&1 at 3rd number
delta[(qcp3,0)]:=[qcp3,0,'L']:
delta[(qcp3,1)]:=[qcp3,1,'L']:
delta[(qcp3,\Delta)]:=[qf,1,'S']: ## Add the carry bit
tm2:=mkDTM1T(Q,Sig,Gam,op(delta),q0,\Delta,F,Q minus F);
 

 

`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
`:=`(tm2, DTM1T({q0, qc10, qcp1, qc11, qc00, qc1L, qc01, q1, q2, q3, qcp2, qcp3, qn01, qn1L, qn10, qn11, qnp1, qnp2, qc0L, qn0L, qn, qn0, qn1, qnp, qc0, qc1, qcp, qn00, qc, qf}, {0, 1, a,
> type(tm2,DTM);
 

true (13.1.4.1)  

> transitionGraph(tm2);
 

Plot_2d
 

> stringVerificationDTM(tm2,[1,0,0,"#",1,1,0],`walk`);
 

Accepted (13.1.4.2)
 

> walk;
 

[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
[q0, 1, 0, 0, [q1, Delta, 1, 0, 0, "#", 1, 1, 0] => ["#", q2, 1, 0, 0, "#", 1, 1, 0] => ["#", 1, q2, 0, 0, "#", 1, 1, 0] => ["#", 1, 0, q2, 0, "#", 1, 1, 0] => ["#", 1, 0, 0, q2, "#"..." align="center" border="0">
(13.1.4.3)