---

Step * of Lemma process-valueall-type

∀[M,E:Type ─→ Type].  valueall-type(process(P.M[P];P.E[P])) supposing M[Top]
BY
{ (Auto THEN InstLemma `subtype-valueall-type` [⌈process(P.M[P];P.E[P])⌉;⌈M[Top] ─→ (Top × E[Top])⌉]⋅ THEN Auto) }

1
.....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]))

---

Latex:


\mforall{}[M,E:Type  {}\mrightarrow{}  Type].    valueall-type(process(P.M[P];P.E[P]))  supposing  M[Top]


By

(Auto
  THEN  InstLemma  `subtype-valueall-type`  [\mkleeneopen{}process(P.M[P];P.E[P])\mkleeneclose{};\mkleeneopen{}M[Top]  {}\mrightarrow{}  (Top  \mtimes{}  E[Top])\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index