---

Step * 1 1 of Lemma loop-class-memory-no-input


1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. es : EO+(Info)
6. e : E@i
7. ∀e1:E
     ((e1 < e)
     ⇒ ((¬↑first(e1)) ⇒ (¬↑pred(e1) ∈b X))
     ⇒ (loop-class-memory(X;init)(e1) = Prior(loop-class-memory(X;init))?init(e1) ∈ bag(B)))
8. (¬↑first(e)) ⇒ (¬↑pred(e) ∈b X)@i
9. 0 < #(init loc(e))
⊢ loop-class-memory(X;init)(e) = Prior(loop-class-memory(X;init))?init(e) ∈ bag(B)
BY
{ (RepUR ``class-ap`` 0
   THEN RW (AddrC [2] (RecUnfoldC `loop-class-memory`)) 0
   THEN (RWO "primed-class-opt-cases" 0 THENA (Try (Complete (Auto)) THEN DoSubsume THEN Auto))
   THEN Fold `class-ap` 0
   THEN RepeatFor 3 (OldAutoSplit)
   THEN Try (Complete ((RecFold `loop-class-memory` 0 THEN Auto)))
   THEN Try (Complete (((Subst ⌈loc(e) = loc(pred(e)) ∈ Id⌉ (-4)⋅ THENA Auto)
                        THEN Using [`X',⌈X⌉] (FLemma `loop-class-memory-size` [-4])⋅
                        THEN Auto)))) }

1
1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. es : EO+(Info)
6. e : E@i
7. ∀e1:E
     ((e1 < e)
     ⇒ ((¬↑first(e1)) ⇒ (¬↑pred(e1) ∈b X))
     ⇒ (loop-class-memory(X;init)(e1) = Prior(loop-class-memory(X;init))?init(e1) ∈ bag(B)))
8. (¬↑first(e)) ⇒ (¬↑pred(e) ∈b X)@i
9. 0 < #(init loc(e))
10. ¬↑first(e)
11. 0 < #(eclass3(X;loop-class-memory(X;init))(pred(e)))
12. 0 < #(loop-class-memory(X;init)(pred(e)))
⊢ eclass3(X;loop-class-memory(X;init))(pred(e)) = loop-class-memory(X;init)(pred(e)) ∈ bag(B)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  B  :  Type
3.  X  :  EClass(B  {}\mrightarrow{}  B)
4.  init  :  Id  {}\mrightarrow{}  bag(B)
5.  es  :  EO+(Info)
6.  e  :  E@i
7.  \mforall{}e1:E
          ((e1  <  e)
          {}\mRightarrow{}  ((\mneg{}\muparrow{}first(e1))  {}\mRightarrow{}  (\mneg{}\muparrow{}pred(e1)  \mmember{}\msubb{}  X))
          {}\mRightarrow{}  (loop-class-memory(X;init)(e1)  =  Prior(loop-class-memory(X;init))?init(e1)))
8.  (\mneg{}\muparrow{}first(e))  {}\mRightarrow{}  (\mneg{}\muparrow{}pred(e)  \mmember{}\msubb{}  X)@i
9.  0  <  \#(init  loc(e))
\mvdash{}  loop-class-memory(X;init)(e)  =  Prior(loop-class-memory(X;init))?init(e)


By

---

Latex:
(RepUR  ``class-ap``  0
  THEN  RW  (AddrC  [2]  (RecUnfoldC  `loop-class-memory`))  0
  THEN  (RWO  "primed-class-opt-cases"  0  THENA  (Try  (Complete  (Auto))  THEN  DoSubsume  THEN  Auto))
  THEN  Fold  `class-ap`  0
  THEN  RepeatFor  3  (OldAutoSplit)
  THEN  Try  (Complete  ((RecFold  `loop-class-memory`  0  THEN  Auto)))
  THEN  Try  (Complete  (((Subst  \mkleeneopen{}loc(e)  =  loc(pred(e))\mkleeneclose{}  (-4)\mcdot{}  THENA  Auto)
                                            THEN  Using  [`X',\mkleeneopen{}X\mkleeneclose{}]  (FLemma  `loop-class-memory-size`  [-4])\mcdot{}
                                            THEN  Auto))))

---

Home Index