---

Step * 1 of Lemma has-value-try


1. ∀[t,n,B:Base].
     ↓((t)↓ ∧ (t?n:v.B[v] ~ if n=2 n then t else ⊥))
      ∨ (∃m,u:Base. ((t ~ exception(m; u)) ∧ (t?n:v.B[v] ~ if n=2 m then B[u] else (exception(m; u))))) 
     supposing (t?n:v.B[v])↓
⊢ ∀[t,n,B:Base].
    ↓((t)↓ ∧ (t?n:v.B[v] ~ t)) ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓)) 
    supposing (t?n:v.B[v])↓
BY
{ RepeatFor 6 (ParallelLast') }

1
1. t : Base
2. n : Base
3. B : Base
4. (t?n:v.B[v])↓
5. (t)↓ ∧ (t?n:v.B[v] ~ if n=2 n then t else ⊥)
⊢ (t)↓ ∧ (t?n:v.B[v] ~ t)

2
1. t : Base
2. n : Base
3. B : Base
4. (t?n:v.B[v])↓
5. ∃m,u:Base. ((t ~ exception(m; u)) ∧ (t?n:v.B[v] ~ if n=2 m then B[u] else (exception(m; u))))
⊢ ∃u:Base. ((t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓)

---

Latex:

---

Latex:

1.  \mforall{}[t,n,B:Base].
          \mdownarrow{}((t)\mdownarrow{}  \mwedge{}  (t?n:v.B[v]  \msim{}  if  n=2  n  then  t  else  \mbot{}))
            \mvee{}  (\mexists{}m,u:Base
                    ((t  \msim{}  exception(m;  u))  \mwedge{}  (t?n:v.B[v]  \msim{}  if  n=2  m  then  B[u]  else  (exception(m;  u))))) 
          supposing  (t?n:v.B[v])\mdownarrow{}
\mvdash{}  \mforall{}[t,n,B:Base].
        \mdownarrow{}((t)\mdownarrow{}  \mwedge{}  (t?n:v.B[v]  \msim{}  t))  \mvee{}  (\mexists{}u:Base.  ((t  \msim{}  exception(n;  u))  \mwedge{}  (t?n:v.B[v]  \msim{}  B[u])  \mwedge{}  (B[u])\mdownarrow{})) 
        supposing  (t?n:v.B[v])\mdownarrow{}


By

---

Latex:
RepeatFor  6  (ParallelLast')

---

Home Index