---

Step * 1 1 1 of Lemma has-value-try


1. t : Base
2. n : Base
3. B : Base
4. (if n=2 n
     then t
     else ⊥)↓
5. (t)↓
6. t?n:v.B[v] ~ if n=2 n
                 then t
                 else ⊥
⊢ (t)↓ ∧ (t?n:v.B[v] ~ t)
BY
{ HasValueD (-3)⋅ }

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

---

Latex:

---

Latex:

1.  t  :  Base
2.  n  :  Base
3.  B  :  Base
4.  (if  n=2  n
          then  t
          else  \mbot{})\mdownarrow{}
5.  (t)\mdownarrow{}
6.  t?n:v.B[v]  \msim{}  if  n=2  n
                                  then  t
                                  else  \mbot{}
\mvdash{}  (t)\mdownarrow{}  \mwedge{}  (t?n:v.B[v]  \msim{}  t)


By

---

Latex:
HasValueD  (-3)\mcdot{}

---

Home Index