---

Step * of Lemma has-value-try-iff

∀[t,n,B:Base].
  uiff((t?n:v.B[v])↓;↓((t)↓ ∧ (t?n:v.B[v] ~ t)) ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓)))
BY
{ (Auto THEN Try ((BLemma  `has-value-try` THEN Auto))) }

1
1. t : Base
2. n : Base
3. B : Base
4. ↓((t)↓ ∧ (t?n:v.B[v] ~ t)) ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓))
⊢ (t?n:v.B[v])↓

---

Latex:

---

Latex:
\mforall{}[t,n,B:Base].
    uiff((t?n:v.B[v])\mdownarrow{};\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{})))


By

---

Latex:
(Auto  THEN  Try  ((BLemma    `has-value-try`  THEN  Auto)))

---

Home Index