Step
*
of Lemma
sq_stable__single-valued-prior-iterated-classrel
∀[Info,A,S:Type].
∀init:Id ─→ bag(S). ∀f:A ─→ S ─→ S. ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:S.
(single-valued-classrel(es;X;A)
⇒ single-valued-bag(init loc(e);S)
⇒ SqStable(prior-iterated-classrel(es;A;S;v;X;f;init;e)))
BY
{ (Auto
THEN Unfold `sq_stable` 0
THEN Auto
THEN All (Unfold `prior-iterated-classrel`)
THEN (BoolCase ⌈first(e)⌉⋅ THENA Auto)
THEN Try (Complete (((OrLeft THENA Auto) THEN Auto THEN Unsquash THEN SplitOrHyps THEN Auto)))
THEN Try (Complete (((OrRight THENA Auto) THEN Auto THEN Unsquash THEN SplitOrHyps THEN Auto)))) }
Latex:
\mforall{}[Info,A,S:Type].
\mforall{}init:Id {}\mrightarrow{} bag(S). \mforall{}f:A {}\mrightarrow{} S {}\mrightarrow{} S. \mforall{}X:EClass(A). \mforall{}es:EO+(Info). \mforall{}e:E. \mforall{}v:S.
(single-valued-classrel(es;X;A)
{}\mRightarrow{} single-valued-bag(init loc(e);S)
{}\mRightarrow{} SqStable(prior-iterated-classrel(es;A;S;v;X;f;init;e)))
By
(Auto
THEN Unfold `sq\_stable` 0
THEN Auto
THEN All (Unfold `prior-iterated-classrel`)
THEN (BoolCase \mkleeneopen{}first(e)\mkleeneclose{}\mcdot{} THENA Auto)
THEN Try (Complete (((OrLeft THENA Auto) THEN Auto THEN Unsquash THEN SplitOrHyps THEN Auto)))
THEN Try (Complete (((OrRight THENA Auto) THEN Auto THEN Unsquash THEN SplitOrHyps THEN Auto))))
Home
Index