<?xml version="1.0"?>
<div>:: <span class="kw">deftheorem </span>   defines <a href="peterson.html#R10" title="PETERSON:pred.10">&lt;&lt;</a> <a onclick="hs(this)" href="javascript:()">PETERSON:def 19 : <br/></a><span> for <font color="Olive" title="b1">Values</font> being   <a href="peterson.html#NM1" title="PETERSON:NM.1">Values_with_Bool</a><br/>  for <font color="Olive" title="b2">DS</font> being   <a href="peterson.html#NM8" title="PETERSON:NM.8">DistributedSysWithSharedMem</a> of <font color="Olive" title="b1">Values</font><br/>  for <font color="Olive" title="b3">e1</font>, <font color="Olive" title="b4">e2</font> being   <a href="peterson.html#NM4" title="PETERSON:NM.4">Event</a> of <font color="Olive" title="b2">DS</font> holds <br/> ( <font color="Olive" title="b3">e1</font> <a href="peterson.html#R10" title="PETERSON:pred.10">&lt;&lt;</a> <font color="Olive" title="b4">e2</font> iff ( <font color="Olive" title="b3">e1</font> <a href="orders_2.html#R3" title="ORDERS_2:pred.3">&lt;=</a> <font color="Olive" title="b4">e2</font> &amp;  not <font color="Olive" title="b4">e2</font> <a href="orders_2.html#R3" title="ORDERS_2:pred.3">&lt;=</a> <font color="Olive" title="b3">e1</font> ) );<br/></span></div>
