---

Step * 1 of Lemma bind-provision_wf


1. T : 𝕌'
2. S : 𝕌'
3. x : Provisional(T)
4. f : {t:T| allowed(x) ∧ (t = allow(x) ∈ T)}  ⟶ Provisional(S)
⊢ provision(allowed(x) ∧ allowed(f[allow(x)]); allow(f[allow(x)])) ∈ Provisional(S)
BY
{ ProvisionCD }

1
.....aux..... 
1. T : 𝕌'
2. S : 𝕌'
3. x : Provisional(T)
4. f : {t:T| allowed(x) ∧ (t = allow(x) ∈ T)}  ⟶ Provisional(S)
⊢ allowed(x) ∧ allowed(f[allow(x)]) ∈ Type

2
.....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 ∈ 𝕌'

3
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))
7. allowed(x) ∧ allowed(f[allow(x)])
⊢ allow(f[allow(x)]) ∈ S

---

Latex:

---

Latex:

1.  T  :  \mBbbU{}'
2.  S  :  \mBbbU{}'
3.  x  :  Provisional(T)
4.  f  :  \{t:T|  allowed(x)  \mwedge{}  (t  =  allow(x))\}    {}\mrightarrow{}  Provisional(S)
\mvdash{}  provision(allowed(x)  \mwedge{}  allowed(f[allow(x)]);  allow(f[allow(x)]))  \mmember{}  Provisional(S)


By

---

Latex:
ProvisionCD

---

Home Index