---

Step * 1 of Lemma forkable-process_wf

.....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 ∈ 𝔹
BY
{ (GenConclAtAddrType ⌜M[e] ⟶ 𝔹⌝ [2;1]⋅
   THEN Auto
   THEN With ⌜e⌝ (DVar `f')⋅
   THEN Auto
   THEN RepUR ``so_apply`` (-1)⋅
   THEN Auto)⋅ }

---

Latex:

---

Latex:
.....wf..... 
1.  M  :  Type  {}\mrightarrow{}  Type
2.  E  :  Type  {}\mrightarrow{}  Type
3.  Continuous+(T.M[T])
4.  Continuous+(T.E[T])
5.  g  :  \mcap{}T:Type.  (T  {}\mrightarrow{}  E[T])
6.  f  :  \mcap{}T:Type.  (M[T]  {}\mrightarrow{}  \mBbbB{})
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
\mvdash{}  f  Q  \mmember{}  \mBbbB{}


By

---

Latex:
(GenConclAtAddrType  \mkleeneopen{}M[e]  {}\mrightarrow{}  \mBbbB{}\mkleeneclose{}  [2;1]\mcdot{}
  THEN  Auto
  THEN  With  \mkleeneopen{}e\mkleeneclose{}  (DVar  `f')\mcdot{}
  THEN  Auto
  THEN  RepUR  ``so\_apply``  (-1)\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index