---

Step * of Lemma loop-class-state-single-val

∀[Info,B:Type]. ∀[init:Id ─→ bag(B)]. ∀[X:EClass(B ─→ B)]. ∀[es:EO+(Info)].
  (single-valued-classrel(es;loop-class-state(X;init);B)) supposing 
     ((∀l:Id. single-valued-bag(init l;B)) and 
     single-valued-classrel(es;X;B ─→ B))
BY
{ ((UnivCD THENA Auto)
   THEN UnfoldTopAb 0
   THEN CausalInd'
   THEN Auto
   THEN MaUseClassRel (-2)
   THEN MaUseClassRel (-1)
   THEN All (\h.SplitOnHypITE h THENA CpltAuto)
   THEN Auto
   THEN ExRepD
   THEN Try ((InstHyp [⌈loc(e)⌉] 7⋅ THENA CpltAuto))
   THEN Try (UseSingleVal 13 18)
   THEN Try ((InstHyp [⌈pred(e)⌉;⌈b⌉;⌈b1⌉] 9⋅ THENA Complete (Auto)))
   THEN Auto
   THEN UseSingleVal 15 20
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(B  {}\mrightarrow{}  B)].  \mforall{}[es:EO+(Info)].
    (single-valued-classrel(es;loop-class-state(X;init);B))  supposing 
          ((\mforall{}l:Id.  single-valued-bag(init  l;B))  and 
          single-valued-classrel(es;X;B  {}\mrightarrow{}  B))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  UnfoldTopAb  0
  THEN  CausalInd'
  THEN  Auto
  THEN  MaUseClassRel  (-2)
  THEN  MaUseClassRel  (-1)
  THEN  All  (\mbackslash{}h.SplitOnHypITE  h  THENA  CpltAuto)
  THEN  Auto
  THEN  ExRepD
  THEN  Try  ((InstHyp  [\mkleeneopen{}loc(e)\mkleeneclose{}]  7\mcdot{}  THENA  CpltAuto))
  THEN  Try  (UseSingleVal  13  18)
  THEN  Try  ((InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]  9\mcdot{}  THENA  Complete  (Auto)))
  THEN  Auto
  THEN  UseSingleVal  15  20
  THEN  Auto)

---

Home Index