---

Step * 1 1 of Lemma eclass-ext-classrel


1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. ∀es:EO+(Info). ∀e:E.  ((#(X es e) ≤ 1) ∧ (#(Y es e) ≤ 1))
6. ∀es:EO+(Info). ∀e:E. ∀v:T.  (v ∈ X(e) ⇐⇒ v ∈ Y(e))
7. es : EO+(Info)@i'
8. e : E@i
9. ((X es e) = {} ∈ bag(T)) ⇒ ((Y es e) = {} ∈ bag(T))
10. ((X es e) = {} ∈ bag(T)) ⇐ (Y es e) = {} ∈ bag(T)
11. #(X es e) = 1 ∈ ℤ@i
12. #(Y es e) = 1 ∈ ℤ@i
13. Y es e ~ {only(Y es e)}
14. x : T@i
15. only(Y es e) = x ∈ T@i
16. X es e ~ {only(X es e)}
17. x1 : T@i
18. only(X es e) = x1 ∈ T@i
⊢ only(X es e) = x ∈ T
BY
{ (Assert x ∈ X(e) BY
         ((InstHyp [⌈es⌉;⌈e⌉;⌈x⌉] 6⋅ THENA Auto)
          THEN RepeatFor 2 (D (-1))
          THEN Auto
          THEN ((SubstFor  ⌈x⌉ 0⋅ THEN Auto THEN Unfold `classrel` 0)
                THEN HypSubst 13 0⋅
                THEN Reduce 0
                THEN BagMemberD 0
                THEN Auto)⋅))⋅ }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. ∀es:EO+(Info). ∀e:E.  ((#(X es e) ≤ 1) ∧ (#(Y es e) ≤ 1))
6. ∀es:EO+(Info). ∀e:E. ∀v:T.  (v ∈ X(e) ⇐⇒ v ∈ Y(e))
7. es : EO+(Info)@i'
8. e : E@i
9. ((X es e) = {} ∈ bag(T)) ⇒ ((Y es e) = {} ∈ bag(T))
10. ((X es e) = {} ∈ bag(T)) ⇐ (Y es e) = {} ∈ bag(T)
11. #(X es e) = 1 ∈ ℤ@i
12. #(Y es e) = 1 ∈ ℤ@i
13. Y es e ~ {only(Y es e)}
14. x : T@i
15. only(Y es e) = x ∈ T@i
16. X es e ~ {only(X es e)}
17. x1 : T@i
18. only(X es e) = x1 ∈ T@i
19. x ∈ X(e)
⊢ only(X es e) = x ∈ T

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  X  :  EClass(T)
4.  Y  :  EClass(T)
5.  \mforall{}es:EO+(Info).  \mforall{}e:E.    ((\#(X  es  e)  \mleq{}  1)  \mwedge{}  (\#(Y  es  e)  \mleq{}  1))
6.  \mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}v:T.    (v  \mmember{}  X(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  Y(e))
7.  es  :  EO+(Info)@i'
8.  e  :  E@i
9.  ((X  es  e)  =  \{\})  {}\mRightarrow{}  ((Y  es  e)  =  \{\})
10.  ((X  es  e)  =  \{\})  \mLeftarrow{}{}  (Y  es  e)  =  \{\}
11.  \#(X  es  e)  =  1@i
12.  \#(Y  es  e)  =  1@i
13.  Y  es  e  \msim{}  \{only(Y  es  e)\}
14.  x  :  T@i
15.  only(Y  es  e)  =  x@i
16.  X  es  e  \msim{}  \{only(X  es  e)\}
17.  x1  :  T@i
18.  only(X  es  e)  =  x1@i
\mvdash{}  only(X  es  e)  =  x


By

(Assert  x  \mmember{}  X(e)  BY
              ((InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
                THEN  RepeatFor  2  (D  (-1))
                THEN  Auto
                THEN  ((SubstFor    \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}  THEN  Auto  THEN  Unfold  `classrel`  0)
                            THEN  HypSubst  13  0\mcdot{}
                            THEN  Reduce  0
                            THEN  BagMemberD  0
                            THEN  Auto)\mcdot{}))\mcdot{}

---

Home Index