---

Step * 1 2 of Lemma has-value-try


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])↓)
BY
{ (D -1 THEN ParallelLast THEN D -1) }

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

---

Latex:

---

Latex:

1.  t  :  Base
2.  n  :  Base
3.  B  :  Base
4.  (t?n:v.B[v])\mdownarrow{}
5.  \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))))
\mvdash{}  \mexists{}u:Base.  ((t  \msim{}  exception(n;  u))  \mwedge{}  (t?n:v.B[v]  \msim{}  B[u])  \mwedge{}  (B[u])\mdownarrow{})


By

---

Latex:
(D  -1  THEN  ParallelLast  THEN  D  -1)

---

Home Index