Nuprl Lemma : mu_ex_v5_main-ilf

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


Proof not projected

Error : references
\mforall{}[initial$_{token}$,m1,m2,proc1,proc2:Id].  \mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[i:Id].  \mforall{}[m:Messa\000Cge].
    \{<i,  m>  \mmember{}  mu\_ex\_v5\_main(initial$_{token}$;m1;m2;proc1;proc2)(e)
    \mLeftarrow{}{}\mRightarrow{}  ((loc(e)  =  proc1)  \mdownarrow{}\mvee{}  (loc(e)  =  proc2))
            \mwedge{}  ((((\mcdot{}  \mmember{}  Base([request];Unit)(e)
                \mwedge{}  ((i  =  (mu\_ex\_v5\_getOtherProc(proc1;proc2)  loc(e)))  \mwedge{}  (m  =  make-Msg([token];Unit;\mcdot{})))
                \mwedge{}  (\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(\000Cinitial$_{token}$)(e))))
                        \mwedge{}  (\mneg{}\muparrow{}b))))
                \mdownarrow{}\mvee{}  (\mcdot{}  \mmember{}  Base(``use  sr``;Unit)(e)
                      \mwedge{}  (\mexists{}b,b1:\mBbbB{}
                              ((\mexists{}b2:\mBbbB{}
                                    <b,  b1,  b2>  \mmember{}
                                      Prior(mu\_ex\_v5\_State(initial$_{token}$))?mu\_ex\_v5\_initState(i\000Cnitial$_{token}$)(e))
                              \mwedge{}  (((\muparrow{}b)
                                  \mwedge{}  (i  =  (mu\_ex\_v5\_getMachine(m1;m2;proc1)  loc(e)))
                                  \mwedge{}  (m  =  make-Msg([busy];Unit;\mcdot{})))
                                  \mvee{}  ((\mneg{}\muparrow{}b)
                                      \mwedge{}  (((\muparrow{}b1)
                                          \mwedge{}  (i  =  (mu\_ex\_v5\_getMachine(m1;m2;proc1)  loc(e)))
                                          \mwedge{}  (m  =  make-Msg(``enter  cs``;Unit;\mcdot{})))
                                          \mvee{}  ((\mneg{}\muparrow{}b1)
                                              \mwedge{}  (i  =  (mu\_ex\_v5\_getOtherProc(proc1;proc2)  loc(e)))
                                              \mwedge{}  (m  =  make-Msg([request];Unit;\mcdot{}))))))))))
                \mvee{}  (\mcdot{}  \mmember{}  Base([token];Unit)(e)
                    \mwedge{}  ((i  =  (mu\_ex\_v5\_getMachine(m1;m2;proc1)  loc(e)))  \mwedge{}  (m  =  make-Msg(``enter  cs``;Unit;\mcdot{})))
                    \mwedge{}  (\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\_initSta\000Cte(initial$_{token}$)(e))))
                              \mwedge{}  (\muparrow{}b)))))
                \mdownarrow{}\mvee{}  (\mcdot{}  \mmember{}  Base(``leave  cs``;Unit)(e)
                      \mwedge{}  ((i  =  (mu\_ex\_v5\_getOtherProc(proc1;proc2)  loc(e)))  \mwedge{}  (m  =  make-Msg([token];Unit;\mcdot{})))
                      \mwedge{}  (\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)))))\}


Date html generated: 2012_02_20-PM-07_51_11
Last ObjectModification: 2012_02_02-PM-03_00_50

Home Index