Step * of Lemma 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 ∈ Accum-class(f;init;X)(e) and `
`     v2 ∈ Accum-class(f;init;X)(e) and `
`     single-valued-bag(init loc(e);B) and `
`     single-valued-classrel(es;X;A))`
BY
`{ (InstLemma `rec-combined-class-opt-1-single-val0` []`
`   THEN RepeatFor 10 (ParallelLast)`
`   THEN Unfold `Accum-class` 0`
`   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{}  Accum-class(f;init;X)(e)  and
v2  \mmember{}  Accum-class(f;init;X)(e)  and
single-valued-bag(init  loc(e);B)  and
single-valued-classrel(es;X;A))

By

Latex:
(InstLemma  `rec-combined-class-opt-1-single-val0`  []
THEN  RepeatFor  10  (ParallelLast)
THEN  Unfold  `Accum-class`  0
THEN  Auto)

Home Index