---

Step * of Lemma PiDataVal_ind_wf

∀[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)
BY
{ DatatypeIndWf 0 `PiDataVal` `PiDataVal_ind`  }

---

Latex:

---

Latex:
\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)


By

---

Latex:
DatatypeIndWf  0  `PiDataVal`  `PiDataVal\_ind` 

---

Home Index