Nuprl Lemma : mu_ex_v4-ilf

(([es:EO']. [e:E].
    {inl    mu_ex_v4_Request() + mu_ex_v4_Token() + mu_ex_v4_UseCS() + mu_ex_v4_LeaveCS()(e)
       Base([request];Unit)(e)})
 ([es:EO']. [e:E].
     a:
       {inr (inl a )   mu_ex_v4_Request() + mu_ex_v4_Token() + mu_ex_v4_UseCS() + mu_ex_v4_LeaveCS()(e)
        a  Base([token];)(e)  (  Base([request];Unit)(e))})
 ([es:EO']. [e:E].
     a:Id
       {inr inr (inl a )    mu_ex_v4_Request() + mu_ex_v4_Token() + mu_ex_v4_UseCS() + mu_ex_v4_LeaveCS()(e)
        (a  Base(``use cs``;Id)(e)  (w:. (w  Base([token];)(e))))  (  Base([request];Unit)(e))})
 ([es:EO']. [e:E].
     {inr inr inr      mu_ex_v4_Request() + mu_ex_v4_Token() + mu_ex_v4_UseCS() + mu_ex_v4_LeaveCS()(e)
      ((  Base(``leave cs``;Unit)(e)  (w:Id. (w  Base(``use cs``;Id)(e))))
          (w:. (w  Base([token];)(e))))
          (  Base([request];Unit)(e))}))
 ([initial_token:Id]. [es:EO']. [e:E].
     v:    
       {v  mu_ex_v4_State(initial_token)(e)
        L:(Unit +  + (Id?)  E) List
             (prior-classrel-list(es;Unit +  + (Id?);mu_ex_v4_Request() + mu_ex_v4_Token() + ... + ...;L;e)
              ((  Base([request];Unit)(e)
                (v
                 = (mu_ex_v4_onRequest() loc(e)  
                    list_accum(b,a.mu_ex_v4_onRequest() + mu_ex_v4_onToken() + mu_ex_v4_onUseCS() + ... 
                                   loc(e) 
                                   a 
                                   b;
                               <ff, IdDeq initial_token loc(e), ff>;
                               map(p.(fst(p));L)))))
                ((  Base([request];Unit)(e))
                  ((a:
                      ((v
                      = (mu_ex_v4_onToken() loc(e) a 
                         list_accum(b,a.mu_ex_v4_onRequest() + mu_ex_v4_onToken() + mu_ex_v4_onUseCS() + ... 
                                        loc(e) 
                                        a 
                                        b;
                                    <ff, IdDeq initial_token loc(e), ff>;
                                    map(p.(fst(p));L))))
                       a  Base([token];)(e)))
                    ((w:. (w  Base([token];)(e)))
                      ((a:Id
                          (a  Base(``use cs``;Id)(e)
                           (v
                            = (mu_ex_v4_onUseCS() loc(e) a 
                               list_accum(b,a.mu_ex_v4_onRequest() + mu_ex_v4_onToken() + mu_ex_v4_onUseCS() + ... 
                                              loc(e) 
                                              a 
                                              b;
                                          <ff, IdDeq initial_token loc(e), ff>;
                                          map(p.(fst(p));L))))))
                        ((  Base(``leave cs``;Unit)(e)  (w:Id. (w  Base(``use cs``;Id)(e))))
                          (v
                           = (mu_ex_v4_onLeaveCS() loc(e)  
                              list_accum(b,a.mu_ex_v4_onRequest() + mu_ex_v4_onToken() + mu_ex_v4_onUseCS() + ... 
                                             loc(e) 
                                             a 
                                             b;
                                         <ff, IdDeq initial_token loc(e), ff>;
                                         map(p.(fst(p));L)))))))))))})
 ([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{}[es:EO'].  \mforall{}[e:E].
        \{inl  \mcdot{}    \mmember{}  mu\_ex\_v4\_Request()  +  mu\_ex\_v4\_Token()  +  mu\_ex\_v4\_UseCS()  +  mu\_ex\_v4\_LeaveCS()(e)
        \mLeftarrow{}{}\mRightarrow{}  \mcdot{}  \mmember{}  Base([request];Unit)(e)\})
\mwedge{}  (\mforall{}[es:EO'].  \mforall{}[e:E].
          \mforall{}a:\mBbbZ{}
              \{inr  (inl  a  )    \mmember{}
                  mu\_ex\_v4\_Request()  +  mu\_ex\_v4\_Token()  +  mu\_ex\_v4\_UseCS()  +  mu\_ex\_v4\_LeaveCS()(e)
              \mLeftarrow{}{}\mRightarrow{}  a  \mmember{}  Base([token];\mBbbZ{})(e)  \mwedge{}  (\mneg{}\mcdot{}  \mmember{}  Base([request];Unit)(e))\})
\mwedge{}  (\mforall{}[es:EO'].  \mforall{}[e:E].
          \mforall{}a:Id
              \{inr  inr  (inl  a  )      \mmember{}
                  mu\_ex\_v4\_Request()  +  mu\_ex\_v4\_Token()  +  mu\_ex\_v4\_UseCS()  +  mu\_ex\_v4\_LeaveCS()(e)
              \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  Base(``use  cs``;Id)(e)  \mwedge{}  (\mdownarrow{}\mforall{}w:\mBbbZ{}.  (\mneg{}w  \mmember{}  Base([token];\mBbbZ{})(e))))
                      \mwedge{}  (\mneg{}\mcdot{}  \mmember{}  Base([request];Unit)(e))\})
\mwedge{}  (\mforall{}[es:EO'].  \mforall{}[e:E].
          \{inr  inr  inr  \mcdot{}        \mmember{}
              mu\_ex\_v4\_Request()  +  mu\_ex\_v4\_Token()  +  mu\_ex\_v4\_UseCS()  +  mu\_ex\_v4\_LeaveCS()(e)
          \mLeftarrow{}{}\mRightarrow{}  ((\mcdot{}  \mmember{}  Base(``leave  cs``;Unit)(e)  \mwedge{}  (\mdownarrow{}\mforall{}w:Id.  (\mneg{}w  \mmember{}  Base(``use  cs``;Id)(e))))
                  \mwedge{}  (\mdownarrow{}\mforall{}w:\mBbbZ{}.  (\mneg{}w  \mmember{}  Base([token];\mBbbZ{})(e))))
                  \mwedge{}  (\mneg{}\mcdot{}  \mmember{}  Base([request];Unit)(e))\}))
\mwedge{}  (\mforall{}[initial$_{token}$:Id].  \mforall{}[es:EO'].  \mforall{}[e:E].
          \mforall{}v:\mBbbB{}  \mtimes{}  \mBbbB{}  \mtimes{}  \mBbbB{}
              \{v  \mmember{}  mu\_ex\_v4\_State(initial$_{token}$)(e)
              \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}L:(Unit  +  \mBbbZ{}  +  (Id?)  \mtimes{}  E)  List
                          (prior-classrel-list(es;Unit  +  \mBbbZ{}  +  (Id?);mu\_ex\_v4\_Request()  +  ...  +  ...  +  ...;L;e)
                          \mwedge{}  ((\mcdot{}  \mmember{}  Base([request];Unit)(e)
                              \mwedge{}  (v
                                  =  (mu\_ex\_v4\_onRequest()  loc(e)  \mcdot{} 
                                        list\_accum(b,a.mu\_ex\_v4\_onRequest()  +  mu\_ex\_v4\_onToken()  +  ...  +  ... 
                                                                      loc(e) 
                                                                      a 
                                                                      b;
                                                              <ff,  IdDeq  initial$_{token}$  loc(e),  ff>
                                                              map(\mlambda{}p.(fst(p));L)))))
                              \mvee{}  ((\mneg{}\mcdot{}  \mmember{}  Base([request];Unit)(e))
                                  \mwedge{}  ((\mexists{}a:\mBbbZ{}
                                            ((v
                                            =  (mu\_ex\_v4\_onToken()  loc(e)  a 
                                                  list\_accum(b,a.mu\_ex\_v4\_onRequest()  +  mu\_ex\_v4\_onToken()  +  ...  +  ... 
                                                                                loc(e) 
                                                                                a 
                                                                                b;
                                                                        <ff,  IdDeq  initial$_{token}$  loc(e),  ff>
                                                                        map(\mlambda{}p.(fst(p));L))))
                                            \mwedge{}  a  \mmember{}  Base([token];\mBbbZ{})(e)))
                                      \mvee{}  ((\mdownarrow{}\mforall{}w:\mBbbZ{}.  (\mneg{}w  \mmember{}  Base([token];\mBbbZ{})(e)))
                                          \mwedge{}  ((\mexists{}a:Id
                                                    (a  \mmember{}  Base(``use  cs``;Id)(e)
                                                    \mwedge{}  (v
                                                        =  (mu\_ex\_v4\_onUseCS()  loc(e)  a 
                                                              list\_accum(b,a.mu\_ex\_v4\_onRequest()  +  mu\_ex\_v4\_onToken()  +  ...  +  ... 
                                                                                            loc(e) 
                                                                                            a 
                                                                                            b;
                                                                                    <ff,  IdDeq  initial$_{token}$  loc(e),  f\000Cf>
                                                                                    map(\mlambda{}p.(fst(p));L))))))
                                              \mvee{}  ((\mcdot{}  \mmember{}  Base(``leave  cs``;Unit)(e)  \mwedge{}  (\mdownarrow{}\mforall{}w:Id.  (\mneg{}w  \mmember{}  Base(``use  cs``;Id)(e))))
                                                  \mwedge{}  (v
                                                      =  (mu\_ex\_v4\_onLeaveCS()  loc(e)  \mcdot{} 
                                                            list\_accum(b,a.mu\_ex\_v4\_onRequest()  +  mu\_ex\_v4\_onToken()  +  ...  +  ... 
                                                                                          loc(e) 
                                                                                          a 
                                                                                          b;
                                                                                  <ff,  IdDeq  initial$_{token}$  loc(e),  ff\000C>
                                                                                  map(\mlambda{}p.(fst(p));L)))))))))))\})
\mwedge{}  (\mforall{}[cs,initial$_{token}$,proc1,proc2:Id].  \mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[i:Id].  \mforall{}[m:Messa\000Cge].
          \{<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\_initSt\000Cate(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\_initState(i\000Cnitial$_{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_07
Last ObjectModification: 2012_02_02-PM-02_55_30

Home Index