---

Step * 1 1 of Lemma PiDataVal-induction


1. [P] : PiDataVal() ─→ ℙ
2. ∀id:Id. P[pDVloc(id)]@i
3. ∀id:Id. ∀name:Name.  P[pDVloc_tag(id;name)]@i
4. ∀from:Id. ∀preList:pi_prefix() List.  P[pDVguards(from;preList)]@i
5. ∀val:Name. ∀index:ℕ.  P[pDVmsg(val;index)]@i
6. P[pDVfire()]@i
7. P[pDVcontinue()]@i
8. ∀rndv1:ℕ × Id × ℕ × Name. P[pDVselex(rndv1)]@i
9. ∀rndv2:ℕ × Id × ℕ × Name. ∀counter:ℕ.  P[pDVrequest(rndv2;counter)]@i
10. y : id:Id × Name + from:Id × (pi_prefix() List) + val:Name × ℕ + Unit + Unit + ℕ × Id × ℕ × Name + (rndv2:ℕ
                                                                                                       × Id
                                                                                                       × ℕ
                                                                                                       × Name × ℕ)@i
⊢ P[inr y ]
BY
{ D -1 }

1
1. [P] : PiDataVal() ─→ ℙ
2. ∀id:Id. P[pDVloc(id)]@i
3. ∀id:Id. ∀name:Name.  P[pDVloc_tag(id;name)]@i
4. ∀from:Id. ∀preList:pi_prefix() List.  P[pDVguards(from;preList)]@i
5. ∀val:Name. ∀index:ℕ.  P[pDVmsg(val;index)]@i
6. P[pDVfire()]@i
7. P[pDVcontinue()]@i
8. ∀rndv1:ℕ × Id × ℕ × Name. P[pDVselex(rndv1)]@i
9. ∀rndv2:ℕ × Id × ℕ × Name. ∀counter:ℕ.  P[pDVrequest(rndv2;counter)]@i
10. x : id:Id × Name@i
⊢ P[inr (inl x) ]

2
1. [P] : PiDataVal() ─→ ℙ
2. ∀id:Id. P[pDVloc(id)]@i
3. ∀id:Id. ∀name:Name.  P[pDVloc_tag(id;name)]@i
4. ∀from:Id. ∀preList:pi_prefix() List.  P[pDVguards(from;preList)]@i
5. ∀val:Name. ∀index:ℕ.  P[pDVmsg(val;index)]@i
6. P[pDVfire()]@i
7. P[pDVcontinue()]@i
8. ∀rndv1:ℕ × Id × ℕ × Name. P[pDVselex(rndv1)]@i
9. ∀rndv2:ℕ × Id × ℕ × Name. ∀counter:ℕ.  P[pDVrequest(rndv2;counter)]@i
10. y1 : from:Id × (pi_prefix() List) + val:Name × ℕ + Unit + Unit + ℕ × Id × ℕ × Name + (rndv2:ℕ × Id × ℕ × Name × ℕ)@i
⊢ P[inr inr y1  ]

---

Latex:

---

Latex:

1.  [P]  :  PiDataVal()  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}id:Id.  P[pDVloc(id)]@i
3.  \mforall{}id:Id.  \mforall{}name:Name.    P[pDVloc\_tag(id;name)]@i
4.  \mforall{}from:Id.  \mforall{}preList:pi\_prefix()  List.    P[pDVguards(from;preList)]@i
5.  \mforall{}val:Name.  \mforall{}index:\mBbbN{}.    P[pDVmsg(val;index)]@i
6.  P[pDVfire()]@i
7.  P[pDVcontinue()]@i
8.  \mforall{}rndv1:\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name.  P[pDVselex(rndv1)]@i
9.  \mforall{}rndv2:\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name.  \mforall{}counter:\mBbbN{}.    P[pDVrequest(rndv2;counter)]@i
10.  y  :  id:Id  \mtimes{}  Name  +  from:Id
                                              \mtimes{}  (pi\_prefix()  List)  +  val:Name
                                                                                            \mtimes{}  \mBbbN{}  +  Unit  +  Unit  +  \mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name  +  (rndv2:\mBbbN{}
                                                                                                                                                                            \mtimes{}  Id
                                                                                                                                                                            \mtimes{}  \mBbbN{}
                                                                                                                                                                            \mtimes{}  Name  \mtimes{}  \mBbbN{})@i
\mvdash{}  P[inr  y  ]


By

---

Latex:
D  -1

---

Home Index