---

Step * 1 3 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)
⊢ (X |- Y)(e') = ((X)' | (Y)')(e) ∈ one_or_both(A;B)
BY
{ (Assert ((X)' es e) = ((X)- es e') ∈ bag(A) BY
         (BLemma `prior-val-as-latest-val` 
          THEN Auto
               THEN (Assert ¬↑e'' ∈b (X |- Y) BY
                           BackThruSomeHyp
                           THEN Auto)
               THEN ParallelLast
               THEN BLemma `is-or-latest`
               THEN Auto
          ))⋅ }

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


By

---

Latex:
(Assert  ((X)'  es  e)  =  ((X)\msupminus{}  es  e')  BY
              (BLemma  `prior-val-as-latest-val` 
                THEN  Auto
                          THEN  (Assert  \mneg{}\muparrow{}e''  \mmember{}\msubb{}  (X  |\msupminus{}  Y)  BY
                                                  BackThruSomeHyp
                                                  THEN  Auto)
                          THEN  ParallelLast
                          THEN  BLemma  `is-or-latest`
                          THEN  Auto
                ))\mcdot{}

---

Home Index