---

{ [X:{j}]. [x:PiDataVal()]. [loc:id:Id  X]. [loc_tag:id:Id
                                                             name:Name
                                                             X].
  [guards:from:Id  preList:pi_prefix() List  X]. [msg:val:Name
                                                             index:
                                                             X].
  [fire,continue:X]. [selex:rndv1:  Id    Name  X].
  [request:rndv2:  Id    Name  counter:  X].
    (F((x) where  
     F(id) = loc[id]  
     F(id,name) = loc_tag[id;name]  
     F(from,preList) = guards[from;preList]  
     F(val,index) = msg[val;index]  
     F(fire) = fire  
     F(continue) = continue  
     F(rndv1) = selex[rndv1]  
     F(rndv2,counter) = request[rndv2;counter]  X) }

{ Proof }

---

Definitions occuring in Statement :  PiDataVal: PiDataVal(),  pi_prefix: pi_prefix(),  Id: Id,  name: Name,  nat: ,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  so_apply: x[s],  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  list: type List,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  PiDataVal_ind: PiDataVal_ind,  so_apply: x[s],  so_apply: x[s1;s2],  pi1: fst(t),  pi2: snd(t),  PiDataVal: PiDataVal()
Lemmas :  nat_wf,  Id_wf,  name_wf,  pi_prefix_wf,  PiDataVal_wf

---

\mforall{}[X:\mBbbU{}\{j\}].  \mforall{}[x:PiDataVal()].  \mforall{}[loc:id:Id  {}\mrightarrow{}  X].  \mforall{}[loc$_{tag}$:id:Id  {}\mrightarrow{}  name:Name\000C  {}\mrightarrow{}  X].
\mforall{}[guards:from:Id  {}\mrightarrow{}  preList:pi\_prefix()  List  {}\mrightarrow{}  X].  \mforall{}[msg:val:Name  {}\mrightarrow{}  index:\mBbbN{}  {}\mrightarrow{}  X].
\mforall{}[fire,continue:X].  \mforall{}[selex:rndv1:\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name  {}\mrightarrow{}  X].  \mforall{}[request:rndv2:\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name
                                                                                                                                          {}\mrightarrow{}  counter:\mBbbN{}
                                                                                                                                          {}\mrightarrow{}  X].
    (F((x)  where   
      F(id)  =  loc[id]   
      F(id,name)  =  loc$_{tag}$[id;name]   
      F(from,preList)  =  guards[from;preList]   
      F(val,index)  =  msg[val;index]   
      F(fire)  =  fire   
      F(continue)  =  continue   
      F(rndv1)  =  selex[rndv1]   
      F(rndv2,counter)  =  request[rndv2;counter]  \mmember{}  X)


Date html generated: 2011_08_17-PM-06_54_02
Last ObjectModification: 2011_06_18-PM-12_29_14

Home Index