Nuprl Lemma : mu_ex_v5_EnterCS-ilf

[initial_token,m1,m2,proc1,proc2:Id]. [es:EO']. [e:E]. [i:Id]. [u:Unit].
  (<i, make-Msg(``enter cs``;Unit;u)>  mu_ex_v5_main(initial_token;m1;m2;proc1;proc2)(e)
   ((loc(e) = proc1)  (loc(e) = proc2))
       (u = )
       (i = (mu_ex_v5_getMachine(m1;m2;proc1) loc(e)))
       (((b:
              ((b1:
                 ((b2:. <b, b1, b2>  Prior(mu_ex_v5_State(initial_token))?mu_ex_v5_initState(initial_token)(e))
                  (b1)))
               (b)))
             Base(``use sr``;Unit)(e))
           ((b:
                ((b1:
                   ((b1)
                    (b2:. <b, b1, b2>  Prior(mu_ex_v5_State(initial_token))?mu_ex_v5_initState(initial_token)(e))))
                 (b)))
               Base([token];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(``enter  cs``;Unit;u)>  \mmember{}  mu\_ex\_v5\_main(initial$_{token}$;m1;m2;pr\000Coc1;proc2)(e)
    \mLeftarrow{}{}\mRightarrow{}  ((loc(e)  =  proc1)  \mdownarrow{}\mvee{}  (loc(e)  =  proc2))
            \mwedge{}  (u  =  \mcdot{})
            \mwedge{}  (i  =  (mu\_ex\_v5\_getMachine(m1;m2;proc1)  loc(e)))
            \mwedge{}  (\mdownarrow{}((\mdownarrow{}\mexists{}b:\mBbbB{}
                            ((\mexists{}b1:\mBbbB{}
                                  ((\mexists{}b2:\mBbbB{}
                                        <b,  b1,  b2>  \mmember{}
                                          Prior(mu\_ex\_v5\_State(initial$_{token}$))?mu\_ex\_v5\_initState\000C(initial$_{token}$)(e))
                                  \mwedge{}  (\muparrow{}b1)))
                            \mwedge{}  (\mneg{}\muparrow{}b)))
                    \mwedge{}  \mcdot{}  \mmember{}  Base(``use  sr``;Unit)(e))
                    \mvee{}  ((\mdownarrow{}\mexists{}b:\mBbbB{}
                                ((\mexists{}b1:\mBbbB{}
                                      ((\mneg{}\muparrow{}b1)
                                      \mwedge{}  (\mexists{}b2:\mBbbB{}
                                              <b,  b1,  b2>  \mmember{}
                                                Prior(mu\_ex\_v5\_State(initial$_{token}$))?mu\_ex\_v5\_initSt\000Cate(initial$_{token}$)(e))))
                                \mwedge{}  (\muparrow{}b)))
                        \mwedge{}  \mcdot{}  \mmember{}  Base([token];Unit)(e))))


Date html generated: 2012_02_20-PM-07_51_13
Last ObjectModification: 2012_02_02-PM-03_01_10

Home Index