---

Step * of Lemma primed-class-opt-single-val0

∀[Info,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(B)]. ∀[init:Id ─→ bag(B)].
  ∀e:E. ∀v1,v2:B.
    (single-valued-bag(init loc(e);B)
    ⇒ single-valued-classrel(es;X;B)
    ⇒ v1 ∈ Prior(X)?init(e)
    ⇒ v2 ∈ Prior(X)?init(e)
    ⇒ (v1 = v2 ∈ B))
BY
{ ((UnivCD THENA Auto)
   THEN MaUseClassRel (-2)
   THEN MaUseClassRel (-1)
   THEN Try (Complete ((UseSingleVal (-3) (-1) THEN Auto)))) }

1
1. Info : Type
2. B : Type
3. es : EO+(Info)
4. X : EClass(B)
5. init : Id ─→ bag(B)
6. e : E@i
7. v1 : B@i
8. v2 : B@i
9. single-valued-bag(init loc(e);B)@i
10. single-valued-classrel(es;X;B)@i
11. e' : E
12. es-p-local-pred(es;λe'.(↓∃w:B. w ∈ X(e'))) e e'
13. v1 ∈ X(e')
14. e1 : E
15. es-p-local-pred(es;λe'.(↓∃w:B. w ∈ X(e'))) e e1
16. v2 ∈ X(e1)
⊢ v1 = v2 ∈ B

2
1. Info : Type
2. B : Type
3. es : EO+(Info)
4. X : EClass(B)
5. init : Id ─→ bag(B)
6. e : E@i
7. v1 : B@i
8. v2 : B@i
9. single-valued-bag(init loc(e);B)@i
10. single-valued-classrel(es;X;B)@i
11. e' : E
12. es-p-local-pred(es;λe'.(↓∃w:B. w ∈ X(e'))) e e'
13. v1 ∈ X(e')
14. ∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ X(e'))))
15. v2 ↓∈ init loc(e)
⊢ v1 = v2 ∈ B

3
1. Info : Type
2. B : Type
3. es : EO+(Info)
4. X : EClass(B)
5. init : Id ─→ bag(B)
6. e : E@i
7. v1 : B@i
8. v2 : B@i
9. single-valued-bag(init loc(e);B)@i
10. single-valued-classrel(es;X;B)@i
11. ∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ X(e'))))
12. v1 ↓∈ init loc(e)
13. e' : E
14. es-p-local-pred(es;λe'.(↓∃w:B. w ∈ X(e'))) e e'
15. v2 ∈ X(e')
⊢ v1 = v2 ∈ B

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(B)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
    \mforall{}e:E.  \mforall{}v1,v2:B.
        (single-valued-bag(init  loc(e);B)
        {}\mRightarrow{}  single-valued-classrel(es;X;B)
        {}\mRightarrow{}  v1  \mmember{}  Prior(X)?init(e)
        {}\mRightarrow{}  v2  \mmember{}  Prior(X)?init(e)
        {}\mRightarrow{}  (v1  =  v2))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MaUseClassRel  (-2)
  THEN  MaUseClassRel  (-1)
  THEN  Try  (Complete  ((UseSingleVal  (-3)  (-1)  THEN  Auto))))

---

Home Index