Changes

Line 2,464: Line 2,464:  
==Note 31==
 
==Note 31==
   −
<pre>
+
===Interpretation of the Propositional Program (cont.)===
Interpretation of the Propositional Program (cont.)
     −
Transition Relations:
+
'''Transition Relations'''
   −
  ( p0_q0  p0_r1  p0_r1_s0  ( p1_q0  p1_r2  p1_r1_s0 ))
+
{| align="center" cellpadding="8" width="90%"
  ( p0_q0  p0_r1  p0_r1_s1  ( p1_q1  p1_r2  p1_r1_s1 ))
+
|
  ( p0_q0  p0_r1  p0_r1_s# ( p1_q# p1_r0  p1_r1_s# ))
+
<math>\begin{array}{l}
  ( p0_q0  p0_r2  p0_r2_s# ( p1_q# p1_r1  p1_r2_s# ))
+
\texttt{(~p0\_q0~~p0\_r1~~p0\_r1\_s0~~(~p1\_q0~~p1\_r2~~p1\_r1\_s0~))}
 +
\\
 +
\texttt{(~p0\_q0~~p0\_r1~~p0\_r1\_s1~~(~p1\_q1~~p1\_r2~~p1\_r1\_s1~))}
 +
\\
 +
\texttt{(~p0\_q0~~p0\_r1~~p0\_r1\_s\#~~(~p1\_q\#~~p1\_r0~~p1\_r1\_s\#~))}
 +
\\
 +
\texttt{(~p0\_q0~~p0\_r2~~p0\_r2\_s\#~~(~p1\_q\#~~p1\_r1~~p1\_r2\_s\#~))}
 +
\\ \\
 +
\texttt{(~p0\_q1~~p0\_r1~~p0\_r1\_s0~~(~p1\_q1~~p1\_r2~~p1\_r1\_s0~))}
 +
\\
 +
\texttt{(~p0\_q1~~p0\_r1~~p0\_r1\_s1~~(~p1\_q0~~p1\_r2~~p1\_r1\_s1~))}
 +
\\
 +
\texttt{(~p0\_q1~~p0\_r1~~p0\_r1\_s\#~~(~p1\_q*~~p1\_r0~~p1\_r1\_s\#~))}
 +
\\
 +
\texttt{(~p0\_q1~~p0\_r2~~p0\_r2\_s\#~~(~p1\_q*~~p1\_r1~~p1\_r2\_s\#~))}
 +
\\ \\
 +
\texttt{(~p1\_q0~~p1\_r1~~p1\_r1\_s0~~(~p2\_q0~~p2\_r2~~p2\_r1\_s0~))}
 +
\\
 +
\texttt{(~p1\_q0~~p1\_r1~~p1\_r1\_s1~~(~p2\_q1~~p2\_r2~~p2\_r1\_s1~))}
 +
\\
 +
\texttt{(~p1\_q0~~p1\_r1~~p1\_r1\_s\#~~(~p2\_q\#~~p2\_r0~~p2\_r1\_s\#~))}
 +
\\
 +
\texttt{(~p1\_q0~~p1\_r2~~p1\_r2\_s\#~~(~p2\_q\#~~p2\_r1~~p2\_r2\_s\#~))}
 +
\\ \\
 +
\texttt{(~p1\_q1~~p1\_r1~~p1\_r1\_s0~~(~p2\_q1~~p2\_r2~~p2\_r1\_s0~))}
 +
\\
 +
\texttt{(~p1\_q1~~p1\_r1~~p1\_r1\_s1~~(~p2\_q0~~p2\_r2~~p2\_r1\_s1~))}
 +
\\
 +
\texttt{(~p1\_q1~~p1\_r1~~p1\_r1\_s\#~~(~p2\_q*~~p2\_r0~~p2\_r1\_s\#~))}
 +
\\
 +
\texttt{(~p1\_q1~~p1\_r2~~p1\_r2\_s\#~~(~p2\_q*~~p2\_r1~~p2\_r2\_s\#~))}
 +
\end{array}</math>
 +
|}
   −
  ( p0_q1  p0_r1  p0_r1_s0  ( p1_q1  p1_r2  p1_r1_s0 ))
+
The Transition Relation segment of the propositional program for <math>\operatorname{Stunt}(2)</math> consists of sixteen implication statements with complex antecedents and consequents.  Taken together, these give propositional expression to the TM Figure and Table that were given at the outset.
  ( p0_q1  p0_r1  p0_r1_s1  ( p1_q0  p1_r2  p1_r1_s1 ))
  −
  ( p0_q1  p0_r1  p0_r1_s#  ( p1_q*  p1_r0  p1_r1_s# ))
  −
  ( p0_q1  p0_r2  p0_r2_s#  ( p1_q*  p1_r1  p1_r2_s# ))
  −
 
  −
  ( p1_q0  p1_r1  p1_r1_s0  ( p2_q0  p2_r2  p2_r1_s0 ))
  −
  ( p1_q0  p1_r1  p1_r1_s1  ( p2_q1  p2_r2  p2_r1_s1 ))
  −
  ( p1_q0  p1_r1  p1_r1_s#  ( p2_q#  p2_r0  p2_r1_s# ))
  −
  ( p1_q0  p1_r2  p1_r2_s#  ( p2_q#  p2_r1  p2_r2_s# ))
  −
 
  −
  ( p1_q1  p1_r1  p1_r1_s0  ( p2_q1  p2_r2  p2_r1_s0 ))
  −
  ( p1_q1  p1_r1  p1_r1_s1  ( p2_q0  p2_r2  p2_r1_s1 ))
  −
  ( p1_q1  p1_r1  p1_r1_s#  ( p2_q*  p2_r0  p2_r1_s# ))
  −
  ( p1_q1  p1_r2  p1_r2_s#  ( p2_q*  p2_r1  p2_r2_s# ))
  −
 
  −
The Transition Relation segment of the propositional program
  −
for Stunt(2) consists of sixteen implication statements with
  −
complex antecedents and consequents.  Taken together, these
  −
give propositional expression to the TM Figure and Table
  −
that were given at the outset.
      +
<pre>
 
Just by way of a single example, consider the clause:
 
Just by way of a single example, consider the clause:
  
12,080

edits