---

Step * 2 1 of Lemma prior-imax-class-lb2


1. Info : Type
2. es : EO+(Info)
3. e : E
4. n : ℕ
5. A : Type
6. f : A ─→ ℕ
7. Z : EClass(A)
8. ¬↑e ∈b ((maximum f[x] ≥ 0 with x from Z))'
9. ¬↑e ∈b Z
10. (-1) ≤ n
11. e' : E(Z)
12. (e' <loc e)
⊢ f[Z(e')] ≤ n
BY
{ OnMaybeHyp 7 (\h. (D h
                     THEN BLemma `is-prior-val`
                     THEN Auto
                     THEN With ⌈e'⌉ (D 0)⋅
                     THEN Auto
                     THEN RWO "is-imax-class" 0 
                     THEN Auto)) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e  :  E
4.  n  :  \mBbbN{}
5.  A  :  Type
6.  f  :  A  {}\mrightarrow{}  \mBbbN{}
7.  Z  :  EClass(A)
8.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  ((maximum  f[x]  \mgeq{}  0  with  x  from  Z))'
9.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Z
10.  (-1)  \mleq{}  n
11.  e'  :  E(Z)
12.  (e'  <loc  e)
\mvdash{}  f[Z(e')]  \mleq{}  n


By

---

Latex:
OnMaybeHyp  7  (\mbackslash{}h.  (D  h
                                      THEN  BLemma  `is-prior-val`
                                      THEN  Auto
                                      THEN  With  \mkleeneopen{}e'\mkleeneclose{}  (D  0)\mcdot{}
                                      THEN  Auto
                                      THEN  RWO  "is-imax-class"  0 
                                      THEN  Auto))

---

Home Index