Step * of Lemma Accum-class-trans-refl

`∀[Info,B,A:Type].`
`  ∀R:B ─→ B ─→ ℙ. ∀f:A ─→ B ─→ B. ∀init:Id ─→ bag(B). ∀X:EClass(A). ∀es:EO+(Info). ∀e1,e2:E. ∀v1,v2:B.`
`    (Refl(B;x,y.R[x;y])`
`    `` Trans(B;x,y.R[x;y])`
`    `` (∀s1,s2:B.  SqStable(R[s1;s2]))`
`    `` (∀a:A. ∀e:E.`
`          ((e1 <loc e) `` e ≤loc e2  `` a ∈ X(e) `` (∀s:B. (s ∈ Prior(Accum-class(f;init;X))?init(e) `` R[s;f a s]))))`
`    `` single-valued-classrel(es;X;A)`
`    `` single-valued-bag(init loc(e1);B)`
`    `` v1 ∈ Accum-class(f;init;X)(e1)`
`    `` v2 ∈ Accum-class(f;init;X)(e2)`
`    `` e1 ≤loc e2 `
`    `` R[v1;v2])`
BY
`{ ((UnivCD THENA Auto)`
`   THEN D (-1)`
`   THEN Try (Complete ((InstLemma `Accum-class-trans` [⌈Info⌉;⌈B⌉;⌈A⌉;⌈R⌉;⌈f⌉;⌈init⌉;⌈X⌉;⌈es⌉;⌈e1⌉;⌈e2⌉;⌈v1⌉;⌈v2⌉]⋅`
`                        THEN Auto`
`                        )))`
`   THEN Try (Complete (((RevHypSubst' (-1) (-2) THENA Auto)`
`                        THEN InstLemma `Accum-class-single-val0` [⌈Info⌉;⌈A⌉;⌈B⌉;⌈es⌉;⌈f⌉;⌈X⌉;⌈init⌉;⌈e1⌉;⌈v1⌉;⌈v2⌉]⋅`
`                        THEN Auto)))) }`

Latex:

Latex:
\mforall{}[Info,B,A:Type].
\mforall{}R:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B.  \mforall{}init:Id  {}\mrightarrow{}  bag(B).  \mforall{}X:EClass(A).  \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.
\mforall{}v1,v2:B.
(Refl(B;x,y.R[x;y])
{}\mRightarrow{}  Trans(B;x,y.R[x;y])
{}\mRightarrow{}  (\mforall{}s1,s2:B.    SqStable(R[s1;s2]))
{}\mRightarrow{}  (\mforall{}a:A.  \mforall{}e:E.
((e1  <loc  e)
{}\mRightarrow{}  e  \mleq{}loc  e2
{}\mRightarrow{}  a  \mmember{}  X(e)
{}\mRightarrow{}  (\mforall{}s:B.  (s  \mmember{}  Prior(Accum-class(f;init;X))?init(e)  {}\mRightarrow{}  R[s;f  a  s]))))
{}\mRightarrow{}  single-valued-classrel(es;X;A)
{}\mRightarrow{}  single-valued-bag(init  loc(e1);B)
{}\mRightarrow{}  v1  \mmember{}  Accum-class(f;init;X)(e1)
{}\mRightarrow{}  v2  \mmember{}  Accum-class(f;init;X)(e2)
{}\mRightarrow{}  e1  \mleq{}loc  e2
{}\mRightarrow{}  R[v1;v2])

By

Latex:
((UnivCD  THENA  Auto)
THEN  D  (-1)
THEN  Try  (Complete  ((InstLemma  `Accum-class-trans`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}init\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};
\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}]\mcdot{}
THEN  Auto
)))
THEN  Try  (Complete  (((RevHypSubst'  (-1)  (-2)  THENA  Auto)
THEN  InstLemma  `Accum-class-single-val0`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}init\mkleeneclose{};
\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}]\mcdot{}
THEN  Auto))))

Home Index