---

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


1. Info : Type
2. A : Type
3. u : es:EO+(Info) ─→ e:E ─→ bag(A)@i'
4. es : EO+(Info)@i'
5. e : E@i
6. u1 : es:EO+(Info) ─→ e:E ─→ bag(A)
7. v : (es:EO+(Info) ─→ e:E ─→ bag(A)) List
8. (↑(#(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:
          u es e))
   = only(u es 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(u es e)
   ∈ A)
BY
{ (AutoSplit THEN D -2 THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  u  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A)@i'
4.  es  :  EO+(Info)@i'
5.  e  :  E@i
6.  u1  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A)
7.  v  :  (es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A))  List
8.  (\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:
                    u  es  e))
      =  only(u  es  e))
\mvdash{}  (\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(u  es  e))


By

---

Latex:
(AutoSplit  THEN  D  -2  THEN  Auto)

---

Home Index