---

Step * 1 of Lemma process-valueall-type

.....antecedent..... 
1. M : Type ⟶ Type
2. E : Type ⟶ Type
3. M[Top]
⊢ process(P.M[P];P.E[P]) ⊆r (M[Top] ⟶ (Top × E[Top]))
BY
{ ((D 0 THEN Auto) THEN (With ⌜1⌝ (D (-1))⋅ THEN Auto) THEN Reduce (-1) THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  M  :  Type  {}\mrightarrow{}  Type
2.  E  :  Type  {}\mrightarrow{}  Type
3.  M[Top]
\mvdash{}  process(P.M[P];P.E[P])  \msubseteq{}r  (M[Top]  {}\mrightarrow{}  (Top  \mtimes{}  E[Top]))


By

---

Latex:
((D  0  THEN  Auto)  THEN  (With  \mkleeneopen{}1\mkleeneclose{}  (D  (-1))\mcdot{}  THEN  Auto)  THEN  Reduce  (-1)  THEN  Auto)

---

Home Index