---

Step * 2 2 1 1 1 1 2 1 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. #(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)
BY
{ (All (Unfold `eclass`) THEN Auto) }

1
1. Info : Type
2. A : Type
3. u : es:EO+(Info) ⟶ e:E ⟶ bag(A)@i'
4. u1 : es:EO+(Info) ⟶ e:E ⟶ bag(A)
5. v : (es:EO+(Info) ⟶ e:E ⟶ bag(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
15. ¬False@i
⊢ single-valued-bag(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)

2
1. Info : Type
2. A : Type
3. u : es:EO+(Info) ⟶ e:E ⟶ bag(A)@i'
4. u1 : es:EO+(Info) ⟶ e:E ⟶ bag(A)
5. v : (es:EO+(Info) ⟶ e:E ⟶ bag(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
15. ¬False@i
16. single-valued-bag(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)
⊢ 0 < #(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))

---

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.  \#(u  es  e)  \mneq{}  1
10.  \muparrow{}e  \mmember{}\msubb{}  first-eclass([u;  [u1  /  v]])
11.  (\mexists{}X\mmember{}[u1  /  v].  \muparrow{}e  \mmember{}\msubb{}  X)
12.  i  :  \mBbbN{}||[u1  /  v]||
13.  \muparrow{}e  \mmember{}\msubb{}  [u1  /  v][i]
14.  first-eclass([u1  /  v])(e)  =  [u1  /  v][i](e)
\mvdash{}  (\mneg{}False)
{}\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:
                    u1  es  e))
      =  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:
(All  (Unfold  `eclass`)  THEN  Auto)

---

Home Index