---

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

.....subterm..... T:t
2:n
1. Info : Type
2. A : Type
3. u : EClass(A)@i'
4. v : EClass(A) List@i'
5. ∀es:EO+(Info). ∀e:E.  (∃X∈v. (↑e ∈b X) ∧ (first-eclass(v)(e) = X(e) ∈ A)) supposing ↑e ∈b first-eclass(v)@i'
6. es : EO+(Info)@i'
7. e : E@i
8. ↑e ∈b first-eclass([u / v])
9. (∃X∈v. ↑e ∈b X)
10. ¬↑e ∈b u
11. i : ℕ||v||
12. ↑e ∈b v[i]
13. first-eclass(v)(e) = v[i](e) ∈ A
⊢ first-eclass([u / v])(e) = first-eclass(v)(e) ∈ A
BY
{ (MoveToConcl (-4) THEN RepUR ``first-eclass in-eclass can-apply eclass-val do-apply`` 0 THEN DVar `v' THEN Reduce 0)
⋅ }

1
1. Info : Type
2. A : Type
3. u : EClass(A)@i'
4. ∀es:EO+(Info). ∀e:E.  (∃X∈[]. (↑e ∈b X) ∧ (first-eclass([])(e) = X(e) ∈ A)) supposing ↑e ∈b first-eclass([])@i'
5. es : EO+(Info)@i'
6. e : E@i
7. ↑e ∈b first-eclass([u])
8. (∃X∈[]. ↑e ∈b X)
9. i : ℕ||[]||
10. ↑e ∈b [][i]
11. first-eclass([])(e) = [][i](e) ∈ A
⊢ (¬↑(#(u es e) =z 1)) ⇒ (only(u es e) = only({}) ∈ A)

2
1. Info : Type
2. A : Type
3. u : EClass(A)@i'
4. u1 : EClass(A)
5. v : EClass(A) List
6. ∀es:EO+(Info). ∀e:E.
     (∃X∈[u1 / v]. (↑e ∈b X) ∧ (first-eclass([u1 / v])(e) = X(e) ∈ A)) supposing ↑e ∈b first-eclass([u1 / v])@i'
7. es : EO+(Info)@i'
8. e : E@i
9. ↑e ∈b first-eclass([u; [u1 / v]])
10. (∃X∈[u1 / v]. ↑e ∈b X)
11. i : ℕ||[u1 / v]||
12. ↑e ∈b [u1 / v][i]
13. first-eclass([u1 / v])(e) = [u1 / v][i](e) ∈ A
⊢ (¬↑(#(u es e) =z 1))
⇒ (only(accumulate (with value b and list item X):
          if (#(b) =z 1) then b else X es e fi 
         over list:
           v
         with starting value:
          if (#(u es e) =z 1) then u es e else u1 es e fi ))
   = only(accumulate (with value b and list item X):
           if (#(b) =z 1) then b else X es e fi 
          over list:
            v
          with starting value:
           u1 es e))
   ∈ A)

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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.
          (\mexists{}X\mmember{}v.  (\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (first-eclass(v)(e)  =  X(e)))  supposing  \muparrow{}e  \mmember{}\msubb{}  first-eclass(v)@i'
6.  es  :  EO+(Info)@i'
7.  e  :  E@i
8.  \muparrow{}e  \mmember{}\msubb{}  first-eclass([u  /  v])
9.  (\mexists{}X\mmember{}v.  \muparrow{}e  \mmember{}\msubb{}  X)
10.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  u
11.  i  :  \mBbbN{}||v||
12.  \muparrow{}e  \mmember{}\msubb{}  v[i]
13.  first-eclass(v)(e)  =  v[i](e)
\mvdash{}  first-eclass([u  /  v])(e)  =  first-eclass(v)(e)


By

---

Latex:
(MoveToConcl  (-4)
  THEN  RepUR  ``first-eclass  in-eclass  can-apply  eclass-val  do-apply``  0
  THEN  DVar  `v'
  THEN  Reduce  0)\mcdot{}

---

Home Index