Paper/Paper.thy
changeset 135 ba63ba7d282b
parent 134 f47f1ef313d1
child 136 8fa9e018abe4
equal deleted inserted replaced
134:f47f1ef313d1 135:ba63ba7d282b
  1343 
  1343 
  1344   SO the following TM calculates something according to def from chap 8,
  1344   SO the following TM calculates something according to def from chap 8,
  1345   but not with chap 3. For example:
  1345   but not with chap 3. For example:
  1346   
  1346   
  1347   \begin{center}
  1347   \begin{center}
  1348   @{term "[(L, 0), (L, 2), (R, 2), (R, 0)]"}
  1348   @{term "[(L, (0::nat)), (L, 2), (R, 2), (R, 0)]"}
  1349   \end{center}
  1349   \end{center}
  1350 
  1350 
  1351   If started with @{term "([], [Oc])"} it halts with the
  1351   If started with @{term "([], [Oc])"} it halts with the
  1352   non-standard tape @{term "([Oc], [])"} according to the definition in Chap 3;
  1352   non-standard tape @{term "([Oc], [])"} according to the definition in Chap 3;
  1353   but with @{term "([], [Oc])"} according to def Chap 8
  1353   but with @{term "([], [Oc])"} according to def Chap 8