Nuprl Lemma : mu_ex_v4_EnterCS-ilf

[cs,initial_token,proc1,proc2:Id]. [es:EO']. [e:E]. [i,i1:Id].
  (<i, make-Msg(``enter cs``;Id;i1)>  mu_ex_v4_main(cs;initial_token;proc1;proc2)(e)
   ((loc(e) = proc1)  (loc(e) = proc2))
       (((<i, make-Msg(``enter cs``;Id;i1)>  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)
         ((((i = cs)  (i1 = loc(e)))
            (b:
               ((b1:
                  ((b2:. <b, b1, b2>  Prior(mu_ex_v4_State(initial_token))?mu_ex_v4_initState(initial_token)(e))
                   (b1)))
                (b))))
            (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))
           (i = cs)
           (i1 = loc(e)))
           (a:. a  Base([token];)(e))))
         <i, make-Msg(``enter cs``;Id;i1)>  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)))


Proof not projected

Error : references
\mforall{}[cs,initial$_{token}$,proc1,proc2:Id].  \mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[i,i1:Id].
    (<i,  make-Msg(``enter  cs``;Id;i1)>  \mmember{}  mu\_ex\_v4\_main(cs;initial$_{token}$;proc1;\000Cproc2)(e)
    \mLeftarrow{}{}\mRightarrow{}  ((loc(e)  =  proc1)  \mdownarrow{}\mvee{}  (loc(e)  =  proc2))
            \mwedge{}  (((<i,  make-Msg(``enter  cs``;Id;i1)>  \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{}  ((((i  =  cs)  \mwedge{}  (i1  =  loc(e)))
                      \mwedge{}  (\mexists{}b:\mBbbB{}
                              ((\mexists{}b1:\mBbbB{}
                                    ((\mexists{}b2:\mBbbB{}
                                          <b,  b1,  b2>  \mmember{}
                                            Prior(mu\_ex\_v4\_State(initial$_{token}$))?mu\_ex\_v4\_initStat\000Ce(initial$_{token}$)(e))
                                    \mwedge{}  (\muparrow{}b1)))
                              \mwedge{}  (\mneg{}\muparrow{}b))))
                      \mwedge{}  (\mexists{}a:Id.  a  \mmember{}  Base(``use  cs``;Id)(e))))
                \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{}  (i1  =  loc(e)))
                    \mwedge{}  (\mdownarrow{}\mexists{}a:\mBbbZ{}.  a  \mmember{}  Base([token];\mBbbZ{})(e))))
                \mdownarrow{}\mvee{}  <i,  make-Msg(``enter  cs``;Id;i1)>  \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)))


Date html generated: 2012_02_20-PM-07_51_10
Last ObjectModification: 2012_02_02-PM-02_55_50

Home Index