Nuprl Lemma : mu_ex_v5_Token-ilf

[initial_token,m1,m2,proc1,proc2:Id]. [es:EO']. [e:E]. [i:Id]. [u:Unit].
  (<i, make-Msg([token];Unit;u)>  mu_ex_v5_main(initial_token;m1;m2;proc1;proc2)(e)
   ((loc(e) = proc1)  (loc(e) = proc2))
       (u = )
       (i = (mu_ex_v5_getOtherProc(proc1;proc2) loc(e)))
       (((b:
             ((b1:
                ((b1)
                 (b2:. <b, b1, b2>  Prior(mu_ex_v5_State(initial_token))?mu_ex_v5_initState(initial_token)(e))))
              (b)))
             Base([request];Unit)(e))
           ((b,b1:
               ((b2:
                  (<b, b1, b2>  Prior(mu_ex_v5_State(initial_token))?mu_ex_v5_initState(initial_token)(e)  (b2)))
                (b1)))
               Base(``leave cs``;Unit)(e))))


Proof not projected

Error : references
\mforall{}[initial$_{token}$,m1,m2,proc1,proc2:Id].  \mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[i:Id].  \mforall{}[u:Unit]\000C.
    (<i,  make-Msg([token];Unit;u)>  \mmember{}  mu\_ex\_v5\_main(initial$_{token}$;m1;m2;proc1;p\000Croc2)(e)
    \mLeftarrow{}{}\mRightarrow{}  ((loc(e)  =  proc1)  \mdownarrow{}\mvee{}  (loc(e)  =  proc2))
            \mwedge{}  (u  =  \mcdot{})
            \mwedge{}  (i  =  (mu\_ex\_v5\_getOtherProc(proc1;proc2)  loc(e)))
            \mwedge{}  (\mdownarrow{}((\mexists{}b:\mBbbB{}
                          ((\mexists{}b1:\mBbbB{}
                                ((\muparrow{}b1)
                                \mwedge{}  (\mexists{}b2:\mBbbB{}
                                        <b,  b1,  b2>  \mmember{}
                                          Prior(mu\_ex\_v5\_State(initial$_{token}$))?mu\_ex\_v5\_initState\000C(initial$_{token}$)(e))))
                          \mwedge{}  (\mneg{}\muparrow{}b)))
                    \mwedge{}  \mcdot{}  \mmember{}  Base([request];Unit)(e))
                    \mvee{}  ((\mexists{}b,b1:\mBbbB{}
                              ((\mexists{}b2:\mBbbB{}
                                    (<b,  b1,  b2>  \mmember{}
                                        Prior(mu\_ex\_v5\_State(initial$_{token}$))?mu\_ex\_v5\_initState(\000Cinitial$_{token}$)(e)
                                    \mwedge{}  (\muparrow{}b2)))
                              \mwedge{}  (\muparrow{}b1)))
                        \mwedge{}  \mcdot{}  \mmember{}  Base(``leave  cs``;Unit)(e))))


Date html generated: 2012_02_20-PM-07_51_12
Last ObjectModification: 2012_02_02-PM-03_00_53

Home Index