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