---

Step * of Lemma recprocess_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]))]. ∀[ext:∩T:Type
                                                                                                        (E[T]
                                                                                                        ─→ M[T]
                                                                                                        ─→ T
                                                                                                        ─→ E[T])].
     (recprocess(s0;s,m.next[s;m];e,m,p.ext[e;m;p]) ∈ process(P.M[P];P.E[P]))) supposing 
     (Continuous+(T.E[T]) and 
     Continuous+(T.M[T]) and 
     Continuous+(T.S[T]))
BY
{ WithCumulativity((ProveWfLemma
                    THEN Unfold `process` 0
                    THEN Using [`A',⌈S⌉] (BLemma `fix_wf_corec_parameter3`)⋅
                    THEN Try (Complete (Auto))
                    THEN Isect2CD
                    THEN Auto
                    THEN All (Fold `process`)
                    THEN 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]))].
      \mforall{}[ext:\mcap{}T:Type.  (E[T]  {}\mrightarrow{}  M[T]  {}\mrightarrow{}  T  {}\mrightarrow{}  E[T])].
          (recprocess(s0;s,m.next[s;m];e,m,p.ext[e;m;p])  \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((ProveWfLemma
                                    THEN  Unfold  `process`  0
                                    THEN  Using  [`A',\mkleeneopen{}S\mkleeneclose{}]  (BLemma  `fix\_wf\_corec\_parameter3`)\mcdot{}
                                    THEN  Try  (Complete  (Auto))
                                    THEN  Isect2CD
                                    THEN  Auto
                                    THEN  All  (Fold  `process`)
                                    THEN  Auto))

---

Home Index