---

Step * of Lemma Prior-Accum-class-single-val0

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[f:A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E]. ∀[v1,v2:B].
  (v1 = v2 ∈ B) supposing 
     (v1 ∈ Prior(Accum-class(f;init;X))?init(e) and 
     v2 ∈ Prior(Accum-class(f;init;X))?init(e) and 
     single-valued-bag(init loc(e);B) and 
     single-valued-classrel(es;X;A))
BY
{ ((UnivCD THENA Auto)
   THEN MaUseClassRel (-2)
   THEN MaUseClassRel (-1)
   THEN All (RepUR ``es-p-local-pred``)
   THEN SquashExRepD
   THEN Try (Complete ((UseSingleVal (-3) (-1) THEN Auto)))
   THEN Try (Complete ((Assert ⌜False⌝⋅ THEN Auto)))
   THEN UseLoclTri ⌜es⌝⌜e'⌝⌜e1⌝⋅
   THEN Try (Complete (((HypSubst' (-1) (-8) THENA Auto) THEN FLemma `Accum-class-single-val0` [-3;-1] THEN Auto)))
   THEN Assert ⌜False⌝⋅
   THEN Auto
   THEN Try (Complete (((InstHyp [⌜e1⌝] (-9)⋅ THENA Auto) THEN D (-1) THEN D 0 THEN MaAuto)))
   THEN Try (Complete (((InstHyp [⌜e'⌝] (-3)⋅ THENA Auto) THEN D (-1) THEN D 0 THEN MaAuto)))) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MaUseClassRel  (-2)
  THEN  MaUseClassRel  (-1)
  THEN  All  (RepUR  ``es-p-local-pred``)
  THEN  SquashExRepD
  THEN  Try  (Complete  ((UseSingleVal  (-3)  (-1)  THEN  Auto)))
  THEN  Try  (Complete  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e'\mkleeneclose{}\mkleeneopen{}e1\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  (((HypSubst'  (-1)  (-8)  THENA  Auto)
                                            THEN  FLemma  `Accum-class-single-val0`  [-3;-1]
                                            THEN  Auto)))
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  (((InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-9)\mcdot{}  THENA  Auto)  THEN  D  (-1)  THEN  D  0  THEN  MaAuto)))
  THEN  Try  (Complete  (((InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  D  (-1)  THEN  D  0  THEN  MaAuto))))

---

Home Index