---

Step * 1 2 1 1 of Lemma first-class-val

.....falsecase..... 
1. Info : Type
2. A : Type
3. u : EClass(A)@i'
4. v : EClass(A) List@i'
5. ∀es:EO+(Info). ∀e:E.
     ((↑e ∈b first-class(v))
     ⇒ ((↑e ∈b v[index-of-first X in v.e ∈b X - 1])
        ∧ (first-class(v)(e) = v[index-of-first X in v.e ∈b X - 1](e) ∈ A)))@i'
6. es : EO+(Info)@i'
7. ∀e:E
     ((↑e ∈b first-class(v))
     ⇒ ((↑e ∈b v[index-of-first X in v.e ∈b X - 1])
        ∧ (first-class(v)(e) = v[index-of-first X in v.e ∈b X - 1](e) ∈ A)))
8. e : E@i
9. (↑e ∈b first-class(v))
⇒ ((↑e ∈b v[index-of-first X in v.e ∈b X - 1]) ∧ (first-class(v)(e) = v[index-of-first X in v.e ∈b X - 1](e) ∈ A))
10. ↑e ∈b [u?first-class(v)]@i
11. [u?first-class(v)](e) = first-class(v)(e) ∈ A
12. ¬↑e ∈b u
13. ¬↑e ∈b u
⊢ (↑e ∈b [u / v][if 0 <z index-of-first X in v.e ∈b X then index-of-first X in v.e ∈b X + 1 else 0 fi  - 1])
∧ ([u?first-class(v)](e)
  = [u / v][if 0 <z index-of-first X in v.e ∈b X then index-of-first X in v.e ∈b X + 1 else 0 fi  - 1](e)
  ∈ A)
BY
{ (DupHyp (-4) THEN (RWO "is-cond-class" (-1) THENA Auto) THEN D -1 THEN Try (Trivial) THEN ThinTrivial) }

1
1. Info : Type
2. A : Type
3. u : EClass(A)@i'
4. v : EClass(A) List@i'
5. ∀es:EO+(Info). ∀e:E.
     ((↑e ∈b first-class(v))
     ⇒ ((↑e ∈b v[index-of-first X in v.e ∈b X - 1])
        ∧ (first-class(v)(e) = v[index-of-first X in v.e ∈b X - 1](e) ∈ A)))@i'
6. es : EO+(Info)@i'
7. ∀e:E
     ((↑e ∈b first-class(v))
     ⇒ ((↑e ∈b v[index-of-first X in v.e ∈b X - 1])
        ∧ (first-class(v)(e) = v[index-of-first X in v.e ∈b X - 1](e) ∈ A)))
8. e : E@i
9. ↑e ∈b [u?first-class(v)]@i
10. [u?first-class(v)](e) = first-class(v)(e) ∈ A
11. ¬↑e ∈b u
12. ¬↑e ∈b u
13. ↑e ∈b first-class(v)
14. (↑e ∈b v[index-of-first X in v.e ∈b X - 1]) ∧ (first-class(v)(e) = v[index-of-first X in v.e ∈b X - 1](e) ∈ A)
⊢ (↑e ∈b [u / v][if 0 <z index-of-first X in v.e ∈b X then index-of-first X in v.e ∈b X + 1 else 0 fi  - 1])
∧ ([u?first-class(v)](e)
  = [u / v][if 0 <z index-of-first X in v.e ∈b X then index-of-first X in v.e ∈b X + 1 else 0 fi  - 1](e)
  ∈ A)

---

Latex:

---

Latex:
.....falsecase..... 
1.  Info  :  Type
2.  A  :  Type
3.  u  :  EClass(A)@i'
4.  v  :  EClass(A)  List@i'
5.  \mforall{}es:EO+(Info).  \mforall{}e:E.
          ((\muparrow{}e  \mmember{}\msubb{}  first-class(v))
          {}\mRightarrow{}  ((\muparrow{}e  \mmember{}\msubb{}  v[index-of-first  X  in  v.e  \mmember{}\msubb{}  X  -  1])
                \mwedge{}  (first-class(v)(e)  =  v[index-of-first  X  in  v.e  \mmember{}\msubb{}  X  -  1](e))))@i'
6.  es  :  EO+(Info)@i'
7.  \mforall{}e:E
          ((\muparrow{}e  \mmember{}\msubb{}  first-class(v))
          {}\mRightarrow{}  ((\muparrow{}e  \mmember{}\msubb{}  v[index-of-first  X  in  v.e  \mmember{}\msubb{}  X  -  1])
                \mwedge{}  (first-class(v)(e)  =  v[index-of-first  X  in  v.e  \mmember{}\msubb{}  X  -  1](e))))
8.  e  :  E@i
9.  (\muparrow{}e  \mmember{}\msubb{}  first-class(v))
{}\mRightarrow{}  ((\muparrow{}e  \mmember{}\msubb{}  v[index-of-first  X  in  v.e  \mmember{}\msubb{}  X  -  1])
      \mwedge{}  (first-class(v)(e)  =  v[index-of-first  X  in  v.e  \mmember{}\msubb{}  X  -  1](e)))
10.  \muparrow{}e  \mmember{}\msubb{}  [u?first-class(v)]@i
11.  [u?first-class(v)](e)  =  first-class(v)(e)
12.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  u
13.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  u
\mvdash{}  (\muparrow{}e  \mmember{}\msubb{}  [u  /  v][if  0  <z  index-of-first  X  in  v.e  \mmember{}\msubb{}  X
                  then  index-of-first  X  in  v.e  \mmember{}\msubb{}  X  +  1
                  else  0
                  fi    -  1])
\mwedge{}  ([u?first-class(v)](e)
    =  [u  /  v][if  0  <z  index-of-first  X  in  v.e  \mmember{}\msubb{}  X  then  index-of-first  X  in  v.e  \mmember{}\msubb{}  X  +  1  else  0  fi   
        -  1](e))


By

---

Latex:
(DupHyp  (-4)
  THEN  (RWO  "is-cond-class"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  Try  (Trivial)
  THEN  ThinTrivial)

---

Home Index