---

Step * of Lemma forkable-process_wf

∀[M,E:Type ─→ Type].
  (∀[g:∩T:Type. (T ─→ E[T])]. ∀[f:∩T:Type. (M[T] ─→ 𝔹)]. ∀[P:process(P.M[P];P.E[P])].
     (forkable-process(f;g;P) ∈ process(P.M[P];P.E[P]))) supposing 
     (Continuous+(T.E[T]) and 
     Continuous+(T.M[T]))
BY
{ WithCumulativity((ProveWfLemma
                    THEN Using [`S',⌈λ2T.T⌉] MemCD⋅
                    THEN Reduce 0
                    THEN Auto
                    THEN Try ((ProveContinuous THEN Auto)))) }

1
.....wf..... 
1. M : Type ─→ Type
2. E : Type ─→ Type
3. Continuous+(T.M[T])
4. Continuous+(T.E[T])
5. g : ∩T:Type. (T ─→ E[T])
6. f : ∩T:Type. (M[T] ─→ 𝔹)
7. P : process(P.M[P];P.E[P])
8. e : Type
9. m : E[e]@i
10. Q : M[e]@i
11. Q@0 : e@i
⊢ f Q ∈ 𝔹

---

Latex:


\mforall{}[M,E:Type  {}\mrightarrow{}  Type].
    (\mforall{}[g:\mcap{}T:Type.  (T  {}\mrightarrow{}  E[T])].  \mforall{}[f:\mcap{}T:Type.  (M[T]  {}\mrightarrow{}  \mBbbB{})].  \mforall{}[P:process(P.M[P];P.E[P])].
          (forkable-process(f;g;P)  \mmember{}  process(P.M[P];P.E[P])))  supposing 
          (Continuous+(T.E[T])  and 
          Continuous+(T.M[T]))


By

WithCumulativity((ProveWfLemma
                                    THEN  Using  [`S',\mkleeneopen{}\mlambda{}\msubtwo{}T.T\mkleeneclose{}]  MemCD\mcdot{}
                                    THEN  Reduce  0
                                    THEN  Auto
                                    THEN  Try  ((ProveContinuous  THEN  Auto))))

---

Home Index