---

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

∀[Info,B:Type]. ∀[init:Id ⟶ bag(B)]. ∀[X:EClass(B ⟶ B)]. ∀[es:EO+(Info)].
  (single-valued-classrel(es;loop-class-memory(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 All MaUseClassRel
   THEN RepeatFor 2 ((All (\h.SplitOnHypITE h THENA CpltAuto) THEN Auto THEN ExRepD))
   THEN Try ((InstHyp [⌜loc(e)⌝] 7⋅ THENA CpltAuto))
   THEN (InstHyp [⌜pred(e)⌝;⌜b1⌝;⌜b⌝] 9⋅ THENA Auto)
   THEN Auto
   THEN SingleValTerm ⌜pred(e)⌝⋅
   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-memory(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  All  MaUseClassRel
  THEN  RepeatFor  2  ((All  (\mbackslash{}h.SplitOnHypITE  h  THENA  CpltAuto)  THEN  Auto  THEN  ExRepD))
  THEN  Try  ((InstHyp  [\mkleeneopen{}loc(e)\mkleeneclose{}]  7\mcdot{}  THENA  CpltAuto))
  THEN  (InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  9\mcdot{}  THENA  Auto)
  THEN  Auto
  THEN  SingleValTerm  \mkleeneopen{}pred(e)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index