---

Step * 1 3 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)
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
BY
{ (D -1 THEN MemCD THEN Try (Trivial)) }

1
.....subterm..... T:t
1:n
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)
8. allowed(f[allow(x)])
⊢ f[allow(x)] ∈ Provisional(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)
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))
7.  allowed(x)  \mwedge{}  allowed(f[allow(x)])
\mvdash{}  allow(f[allow(x)])  \mmember{}  S


By

---

Latex:
(D  -1  THEN  MemCD  THEN  Try  (Trivial))

---

Home Index