---

Step * of Lemma State-loc-comb-total

∀[Info,B,A:Type]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[init:Id ─→ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  es-total-class(es;State-loc-comb(init;f;X)) supposing ∀l:Id. (1 ≤ #(init l))
BY
{ ((UnivCD THENA MaAuto)
   THEN Unfold `es-total-class` 0
   THEN Auto
   THEN (InstLemma `State-loc-comb-exists` [⌈Info⌉;⌈B⌉;⌈A⌉;⌈f⌉;⌈init⌉;⌈X⌉;⌈es⌉;⌈e⌉]⋅
         THENA (Auto THEN InstHyp [⌈loc(e)⌉] (-2)⋅ THEN Auto)
         )
   THEN All(RepUR ``classrel class-ap``)
   THEN FLemma `bag-member-iff-size` [-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B,A:Type].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].
    es-total-class(es;State-loc-comb(init;f;X))  supposing  \mforall{}l:Id.  (1  \mleq{}  \#(init  l))


By

---

Latex:
((UnivCD  THENA  MaAuto)
  THEN  Unfold  `es-total-class`  0
  THEN  Auto
  THEN  (InstLemma  `State-loc-comb-exists`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}init\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  InstHyp  [\mkleeneopen{}loc(e)\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)
              )
  THEN  All(RepUR  ``classrel  class-ap``)
  THEN  FLemma  `bag-member-iff-size`  [-1]
  THEN  Auto)

---

Home Index