12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)
Revision as of 17:45, 27 April 2013
, 17:45, 27 April 2013→Additional evaluation rules: add figures
===Additional evaluation rules===
===Additional evaluation rules===
Three immediate corollaries of the fundamental evaluation rule are listed below for future reference.
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
<pre>
o-----------------------------------------------------------o
| Emptiness Rule |
o-----------------------------------------------------------o
| |
| o o---o o-o-o |
| | \ / \ / |
| @ = @ = @ = ... |
| |
o-----------------------------------------------------------o
</pre>
| (23a)
|}
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
<pre>
o-----------------------------------------------------------o
| Indistinctness Rule |
o-----------------------------------------------------------o
| |
| a a a a a |
| o o---o o-o-o |
| | \ / \ / |
| @ = @ = @ = ... |
| |
o-----------------------------------------------------------o
</pre>
| (23b)
|}
{| align="center" cellpadding="8" style="text-align:center; width:90%"
|
<pre>
o-----------------------------------------------------------o
| Evaluation Rule |
o-----------------------------------------------------------o
| |
| o |
| | x_2 ... x_k |
| o---o-...-o---o |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / x_2 ... x_k |
| @ = @ |
| |
o-----------------------------------------------------------o
| |
| ((), x_2, ..., x_k) = x_2 ... x_k |
| |
o-----------------------------------------------------------o
| Setup <---- | ----> Spike |
o-----------------------------------------------------------o
</pre>
| (23c)
|}
==Case analysis-synthesis theorem==
==Case analysis-synthesis theorem==