---

Step * of Lemma virus-process_wf

∀[M,E:Type ─→ Type]. ∀[g:∩T:Type. (T ─→ E[T])].  (virus-process(g) ∈ process(P.M[P];P.E[P]))
BY
{ (ProveWfLemma
   THEN Unfold `process` 0
   THEN BLemma `fix_wf_corec`
   THEN Auto
   THEN GenConclAtAddrType ⌈T ─→ E[T]⌉ [2;1]⋅
   THEN Auto
   THEN With ⌈T⌉ (DVar `g')⋅
   THEN Auto) }

---

Latex:


\mforall{}[M,E:Type  {}\mrightarrow{}  Type].  \mforall{}[g:\mcap{}T:Type.  (T  {}\mrightarrow{}  E[T])].    (virus-process(g)  \mmember{}  process(P.M[P];P.E[P]))


By

(ProveWfLemma
  THEN  Unfold  `process`  0
  THEN  BLemma  `fix\_wf\_corec`
  THEN  Auto
  THEN  GenConclAtAddrType  \mkleeneopen{}T  {}\mrightarrow{}  E[T]\mkleeneclose{}  [2;1]\mcdot{}
  THEN  Auto
  THEN  With  \mkleeneopen{}T\mkleeneclose{}  (DVar  `g')\mcdot{}
  THEN  Auto)

---

Home Index