Nuprl Lemma : mu_ex_v5_Request-ilf

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


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([request];Unit;u)>  \mmember{}  mu\_ex\_v5\_main(initial$_{token}$;m1;m2;proc1\000C;proc2)(e)
    \mLeftarrow{}{}\mRightarrow{}  ((loc(e)  =  proc1)  \mdownarrow{}\mvee{}  (loc(e)  =  proc2))
            \mwedge{}  \mcdot{}  \mmember{}  Base(``use  sr``;Unit)(e)
            \mwedge{}  ((i  =  (mu\_ex\_v5\_getOtherProc(proc1;proc2)  loc(e)))  \mwedge{}  (u  =  \mcdot{}))
            \mwedge{}  (\mdownarrow{}\mexists{}b:\mBbbB{}
                      ((\mexists{}b1:\mBbbB{}
                            ((\mexists{}b2:\mBbbB{}
                                  <b,  b1,  b2>  \mmember{}  Prior(mu\_ex\_v5\_State(initial$_{token}$))?mu\_ex\_v5\000C\_initState(initial$_{token}$)(
                                                              e))
                            \mwedge{}  (\mneg{}\muparrow{}b1)))
                      \mwedge{}  (\mneg{}\muparrow{}b))))


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

Home Index