---

Step * of Lemma loop-class-memory-prior-eq

∀[Info,B:Type]. ∀[X:EClass(B ⟶ B)]. ∀[init:Id ⟶ bag(B)]. ∀[es:EO+(Info)]. ∀[e:E].
  (Prior(loop-class-memory(X;init))?init(e)
  = if first(e) then init loc(e) else loop-class-memory(X;init)(pred(e)) fi 
  ∈ bag(B))
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN CausalInd'
   THEN AutoSplit
   THEN (RWO "primed-class-opt-cases2" 0 THENA (Try (Complete (Auto)) THEN DoSubsume THEN Auto))
   THEN RepeatFor 2 (AutoSplit)
   THEN (Assert ⌜¬0 < #(loop-class-memory(X;init)(pred(e)))⌝⋅ THENA Auto')
   THEN (RWO "loop-class-memory-size<" (-1) THENA Auto)
   THEN (Assert ⌜↑(#(loop-class-memory(X;init)(pred(e))) =z 0)⌝⋅ THENA (RW assert_pushdownC 0 THEN Auto'))
   THEN (RWO "null-bag-size<" (-1) THENA Auto)
   THEN (RWO "assert-bag-null" (-1) THENA Auto)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN (BLemma `assert-bag-null` THENA Auto)
   THEN (RWO "null-bag-size" 0 THENA Auto)
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN SupposeNot
   THEN D (-3)
   THEN Using [`X',⌜X⌝] (BLemma `loop-class-memory-size-prior`)⋅
   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].
    (Prior(loop-class-memory(X;init))?init(e)
    =  if  first(e)  then  init  loc(e)  else  loop-class-memory(X;init)(pred(e))  fi  )


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'
  THEN  AutoSplit
  THEN  (RWO  "primed-class-opt-cases2"  0  THENA  (Try  (Complete  (Auto))  THEN  DoSubsume  THEN  Auto))
  THEN  RepeatFor  2  (AutoSplit)
  THEN  (Assert  \mkleeneopen{}\mneg{}0  <  \#(loop-class-memory(X;init)(pred(e)))\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  (RWO  "loop-class-memory-size<"  (-1)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\muparrow{}(\#(loop-class-memory(X;init)(pred(e)))  =\msubz{}  0)\mkleeneclose{}\mcdot{}
              THENA  (RW  assert\_pushdownC  0  THEN  Auto')
              )
  THEN  (RWO  "null-bag-size<"  (-1)  THENA  Auto)
  THEN  (RWO  "assert-bag-null"  (-1)  THENA  Auto)
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  (BLemma  `assert-bag-null`  THENA  Auto)
  THEN  (RWO  "null-bag-size"  0  THENA  Auto)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  SupposeNot
  THEN  D  (-3)
  THEN  Using  [`X',\mkleeneopen{}X\mkleeneclose{}]  (BLemma  `loop-class-memory-size-prior`)\mcdot{}
  THEN  Auto')

---

Home Index