---

Step * 4 of Lemma rec-combined-class-opt-1-single-val0


1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. F : A ─→ B ─→ B
6. X : EClass(A)
7. init : Id ─→ bag(B)
8. e : E@i
9. ∀e':E
     ((e' < e)
     ⇒ (∀v1,v2:B.
           (single-valued-bag(init loc(e');B)
           ⇒ single-valued-classrel(es;X;A)
           ⇒ v2 ∈ lifting-2(F)|X,Prior(self)?init|(e')
           ⇒ v1 ∈ lifting-2(F)|X,Prior(self)?init|(e')
           ⇒ (v1 = v2 ∈ B))))
10. v1 : B@i
11. v2 : B@i
12. single-valued-bag(init loc(e);B)@i
13. single-valued-classrel(es;X;A)@i
14. a : A
15. b : B
16. v2 = (F a b) ∈ B
17. ∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ lifting-2(F)|X,Prior(self)?init|(e'))))
18. b ↓∈ init loc(e)
19. a ∈ X(e)
20. a1 : A
21. b1 : B
22. v1 = (F a1 b1) ∈ B
23. ∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ lifting-2(F)|X,Prior(self)?init|(e'))))
24. b1 ↓∈ init loc(e)
25. a1 ∈ X(e)
26. a = a1 ∈ A
⊢ b1 = b ∈ B
BY
{ (UseSingleVal (-9) (-3) THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  es  :  EO+(Info)
5.  F  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
6.  X  :  EClass(A)
7.  init  :  Id  {}\mrightarrow{}  bag(B)
8.  e  :  E@i
9.  \mforall{}e':E
          ((e'  <  e)
          {}\mRightarrow{}  (\mforall{}v1,v2:B.
                      (single-valued-bag(init  loc(e');B)
                      {}\mRightarrow{}  single-valued-classrel(es;X;A)
                      {}\mRightarrow{}  v2  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')
                      {}\mRightarrow{}  v1  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e')
                      {}\mRightarrow{}  (v1  =  v2))))
10.  v1  :  B@i
11.  v2  :  B@i
12.  single-valued-bag(init  loc(e);B)@i
13.  single-valued-classrel(es;X;A)@i
14.  a  :  A
15.  b  :  B
16.  v2  =  (F  a  b)
17.  \mforall{}e':E.  ((e'  <loc  e)  {}\mRightarrow{}  (\mforall{}w:B.  (\mneg{}w  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e'))))
18.  b  \mdownarrow{}\mmember{}  init  loc(e)
19.  a  \mmember{}  X(e)
20.  a1  :  A
21.  b1  :  B
22.  v1  =  (F  a1  b1)
23.  \mforall{}e':E.  ((e'  <loc  e)  {}\mRightarrow{}  (\mforall{}w:B.  (\mneg{}w  \mmember{}  lifting-2(F)|X,Prior(self)?init|(e'))))
24.  b1  \mdownarrow{}\mmember{}  init  loc(e)
25.  a1  \mmember{}  X(e)
26.  a  =  a1
\mvdash{}  b1  =  b


By

---

Latex:
(UseSingleVal  (-9)  (-3)  THEN  Auto)

---

Home Index