---

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


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
BY
{ (All (RepUR ``es-p-local-pred``)
   THEN SquashExRepD
   THEN UseLoclTri ⌜es⌝⌜e'⌝⌜e1⌝⋅
   THEN Assert ⌜False⌝⋅
   THEN Auto
   THEN ((InstHyp [⌜e1⌝] (-9)⋅ THENA Complete (Auto)) ORELSE (InstHyp [⌜e'⌝] (-3)⋅ THENA Try (Complete (Auto))))
   THEN (D (-1) THEN D 0)
   THEN MaAuto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  B  :  Type
3.  es  :  EO+(Info)
4.  X  :  EClass(B)
5.  init  :  Id  {}\mrightarrow{}  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;\mlambda{}e'.(\mdownarrow{}\mexists{}w:B.  w  \mmember{}  X(e')))  e  e'
13.  v1  \mmember{}  X(e')
14.  e1  :  E
15.  es-p-local-pred(es;\mlambda{}e'.(\mdownarrow{}\mexists{}w:B.  w  \mmember{}  X(e')))  e  e1
16.  v2  \mmember{}  X(e1)
\mvdash{}  v1  =  v2


By

---

Latex:
(All  (RepUR  ``es-p-local-pred``)
  THEN  SquashExRepD
  THEN  UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e'\mkleeneclose{}\mkleeneopen{}e1\mkleeneclose{}\mcdot{}
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  ((InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-9)\mcdot{}  THENA  Complete  (Auto))
  ORELSE  (InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  (-3)\mcdot{}  THENA  Try  (Complete  (Auto)))
  )
  THEN  (D  (-1)  THEN  D  0)
  THEN  MaAuto)

---

Home Index