---

Step * of Lemma rec-value-evalall

∀[x:Base]. uiff((evalall(x))↓;x ∈ rec-value())
BY
{ Auto }

1
1. x : Base
2. (evalall(x))↓
⊢ x ∈ rec-value()

2
1. x : Base
2. x ∈ rec-value()
⊢ (evalall(x))↓

---

Latex:

---

Latex:
\mforall{}[x:Base].  uiff((evalall(x))\mdownarrow{};x  \mmember{}  rec-value())


By

---

Latex:
Auto

---

Home Index