---

Step * of Lemma loop-class-memory-classrel

∀[Info,B:Type]. ∀[X:EClass(B ─→ B)]. ∀[init:Id ─→ bag(B)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:B].
  uiff(v ∈ loop-class-memory(X;init)(e);↓if first(e)
                                         then v ↓∈ init loc(e)
                                         else ∃b:B
                                               (b ∈ loop-class-memory(X;init)(pred(e))
                                               ∧ if pred(e) ∈b X
                                                 then ∃f:B ─→ B. (f ∈ X(pred(e)) ∧ (v = (f b) ∈ B))
                                                 else v = b ∈ B
                                                 fi )
                                         fi )
BY
{ ((UnivCD THENA Auto)
   THEN RW (AddrC [1] (RecUnfoldC `loop-class-memory`)) 0
   THEN RepeatFor 2 (Try (OldAutoSplit))
   THEN D 0
   THEN (UnivCD THENA Auto)
   THEN Try (MaUseClassRel (-1))
   THEN Try (Complete ((D 0 THEN Auto)))
   THEN Try (Complete ((RepUR ``es-p-local-pred`` (-2) THEN Auto)))
   THEN Try ((MaUseClassRel 0 THEN SquashExRepD))
   THEN Try (Complete ((D 0 THEN OrRight THEN Auto)))
   THEN Try (MaUseClassRel (-1))
   THEN All (RepUR ``es-p-local-pred``)
   THEN RepD
   THEN Try ((Assert ⌈↓∃b:B. b ∈ loop-class-memory(X;init)(e')⌉⋅
              THENA Complete ((D 0 THEN InstConcl [⌈b⌉]⋅ THEN Auto))
              ))
   THEN Try ((RWO "loop-class-memory-exists<" (-1) THENA Complete (Auto)))
   THEN Try ((Subst ⌈loc(e') = loc(pred(e)) ∈ Id⌉ (-1)⋅ THENA Complete (Auto)))
   THEN Try ((Using [`X',⌈X⌉] (FLemma `loop-class-memory-exists` [-1])⋅ THENA Complete (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
7. v : B
8. ¬↑first(e)
9. ↑pred(e) ∈b X
10. e' : E
11. (e' <loc e)
12. ↓∃w:B. w ∈ eclass3(X;loop-class-memory(X;init))(e')
13. ∀e'':E. ((e'' <loc e) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ eclass3(X;loop-class-memory(X;init))(e'')))
14. f : B ─→ B
15. b : B
16. f ∈ X(e')
17. b ∈ loop-class-memory(X;init)(e')
18. v = (f b) ∈ B
19. 0 < #(init loc(pred(e)))
20. ↓∃v:B. v ∈ loop-class-memory(X;init)(pred(e))
⊢ ↓∃b:B. (b ∈ loop-class-memory(X;init)(pred(e)) ∧ (∃f:B ─→ B. (f ∈ X(pred(e)) ∧ (v = (f b) ∈ B))))

2
1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. es : EO+(Info)
6. e : E
7. v : B
8. ¬↑first(e)
9. ↑pred(e) ∈b X
10. ∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ eclass3(X;loop-class-memory(X;init))(e'))))
11. v ↓∈ init loc(e)
⊢ ↓∃b:B. (b ∈ loop-class-memory(X;init)(pred(e)) ∧ (∃f:B ─→ B. (f ∈ X(pred(e)) ∧ (v = (f b) ∈ B))))

3
1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. es : EO+(Info)
6. e : E
7. v : B
8. ¬↑first(e)
9. ↑pred(e) ∈b X
10. b : B
11. b ∈ loop-class-memory(X;init)(pred(e))
12. f : B ─→ B
13. f ∈ X(pred(e))
14. v = (f b) ∈ B
⊢ ↓(∃e':E
     (((e' <loc e)
     ∧ (↓∃w:B. w ∈ eclass3(X;loop-class-memory(X;init))(e'))
     ∧ (∀e'':E. ((e'' <loc e) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ eclass3(X;loop-class-memory(X;init))(e'')))))
     ∧ v ∈ eclass3(X;loop-class-memory(X;init))(e')))
   ∨ ((∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ eclass3(X;loop-class-memory(X;init))(e'))))) ∧ v ↓∈ init loc(e))

4
1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. es : EO+(Info)
6. e : E
7. v : B
8. ¬↑first(e)
9. ¬↑pred(e) ∈b X
10. e' : E
11. (e' <loc e)
12. ↓∃w:B. w ∈ eclass3(X;loop-class-memory(X;init))(e')
13. ∀e'':E. ((e'' <loc e) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ eclass3(X;loop-class-memory(X;init))(e'')))
14. f : B ─→ B
15. b : B
16. f ∈ X(e')
17. b ∈ loop-class-memory(X;init)(e')
18. v = (f b) ∈ B
19. 0 < #(init loc(pred(e)))
20. ↓∃v:B. v ∈ loop-class-memory(X;init)(pred(e))
⊢ ↓∃b:B. (b ∈ loop-class-memory(X;init)(pred(e)) ∧ (v = b ∈ B))

5
1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. es : EO+(Info)
6. e : E
7. v : B
8. ¬↑first(e)
9. ¬↑pred(e) ∈b X
10. ∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ eclass3(X;loop-class-memory(X;init))(e'))))
11. v ↓∈ init loc(e)
⊢ ↓∃b:B. (b ∈ loop-class-memory(X;init)(pred(e)) ∧ (v = b ∈ B))

6
1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. es : EO+(Info)
6. e : E
7. v : B
8. ¬↑first(e)
9. ¬↑pred(e) ∈b X
10. b : B
11. b ∈ loop-class-memory(X;init)(pred(e))
12. v = b ∈ B
⊢ ↓(∃e':E
     (((e' <loc e)
     ∧ (↓∃w:B. w ∈ eclass3(X;loop-class-memory(X;init))(e'))
     ∧ (∀e'':E. ((e'' <loc e) ⇒ (e' <loc e'') ⇒ (¬↓∃w:B. w ∈ eclass3(X;loop-class-memory(X;init))(e'')))))
     ∧ v ∈ eclass3(X;loop-class-memory(X;init))(e')))
   ∨ ((∀e':E. ((e' <loc e) ⇒ (∀w:B. (¬w ∈ eclass3(X;loop-class-memory(X;init))(e'))))) ∧ v ↓∈ init loc(e))

---

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-memory(X;init)(e);\mdownarrow{}if  first(e)
                                                                                  then  v  \mdownarrow{}\mmember{}  init  loc(e)
                                                                                  else  \mexists{}b:B
                                                                                              (b  \mmember{}  loop-class-memory(X;init)(pred(e))
                                                                                              \mwedge{}  if  pred(e)  \mmember{}\msubb{}  X
                                                                                                  then  \mexists{}f:B  {}\mrightarrow{}  B.  (f  \mmember{}  X(pred(e))  \mwedge{}  (v  =  (f  b)))
                                                                                                  else  v  =  b
                                                                                                  fi  )
                                                                                  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RW  (AddrC  [1]  (RecUnfoldC  `loop-class-memory`))  0
  THEN  RepeatFor  2  (Try  (OldAutoSplit))
  THEN  D  0
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (MaUseClassRel  (-1))
  THEN  Try  (Complete  ((D  0  THEN  Auto)))
  THEN  Try  (Complete  ((RepUR  ``es-p-local-pred``  (-2)  THEN  Auto)))
  THEN  Try  ((MaUseClassRel  0  THEN  SquashExRepD))
  THEN  Try  (Complete  ((D  0  THEN  OrRight  THEN  Auto)))
  THEN  Try  (MaUseClassRel  (-1))
  THEN  All  (RepUR  ``es-p-local-pred``)
  THEN  RepD
  THEN  Try  ((Assert  \mkleeneopen{}\mdownarrow{}\mexists{}b:B.  b  \mmember{}  loop-class-memory(X;init)(e')\mkleeneclose{}\mcdot{}
                        THENA  Complete  ((D  0  THEN  InstConcl  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto))
                        ))
  THEN  Try  ((RWO  "loop-class-memory-exists<"  (-1)  THENA  Complete  (Auto)))
  THEN  Try  ((Subst  \mkleeneopen{}loc(e')  =  loc(pred(e))\mkleeneclose{}  (-1)\mcdot{}  THENA  Complete  (Auto)))
  THEN  Try  ((Using  [`X',\mkleeneopen{}X\mkleeneclose{}]  (FLemma  `loop-class-memory-exists`  [-1])\mcdot{}  THENA  Complete  (Auto))))

---

Home Index