---

Step * of Lemma PiDataVal-induction

∀[P:PiDataVal() ⟶ ℙ]
  ((∀id:Id. P[pDVloc(id)])
  ⇒ (∀id:Id. ∀name:Name.  P[pDVloc_tag(id;name)])
  ⇒ (∀from:Id. ∀preList:pi_prefix() List.  P[pDVguards(from;preList)])
  ⇒ (∀val:Name. ∀index:ℕ.  P[pDVmsg(val;index)])
  ⇒ P[pDVfire()]
  ⇒ P[pDVcontinue()]
  ⇒ (∀rndv1:ℕ × Id × ℕ × Name. P[pDVselex(rndv1)])
  ⇒ (∀rndv2:ℕ × Id × ℕ × Name. ∀counter:ℕ.  P[pDVrequest(rndv2;counter)])
  ⇒ {∀x:PiDataVal(). P[x]})
BY
{ (Auto THEN (Unfold `guard` 0 THEN (D 0 THENA Auto))) }

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 : PiDataVal()@i
⊢ P[x]

---

Latex:

---

Latex:
\mforall{}[P:PiDataVal()  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}id:Id.  P[pDVloc(id)])
    {}\mRightarrow{}  (\mforall{}id:Id.  \mforall{}name:Name.    P[pDVloc\_tag(id;name)])
    {}\mRightarrow{}  (\mforall{}from:Id.  \mforall{}preList:pi\_prefix()  List.    P[pDVguards(from;preList)])
    {}\mRightarrow{}  (\mforall{}val:Name.  \mforall{}index:\mBbbN{}.    P[pDVmsg(val;index)])
    {}\mRightarrow{}  P[pDVfire()]
    {}\mRightarrow{}  P[pDVcontinue()]
    {}\mRightarrow{}  (\mforall{}rndv1:\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name.  P[pDVselex(rndv1)])
    {}\mRightarrow{}  (\mforall{}rndv2:\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name.  \mforall{}counter:\mBbbN{}.    P[pDVrequest(rndv2;counter)])
    {}\mRightarrow{}  \{\mforall{}x:PiDataVal().  P[x]\})


By

---

Latex:
(Auto  THEN  (Unfold  `guard`  0  THEN  (D  0  THENA  Auto)))

---

Home Index