---

Step * of Lemma pi-run-example_wf

     (Unhideable token semantics in effect)

∀[P:pi_term()]. ∀[t:ℕ].
  (pi-run-example{$a,$b,$c,$d,$e,$f,$g,$h,$i,$j,$k}(P;t) ∈ {L:(ℤ × Id × Id × pMsg(P.piM(P))? × System(P.piM(P))) List| 
                                                            ||L|| = (t + 1) ∈ ℤ} )
BY
{ ProveWfLemma
THEN RepUR ``piM pMsg`` 0
THEN Auto }

1
1. P : pi_term()
2. t : ℕ
⊢ PiDataVal()

---

Latex:

---

Latex:
          (Unhideable  token  semantics  in  effect)

\mforall{}[P:pi\_term()].  \mforall{}[t:\mBbbN{}].
    (pi-run-example\{\$a,\$b,\$c,\$d,\$e,\$f,\$g,\$h,\$i,\$j,\$k\}(P;t)
      \mmember{}  \{L:(\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pMsg(P.piM(P))?  \mtimes{}  System(P.piM(P)))  List|  ||L||  =  (t  +  1)\}  )


By

---

Latex:
ProveWfLemma
THEN  RepUR  ``piM  pMsg``  0
THEN  Auto

---

Home Index