---

Step * of Lemma iterate-process_wf

∀[M,E:Type ─→ Type].
  (∀P:process(P.M[P];P.E[P]). ∀inputs:M[process(P.M[P];P.E[P])] List.  (P*(inputs) ∈ process(P.M[P];P.E[P]))) supposing 
     (Continuous+(P.E[P]) and 
     Continuous+(P.M[P]))
BY
{ (InstLemma `process-subtype` []⋅
   THEN RepeatFor 4 (ParallelLast')
   THEN ProveWfLemma
   THEN GenConclAtAddrType ⌈M[process(P.M[P];P.E[P])] ─→ (process(P.M[P];P.E[P]) × E[process(P.M[P];P.E[P])])⌉ [2;1]⋅
   THEN Auto) }

---

Latex:


\mforall{}[M,E:Type  {}\mrightarrow{}  Type].
    (\mforall{}P:process(P.M[P];P.E[P]).  \mforall{}inputs:M[process(P.M[P];P.E[P])]  List.
          (P*(inputs)  \mmember{}  process(P.M[P];P.E[P])))  supposing 
          (Continuous+(P.E[P])  and 
          Continuous+(P.M[P]))


By

(InstLemma  `process-subtype`  []\mcdot{}
  THEN  RepeatFor  4  (ParallelLast')
  THEN  ProveWfLemma
  THEN  GenConclAtAddrType  \mkleeneopen{}M[process(P.M[P];P.E[P])]
                                                    {}\mrightarrow{}  (process(P.M[P];P.E[P])  \mtimes{}  E[process(P.M[P];P.E[P])])\mkleeneclose{}  [2;1]\mcdot{}
  THEN  Auto)

---

Home Index