---

Step * of Lemma loop-class-state-classrel

∀[Info,B:Type]. ∀[X:EClass(B ─→ B)]. ∀[init:Id ─→ bag(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ loop-class-state(X;init)(e);↓∃b:B
                                         (if first(e)
                                         then b ↓∈ init loc(e)
                                         else b ∈ loop-class-state(X;init)(pred(e))
                                         fi 
                                         ∧ if e ∈b X then ∃f:B ─→ B. (f ∈ X(e) ∧ (v = (f b) ∈ B)) else v = b ∈ B fi ))
BY
{ ((UnivCD THENA Auto)
   THEN RW (AddrC [1] (RecUnfoldC `loop-class-state`)) 0
   THEN (RWO "eclass-cond-classrel" 0 THENA Auto)
   THEN RepeatFor 2 (AutoSplit)
   THEN Auto
   THEN Try (SquashExRepD)
   THEN Try (OnSomeHyp(\i.RWO "loop-class-state-prior" i THENA Complete Auto))
   THEN SplitOrHyps
   THEN Auto
   THEN Try ((RWO "loop-class-state-prior" 0 THENA Auto))
   THEN Try ((D 0 THEN (InstConcl [⌈b⌉]⋅ THENA Complete (Auto))))
   THEN Try ((D 0 THEN (InstConcl [⌈f⌉]⋅ THENA Complete (Auto))))
   THEN Auto
   THEN Try ((InstConcl [⌈b⌉]⋅ THENA Complete (Auto)))
   THEN Try ((InstConcl [⌈f⌉]⋅ THENA Complete (Auto)))
   THEN Auto
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN Try (Complete ((OrRight THEN Auto)))
   THEN Try ((D 0 THEN (InstConcl [⌈v⌉]⋅ THENA Complete (Auto))))
   THEN Auto
   THEN D 0
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN Try (Complete ((OrRight THEN Auto)))) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  B)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:B].
    uiff(v  \mmember{}  loop-class-state(X;init)(e);\mdownarrow{}\mexists{}b:B
                                                                                  (if  first(e)
                                                                                  then  b  \mdownarrow{}\mmember{}  init  loc(e)
                                                                                  else  b  \mmember{}  loop-class-state(X;init)(pred(e))
                                                                                  fi 
                                                                                  \mwedge{}  if  e  \mmember{}\msubb{}  X
                                                                                      then  \mexists{}f:B  {}\mrightarrow{}  B.  (f  \mmember{}  X(e)  \mwedge{}  (v  =  (f  b)))
                                                                                      else  v  =  b
                                                                                      fi  ))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RW  (AddrC  [1]  (RecUnfoldC  `loop-class-state`))  0
  THEN  (RWO  "eclass-cond-classrel"  0  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  Auto
  THEN  Try  (SquashExRepD)
  THEN  Try  (OnSomeHyp(\mbackslash{}i.RWO  "loop-class-state-prior"  i  THENA  Complete  Auto))
  THEN  SplitOrHyps
  THEN  Auto
  THEN  Try  ((RWO  "loop-class-state-prior"  0  THENA  Auto))
  THEN  Try  ((D  0  THEN  (InstConcl  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Complete  (Auto))))
  THEN  Try  ((D  0  THEN  (InstConcl  [\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Complete  (Auto))))
  THEN  Auto
  THEN  Try  ((InstConcl  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Complete  (Auto)))
  THEN  Try  ((InstConcl  [\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Complete  (Auto)))
  THEN  Auto
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  Try  (Complete  ((OrRight  THEN  Auto)))
  THEN  Try  ((D  0  THEN  (InstConcl  [\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Complete  (Auto))))
  THEN  Auto
  THEN  D  0
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  Try  (Complete  ((OrRight  THEN  Auto))))

---

Home Index