---

Step * of Lemma loop-class-state-total

∀[Info,B:Type]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(B ⟶ B)]. ∀[es:EO+(Info)].
  es-total-class(es;loop-class-state(X;init)) supposing ∀l:Id. (1 ≤ #(init l))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `es-total-class` 0
   THEN Auto
   THEN (Assert ⌜0 < #(init loc(e))⌝⋅ THENA (InstHyp [⌜loc(e)⌝] (-2)⋅ THEN Auto))
   THEN (RW (LemmaWithC [`X',⌜X⌝] `loop-class-state-exists`) (-1)⋅ THENA Auto)
   THEN All(RepUR ``classrel class-ap``)
   THEN FLemma `bag-member-iff-size` [-1]
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `es-total-class`  0
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}0  <  \#(init  loc(e))\mkleeneclose{}\mcdot{}  THENA  (InstHyp  [\mkleeneopen{}loc(e)\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto))
  THEN  (RW  (LemmaWithC  [`X',\mkleeneopen{}X\mkleeneclose{}]  `loop-class-state-exists`)  (-1)\mcdot{}  THENA  Auto)
  THEN  All(RepUR  ``classrel  class-ap``)
  THEN  FLemma  `bag-member-iff-size`  [-1]
  THEN  Auto)

---

Home Index