---

Step * 1 3 1 1 1 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)
⊢ (X |- Y)(e') = ((X)' | (Y)')(e) ∈ one_or_both(A;B)
BY
{ (RWW "or-latest-val interface-or-val" 0 THENA Auto)⋅ }

1
.....rewrite subgoal..... 
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)
⊢ ↑e' ∈b ((X)- | (Y)-)

2
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)

---

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{}  (X  |\msupminus{}  Y)(e')  =  ((X)'  |  (Y)')(e)


By

---

Latex:
(RWW  "or-latest-val  interface-or-val"  0  THENA  Auto)\mcdot{}

---

Home Index