Nuprl Lemma : mu_ex_v4_main-ilf

[cs,initial_token,proc1,proc2:Id]. [es:EO']. [e:E]. [i:Id]. [m:Message].
  (<i, m>  mu_ex_v4_main(cs;initial_token;proc1;proc2)(e)
   (((loc(e) = proc1)  (loc(e) = proc2))
       (((<i, m>  concat-lifting-loc-3(zi,zh,n,z.
                                          let interested,token,toreply = z in 
                                          if interested
                                          then {}
                                          else {mu_ex_v4_send_token() (mu_ex_v4_otherProc(proc1;proc2) loc(e)) (n + 1)}
                                          fi )|Loc, mu_ex_v4_Request(), mu_ex_v4_PrToken(),
                    mu_ex_v4_PrState(initial_token)|(e)
         (a:Id
             (a  Base(``use cs``;Id)(e)
              (b,b1:
                 ((b2:. <b, b1, b2>  Prior(mu_ex_v4_State(initial_token))?mu_ex_v4_initState(initial_token)(e))
                  (((b)  (i = a)  (m = make-Msg([busy];Unit;)))
                    ((b)
                      (((b1)  (i = cs)  (m = make-Msg(``enter cs``;Id;loc(e))))
                        ((b1)
                          (i = (mu_ex_v4_otherProc(proc1;proc2) loc(e)))
                          (m = make-Msg([request];Unit;)))))))))))
         (((b,b1,b2:. <b, b1, b2>  Prior(mu_ex_v4_State(initial_token))?mu_ex_v4_initState(initial_token)(e))
           (i = cs)
           (m = make-Msg(``enter cs``;Id;loc(e))))
           (a:. a  Base([token];)(e))))
         <i, m>  concat-lifting-loc-3(zl,zk,n,z.
                                          let interested,token,toreply = z in 
                                          if toreply
                                          then {mu_ex_v4_send_token() (mu_ex_v4_otherProc(proc1;proc2) loc(e)) (n + 1)}
                                          else {}
                                          fi )|Loc, mu_ex_v4_LeaveCS(), mu_ex_v4_PrToken(),
                    mu_ex_v4_PrState(initial_token)|(e)))
       ((loc(e) = cs)
          (((i = loc(e))  (a:Id. ((m = make-Msg([exec];Id;a))  a  Base(``enter cs``;Id)(e))))
            ((m = make-Msg(``leave cs``;Unit;))  i  Base([exec];Id)(e)))))


Proof not projected

Error : references
\mforall{}[cs,initial$_{token}$,proc1,proc2:Id].  \mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[i:Id].  \mforall{}[m:Message]\000C.
    (<i,  m>  \mmember{}  mu\_ex\_v4\_main(cs;initial$_{token}$;proc1;proc2)(e)
    \mLeftarrow{}{}\mRightarrow{}  (((loc(e)  =  proc1)  \mdownarrow{}\mvee{}  (loc(e)  =  proc2))
            \mwedge{}  (((<i,  m>  \mmember{}  concat-lifting-loc-3(\mlambda{}zi,zh,n,z.
                                                                                    let  interested,token,toreply  =  z  in 
                                                                                    if  interested
                                                                                    then  \{\}
                                                                                    else  \{mu\_ex\_v4\_send\_token() 
                                                                                                (mu\_ex\_v4\_otherProc(proc1;proc2)  loc(e)) 
                                                                                                (n  +  1)\}
                                                                                    fi  )|Loc,  mu\_ex\_v4\_Request(),  mu\_ex\_v4\_PrToken(),
                                        mu\_ex\_v4\_PrState(initial$_{token}$)|(e)
                \mdownarrow{}\mvee{}  (\mexists{}a:Id
                          (a  \mmember{}  Base(``use  cs``;Id)(e)
                          \mwedge{}  (\mexists{}b,b1:\mBbbB{}
                                  ((\mexists{}b2:\mBbbB{}
                                        <b,  b1,  b2>  \mmember{}
                                          Prior(mu\_ex\_v4\_State(initial$_{token}$))?mu\_ex\_v4\_initState\000C(initial$_{token}$)(e))
                                  \mwedge{}  (((\muparrow{}b)  \mwedge{}  (i  =  a)  \mwedge{}  (m  =  make-Msg([busy];Unit;\mcdot{})))
                                      \mvee{}  ((\mneg{}\muparrow{}b)
                                          \mwedge{}  (((\muparrow{}b1)  \mwedge{}  (i  =  cs)  \mwedge{}  (m  =  make-Msg(``enter  cs``;Id;loc(e))))
                                              \mvee{}  ((\mneg{}\muparrow{}b1)
                                                  \mwedge{}  (i  =  (mu\_ex\_v4\_otherProc(proc1;proc2)  loc(e)))
                                                  \mwedge{}  (m  =  make-Msg([request];Unit;\mcdot{})))))))))))
                \mvee{}  (((\mdownarrow{}\mexists{}b,b1,b2:\mBbbB{}
                              <b,  b1,  b2>  \mmember{}  Prior(mu\_ex\_v4\_State(initial$_{token}$))?mu\_ex\_v4\_i\000CnitState(initial$_{token}$)(
                                                          e))
                    \mwedge{}  (i  =  cs)
                    \mwedge{}  (m  =  make-Msg(``enter  cs``;Id;loc(e))))
                    \mwedge{}  (\mdownarrow{}\mexists{}a:\mBbbZ{}.  a  \mmember{}  Base([token];\mBbbZ{})(e))))
                \mdownarrow{}\mvee{}  <i,  m>  \mmember{}  concat-lifting-loc-3(\mlambda{}zl,zk,n,z.
                                                                                    let  interested,token,toreply  =  z  in 
                                                                                    if  toreply
                                                                                    then  \{mu\_ex\_v4\_send\_token() 
                                                                                                (mu\_ex\_v4\_otherProc(proc1;proc2)  loc(e)) 
                                                                                                (n  +  1)\}
                                                                                    else  \{\}
                                                                                    fi  )|Loc,  mu\_ex\_v4\_LeaveCS(),  mu\_ex\_v4\_PrToken(),
                                        mu\_ex\_v4\_PrState(initial$_{token}$)|(e)))
            \mdownarrow{}\mvee{}  ((loc(e)  =  cs)
                  \mwedge{}  (((i  =  loc(e))  \mwedge{}  (\mexists{}a:Id.  ((m  =  make-Msg([exec];Id;a))  \mwedge{}  a  \mmember{}  Base(``enter  cs``;Id)(e))))
                      \mdownarrow{}\mvee{}  ((m  =  make-Msg(``leave  cs``;Unit;\mcdot{}))  \mwedge{}  i  \mmember{}  Base([exec];Id)(e)))))


Date html generated: 2012_02_20-PM-07_51_08
Last ObjectModification: 2012_02_02-PM-02_55_34

Home Index