---

Step * of Lemma State-loc-comb-invariant-sv1

∀[Info,A,S:Type]. ∀[P:S ─→ ℙ].
  ∀init:Id ─→ bag(S). ∀f:Id ─→ A ─→ S ─→ S. ∀X:EClass(A). ∀es:EO+(Info). ∀e:E. ∀v:S.
    (single-valued-bag(init loc(e);S)
    ⇒ single-valued-classrel(es;X;A)
    ⇒ (∀s:S. (s ↓∈ init loc(e) ⇒ P[s]))
    ⇒ (∀a:A. ∀e':E. ∀s:S.
          (e' ≤loc e 
          ⇒ a ∈ X(e')
          ⇒ if first(e') then s ↓∈ init loc(e') else s ∈ State-loc-comb(init;f;X)(pred(e')) fi 
          ⇒ P[s]
          ⇒ P[f loc(e') a s]))
    ⇒ v ∈ State-loc-comb(init;f;X)(e)
    ⇒ P[v])
BY
{ ((UnivCD THENA MaAuto)
   THEN InstLemma `iterated-classrel-invariant` [⌈Info⌉;⌈A⌉;⌈S⌉;⌈init⌉;⌈f loc(e)⌉;⌈X⌉;⌈P⌉;⌈es⌉;⌈e⌉;⌈v⌉]⋅
   THEN Auto
   THEN Try (Complete (((RWO "State-loc-comb-classrel2" (-1) THENA Auto) THEN D (-1) THEN Unhide THEN Auto)))
   THEN (Subst ⌈loc(e) = loc(e') ∈ Id⌉ 0⋅ THENA MaAuto)
   THEN Using [`e\'',⌈e'⌉] (BHyp (-9))⋅
   THEN Auto
   THEN RepUR ``prior-iterated-classrel`` (-2)
   THEN D (-2)
   THEN RepD
   THEN AutoSplit
   THEN (RWO "State-loc-comb-classrel2" 0 THENA Auto)
   THEN D 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A,S:Type].  \mforall{}[P:S  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}init:Id  {}\mrightarrow{}  bag(S).  \mforall{}f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  S  {}\mrightarrow{}  S.  \mforall{}X:EClass(A).  \mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}v:S.
        (single-valued-bag(init  loc(e);S)
        {}\mRightarrow{}  single-valued-classrel(es;X;A)
        {}\mRightarrow{}  (\mforall{}s:S.  (s  \mdownarrow{}\mmember{}  init  loc(e)  {}\mRightarrow{}  P[s]))
        {}\mRightarrow{}  (\mforall{}a:A.  \mforall{}e':E.  \mforall{}s:S.
                    (e'  \mleq{}loc  e 
                    {}\mRightarrow{}  a  \mmember{}  X(e')
                    {}\mRightarrow{}  if  first(e')  then  s  \mdownarrow{}\mmember{}  init  loc(e')  else  s  \mmember{}  State-loc-comb(init;f;X)(pred(e'))  fi 
                    {}\mRightarrow{}  P[s]
                    {}\mRightarrow{}  P[f  loc(e')  a  s]))
        {}\mRightarrow{}  v  \mmember{}  State-loc-comb(init;f;X)(e)
        {}\mRightarrow{}  P[v])


By

---

Latex:
((UnivCD  THENA  MaAuto)
  THEN  InstLemma  `iterated-classrel-invariant`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}init\mkleeneclose{};\mkleeneopen{}f  loc(e)\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}
  ]\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  (((RWO  "State-loc-comb-classrel2"  (-1)  THENA  Auto)
                                            THEN  D  (-1)
                                            THEN  Unhide
                                            THEN  Auto)))
  THEN  (Subst  \mkleeneopen{}loc(e)  =  loc(e')\mkleeneclose{}  0\mcdot{}  THENA  MaAuto)
  THEN  Using  [`e\mbackslash{}'',\mkleeneopen{}e'\mkleeneclose{}]  (BHyp  (-9))\mcdot{}
  THEN  Auto
  THEN  RepUR  ``prior-iterated-classrel``  (-2)
  THEN  D  (-2)
  THEN  RepD
  THEN  AutoSplit
  THEN  (RWO  "State-loc-comb-classrel2"  0  THENA  Auto)
  THEN  D  0
  THEN  Auto)

---

Home Index