---

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:

---

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

---

Latex:
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