---

Step * 1 of Lemma first-class-val


1. Info : Type
2. A : Type
3. L : EClass(A) List
4. es : EO+(Info)
5. e : E
6. ↑e ∈b first-class(L)
⊢ (↑e ∈b L[index-of-first X in L.e ∈b X - 1]) ∧ (first-class(L)(e) = L[index-of-first X in L.e ∈b X - 1](e) ∈ A)
BY
{ (RepeatFor 3 (MoveToConcl (-1))
   THEN ListInd' (-1)
   THEN Try ((Unfold `first-class` 0
              THEN (RW (AddrC [2;2;1] ReduceC) 0 THEN Try (Complete (Auto)))
              THEN Reduce 0
              THEN Fold `first-class` 0
              THEN RepeatFor 2 (ParallelLast)))) }

1
.....wf..... 
1. Info : Type
2. A : Type
⊢ λL.∀es:EO+(Info). ∀e:E.
       ((↑e ∈b first-class(L))
       ⇒ ((↑e ∈b L[index-of-first X in L.e ∈b X - 1])
          ∧ (first-class(L)(e) = L[index-of-first X in L.e ∈b X - 1](e) ∈ A))) ∈ (EClass(A) List) ─→ ℙ'

2
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))
⊢ (↑e ∈b [u?first-class(v)])
⇒ ((↑e ∈b [u / v][index-of-first X in [u / v].e ∈b X - 1])
   ∧ ([u?first-class(v)](e) = [u / v][index-of-first X in [u / v].e ∈b X - 1](e) ∈ A))

3
.....wf..... 
1. Info : Type
2. A : Type
3. u : EClass(A)@i'
4. v : EClass(A) List@i'
⊢ ∀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)))
  ∈ ℙ'

---

Latex:



1.  Info  :  Type
2.  A  :  Type
3.  L  :  EClass(A)  List
4.  es  :  EO+(Info)
5.  e  :  E
6.  \muparrow{}e  \mmember{}\msubb{}  first-class(L)
\mvdash{}  (\muparrow{}e  \mmember{}\msubb{}  L[index-of-first  X  in  L.e  \mmember{}\msubb{}  X  -  1])
\mwedge{}  (first-class(L)(e)  =  L[index-of-first  X  in  L.e  \mmember{}\msubb{}  X  -  1](e))


By

(RepeatFor  3  (MoveToConcl  (-1))
  THEN  ListInd'  (-1)
  THEN  Try  ((Unfold  `first-class`  0
                        THEN  (RW  (AddrC  [2;2;1]  ReduceC)  0  THEN  Try  (Complete  (Auto)))
                        THEN  Reduce  0
                        THEN  Fold  `first-class`  0
                        THEN  RepeatFor  2  (ParallelLast))))

---

Home Index