---

Step * of Lemma State-comb-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 ∈ State-comb(init;f;X)(e) and 
     v2 ∈ State-comb(init;f;X)(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 FLemma `iterated_classrel-single-val` [-2;-1]
   THEN Auto) }

---

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{}  State-comb(init;f;X)(e)  and 
          v2  \mmember{}  State-comb(init;f;X)(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  FLemma  `iterated\_classrel-single-val`  [-2;-1]
  THEN  Auto)

---

Home Index