---

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


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)
BY
{ AutoSplit }

1
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. #(u es e) ≠ 1
10. ↑e ∈b first-eclass([u; [u1 / v]])
11. (∃X∈[u1 / v]. ↑e ∈b X)
12. i : ℕ||[u1 / v]||
13. ↑e ∈b [u1 / v][i]
14. first-eclass([u1 / v])(e) = [u1 / v][i](e) ∈ A
⊢ (¬False)
⇒ (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))
   = 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:

1.  Info  :  Type
2.  A  :  Type
3.  u  :  EClass(A)@i'
4.  u1  :  EClass(A)
5.  v  :  EClass(A)  List
6.  \mforall{}es:EO+(Info).  \mforall{}e:E.
          (\mexists{}X\mmember{}[u1  /  v].  (\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (first-eclass([u1  /  v])(e)  =  X(e))) 
          supposing  \muparrow{}e  \mmember{}\msubb{}  first-eclass([u1  /  v])@i'
7.  es  :  EO+(Info)@i'
8.  e  :  E@i
9.  \muparrow{}e  \mmember{}\msubb{}  first-eclass([u;  [u1  /  v]])
10.  (\mexists{}X\mmember{}[u1  /  v].  \muparrow{}e  \mmember{}\msubb{}  X)
11.  i  :  \mBbbN{}||[u1  /  v]||
12.  \muparrow{}e  \mmember{}\msubb{}  [u1  /  v][i]
13.  first-eclass([u1  /  v])(e)  =  [u1  /  v][i](e)
\mvdash{}  (\mneg{}\muparrow{}(\#(u  es  e)  =\msubz{}  1))
{}\mRightarrow{}  (only(accumulate  (with  value  b  and  list  item  X):
                    if  (\#(b)  =\msubz{}  1)  then  b  else  X  es  e  fi 
                  over  list:
                      v
                  with  starting  value:
                    if  (\#(u  es  e)  =\msubz{}  1)  then  u  es  e  else  u1  es  e  fi  ))
      =  only(accumulate  (with  value  b  and  list  item  X):
                      if  (\#(b)  =\msubz{}  1)  then  b  else  X  es  e  fi 
                    over  list:
                        v
                    with  starting  value:
                      u1  es  e)))


By

---

Latex:
AutoSplit

---

Home Index