---

Step * 1 1 of Lemma has-value-try


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)
BY
{ (D -1 THEN RWO  "-1" (-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 ⊥
⊢ (t)↓ ∧ (t?n:v.B[v] ~ t)

---

Latex:

---

Latex:

1.  t  :  Base
2.  n  :  Base
3.  B  :  Base
4.  (t?n:v.B[v])\mdownarrow{}
5.  (t)\mdownarrow{}  \mwedge{}  (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:
(D  -1  THEN  RWO    "-1"  (-3))

---

Home Index