---

Step * 1 3 1 1 1 2 of Lemma prior-or-latest


1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. Singlevalued(Y)
8. ∀es:EO+(Info). ∀e:E.  (↑e ∈b ((X |- Y))' ⇐⇒ ↑e ∈b ((X)' | (Y)'))
9. es : EO+(Info)@i'
10. e : E@i
11. ↑e ∈b ((X |- Y))'@i
12. ↑e ∈b ((X)' | (Y)')@i
13. ↑e ∈b ((X |- Y))'
14. e' : E
15. (e' <loc e)
16. ↑e' ∈b (X |- Y)
17. ∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑e'' ∈b (X |- Y)))
18. ((X |- Y))'(e) = (X |- Y)(e') ∈ one_or_both(A;B)
19. ((X)' es e) = ((X)- es e') ∈ bag(A)
20. ((Y)' es e) = ((Y)- es e') ∈ bag(B)
⊢ if e' ∈b (X)- then if e' ∈b (Y)- then oobboth(<(X)-(e'), (Y)-(e')>) else oobleft((X)-(e')) fi  else oobright((Y)-(e'))\000C fi 
= if e ∈b (X)' then if e ∈b (Y)' then oobboth(<(X)'(e), (Y)'(e)>) else oobleft((X)'(e)) fi  else oobright((Y)'(e)) fi 
∈ one_or_both(A;B)
BY
{ RepUR ``in-eclass eclass-val can-apply do-apply`` 0 }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. Singlevalued(Y)
8. ∀es:EO+(Info). ∀e:E.  (↑e ∈b ((X |- Y))' ⇐⇒ ↑e ∈b ((X)' | (Y)'))
9. es : EO+(Info)@i'
10. e : E@i
11. ↑e ∈b ((X |- Y))'@i
12. ↑e ∈b ((X)' | (Y)')@i
13. ↑e ∈b ((X |- Y))'
14. e' : E
15. (e' <loc e)
16. ↑e' ∈b (X |- Y)
17. ∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑e'' ∈b (X |- Y)))
18. ((X |- Y))'(e) = (X |- Y)(e') ∈ one_or_both(A;B)
19. ((X)' es e) = ((X)- es e') ∈ bag(A)
20. ((Y)' es e) = ((Y)- es e') ∈ bag(B)
⊢ if (#((X)- es e') =z 1)
then if (#((Y)- es e') =z 1) then oobboth(<only((X)- es e'), only((Y)- es e')>) else oobleft(only((X)- es e')) fi 
else oobright(only((Y)- es e'))
fi 
= if (#((X)' es e) =z 1)
  then if (#((Y)' es e) =z 1) then oobboth(<only((X)' es e), only((Y)' es e)>) else oobleft(only((X)' es e)) fi 
  else oobright(only((Y)' es e))
  fi 
∈ one_or_both(A;B)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  X  :  EClass(A)
5.  Y  :  EClass(B)
6.  Singlevalued(X)
7.  Singlevalued(Y)
8.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  ((X  |\msupminus{}  Y))'  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  ((X)'  |  (Y)'))
9.  es  :  EO+(Info)@i'
10.  e  :  E@i
11.  \muparrow{}e  \mmember{}\msubb{}  ((X  |\msupminus{}  Y))'@i
12.  \muparrow{}e  \mmember{}\msubb{}  ((X)'  |  (Y)')@i
13.  \muparrow{}e  \mmember{}\msubb{}  ((X  |\msupminus{}  Y))'
14.  e'  :  E
15.  (e'  <loc  e)
16.  \muparrow{}e'  \mmember{}\msubb{}  (X  |\msupminus{}  Y)
17.  \mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}e''  \mmember{}\msubb{}  (X  |\msupminus{}  Y)))
18.  ((X  |\msupminus{}  Y))'(e)  =  (X  |\msupminus{}  Y)(e')
19.  ((X)'  es  e)  =  ((X)\msupminus{}  es  e')
20.  ((Y)'  es  e)  =  ((Y)\msupminus{}  es  e')
\mvdash{}  if  e'  \mmember{}\msubb{}  (X)\msupminus{}
then  if  e'  \mmember{}\msubb{}  (Y)\msupminus{}  then  oobboth(<(X)\msupminus{}(e'),  (Y)\msupminus{}(e')>)  else  oobleft((X)\msupminus{}(e'))  fi 
else  oobright((Y)\msupminus{}(e'))
fi 
=  if  e  \mmember{}\msubb{}  (X)'
    then  if  e  \mmember{}\msubb{}  (Y)'  then  oobboth(<(X)'(e),  (Y)'(e)>)  else  oobleft((X)'(e))  fi 
    else  oobright((Y)'(e))
    fi 


By

---

Latex:
RepUR  ``in-eclass  eclass-val  can-apply  do-apply``  0

---

Home Index