---

Step * of Lemma rec-process_wf

∀[S,M,E:Type ─→ Type].
  (∀[s0:S[process(P.M[P];P.E[P])]]. ∀[next:∩T:{T:Type| process(P.M[P];P.E[P]) ⊆r T} 
                                             (S[M[T] ─→ (T × E[T])] ─→ M[T] ─→ (S[T] × E[T]))].
     (RecProcess(s0;s,m.next[s;m]) ∈ process(P.M[P];P.E[P]))) supposing 
     (Continuous+(T.E[T]) and 
     Continuous+(T.M[T]) and 
     Continuous+(T.S[T]))
BY
{ WithCumulativity((Auto
                    THEN Unfolds ``rec-process process`` 0
                    THEN Using [`A',⌈S⌉] (BLemma `fix_wf_corec_parameter3`)⋅
                    THEN Try (Complete (Auto)))) }

---

Latex:


\mforall{}[S,M,E:Type  {}\mrightarrow{}  Type].
    (\mforall{}[s0:S[process(P.M[P];P.E[P])]].  \mforall{}[next:\mcap{}T:\{T:Type|  process(P.M[P];P.E[P])  \msubseteq{}r  T\} 
                                                                                          (S[M[T]  {}\mrightarrow{}  (T  \mtimes{}  E[T])]  {}\mrightarrow{}  M[T]  {}\mrightarrow{}  (S[T]  \mtimes{}  E[T]))].
          (RecProcess(s0;s,m.next[s;m])  \mmember{}  process(P.M[P];P.E[P])))  supposing 
          (Continuous+(T.E[T])  and 
          Continuous+(T.M[T])  and 
          Continuous+(T.S[T]))


By

WithCumulativity((Auto
                                    THEN  Unfolds  ``rec-process  process``  0
                                    THEN  Using  [`A',\mkleeneopen{}S\mkleeneclose{}]  (BLemma  `fix\_wf\_corec\_parameter3`)\mcdot{}
                                    THEN  Try  (Complete  (Auto))))

---

Home Index