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. Type
3. es EO+(Info)
4. EClass(B)
5. init Id ─→ bag(B)
6. 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'
13. v1 ∈ X(e')
14. e1 E
15. es-p-local-pred(es;λe'.(↓∃w:B. w ∈ X(e'))) e1
16. v2 ∈ X(e1)
⊢ v1 v2 ∈ B

2
1. Info Type
2. Type
3. es EO+(Info)
4. EClass(B)
5. init Id ─→ bag(B)
6. 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'
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. Type
3. es EO+(Info)
4. EClass(B)
5. init Id ─→ bag(B)
6. 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'
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