Nuprl Lemma : mu_ex_v4_LeaveCS-ilf

[cs,initial_token,proc1,proc2:Id]. [es:EO']. [e:E]. [i:Id]. [u:Unit].
  (<i, make-Msg(``leave cs``;Unit;u)>  mu_ex_v4_main(cs;initial_token;proc1;proc2)(e)
   (((loc(e) = proc1)  (loc(e) = proc2))
       (<i, make-Msg(``leave cs``;Unit;u)>  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, make-Msg(``leave cs``;Unit;u)>  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)  (u = )  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{}[u:Unit].
    (<i,  make-Msg(``leave  cs``;Unit;u)>  \mmember{}  mu\_ex\_v4\_main(cs;initial$_{token}$;proc1\000C;proc2)(e)
    \mLeftarrow{}{}\mRightarrow{}  (((loc(e)  =  proc1)  \mdownarrow{}\mvee{}  (loc(e)  =  proc2))
            \mwedge{}  (<i,  make-Msg(``leave  cs``;Unit;u)>  \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,  make-Msg(``leave  cs``;Unit;u)>  \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{}  (u  =  \mcdot{})  \mwedge{}  i  \mmember{}  Base([exec];Id)(e)))


Date html generated: 2012_02_20-PM-07_51_09
Last ObjectModification: 2012_02_02-PM-02_55_46

Home Index