---

Step * of Lemma try-is-exception

∀[t,n,B,m,x:Base].
  exception(m; x) ≤ t?n:v.B[v] 
  supposing ↓((n ∈ Atom2)
             ∧ (((m ∈ Atom2) ∧ (exception(m; x) ≤ t) ∧ (¬(n = m ∈ Atom2)))
               ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (exception(m; x) ≤ B[u])))))
             ∨ ((t)↓ ∧ (exception(m; x) ≤ n))
BY
{ (Intros
   THEN (Unhide THENA Auto)
   THEN (D -1 THEN (Unhide THENA Auto))
   THEN RepeatFor 2 (D -1)
   THEN Try ((D -1 THEN ExRepD))) }

1
1. t : Base
2. n : Base
3. B : Base
4. m : Base
5. x : Base
6. n ∈ Atom2
7. m ∈ Atom2
8. exception(m; x) ≤ t
9. ¬(n = m ∈ Atom2)
⊢ exception(m; x) ≤ t?n:v.B[v]

2
1. t : Base
2. n : Base
3. B : Base
4. m : Base
5. x : Base
6. n ∈ Atom2
7. u : Base
8. t ~ exception(n; u)
9. exception(m; x) ≤ B[u]
⊢ exception(m; x) ≤ t?n:v.B[v]

3
1. t : Base
2. n : Base
3. B : Base
4. m : Base
5. x : Base
6. (t)↓
7. exception(m; x) ≤ n
⊢ exception(m; x) ≤ t?n:v.B[v]

---

Latex:

---

Latex:
\mforall{}[t,n,B,m,x:Base].
    exception(m;  x)  \mleq{}  t?n:v.B[v] 
    supposing  \mdownarrow{}((n  \mmember{}  Atom2)
                          \mwedge{}  (((m  \mmember{}  Atom2)  \mwedge{}  (exception(m;  x)  \mleq{}  t)  \mwedge{}  (\mneg{}(n  =  m)))
                              \mvee{}  (\mexists{}u:Base.  ((t  \msim{}  exception(n;  u))  \mwedge{}  (exception(m;  x)  \mleq{}  B[u])))))
                          \mvee{}  ((t)\mdownarrow{}  \mwedge{}  (exception(m;  x)  \mleq{}  n))


By

---

Latex:
(Intros
  THEN  (Unhide  THENA  Auto)
  THEN  (D  -1  THEN  (Unhide  THENA  Auto))
  THEN  RepeatFor  2  (D  -1)
  THEN  Try  ((D  -1  THEN  ExRepD)))

---

Home Index