---

Step * 1 2 of Lemma bind-provision_wf

.....wf..... 
1. T : 𝕌'
2. S : 𝕌'
3. x : Provisional(T)
4. f : {t:T| allowed(x) ∧ (t = allow(x) ∈ T)}  ⟶ Provisional(S)
5. allowed(x) ∧ allowed(f[allow(x)]) ∈ Type
6. ∀[T:𝕌']. ∀[ok:ℙ]. ∀[v:T supposing ok].  (provision(ok; v) ∈ Provisional(T))
⊢ S ∈ 𝕌'
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  \mBbbU{}'
2.  S  :  \mBbbU{}'
3.  x  :  Provisional(T)
4.  f  :  \{t:T|  allowed(x)  \mwedge{}  (t  =  allow(x))\}    {}\mrightarrow{}  Provisional(S)
5.  allowed(x)  \mwedge{}  allowed(f[allow(x)])  \mmember{}  Type
6.  \mforall{}[T:\mBbbU{}'].  \mforall{}[ok:\mBbbP{}].  \mforall{}[v:T  supposing  ok].    (provision(ok;  v)  \mmember{}  Provisional(T))
\mvdash{}  S  \mmember{}  \mBbbU{}'


By

---

Latex:
Auto

---

Home Index