Nuprl Lemma : mu_ex_v4_Request-ilf
[cs,initial_token,proc1,proc2:Id]. 
[es:EO']. 
[e:E]. 
[i:Id]. 
[u:Unit].
  (<i, make-Msg([request];Unit;u)> 
 mu_ex_v4_main(cs;initial_token;proc1;proc2)(e)
  

 ((loc(e) = proc1) 
 (loc(e) = proc2))
      
 ((<i, make-Msg([request];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 = (mu_ex_v4_otherProc(proc1;proc2) loc(e))) 
 (u = 
))
          
 (
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))))
        
 <i, make-Msg([request];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)))
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([request];Unit;u)>  \mmember{}  mu\_ex\_v4\_main(cs;initial$_{token}$;proc1;pr\000Coc2)(e)
    \mLeftarrow{}{}\mRightarrow{}  ((loc(e)  =  proc1)  \mdownarrow{}\mvee{}  (loc(e)  =  proc2))
            \mwedge{}  ((<i,  make-Msg([request];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)
                \mvee{}  ((((i  =  (mu\_ex\_v4\_otherProc(proc1;proc2)  loc(e)))  \mwedge{}  (u  =  \mcdot{}))
                    \mwedge{}  (\mexists{}b:\mBbbB{}
                            ((\mexists{}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{}  (\mneg{}\muparrow{}b1)))
                            \mwedge{}  (\mneg{}\muparrow{}b))))
                    \mwedge{}  (\mexists{}a:Id.  a  \mmember{}  Base(``use  cs``;Id)(e))))
                \mdownarrow{}\mvee{}  <i,  make-Msg([request];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)))
Date html generated:
2012_02_20-PM-07_51_09
Last ObjectModification:
2012_02_02-PM-02_55_42
Home
Index