---

Step * 1 1 of Lemma loop-class-memory-is-prior-loop-class-state


1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. R : Base
6. R ~ λinit,X. loop-class-memory(X;init)
7. L : Base
8. L ~ λinit,X. loop-class-state(X;init)
9. R init X ∈ EClass(B)
10. L init X ∈ EClass(B)
11. es : EO+(Info)@i'
12. e : E@i
13. ¬↑first(e)
14. ∀e1:E. ((e1 < e) ⇒ ((R init X es e1) = (Prior(L init X)?init es e1) ∈ bag(B)))
15. (R init X es pred(e)) = (Prior(L init X)?init es pred(e)) ∈ bag(B)
⊢ if 0 <z #(eclass3(X;R init X) es pred(e))
then eclass3(X;R init X) es pred(e)
else Prior(eclass3(X;R init X))?init es pred(e)
fi 
= if 0 <z #(L init X es pred(e)) then L init X es pred(e) else Prior(L init X)?init es pred(e) fi 
∈ bag(B)
BY
{ (Subst ⌈Prior(eclass3(X;R init X))?init es pred(e) ~ R init X es pred(e)⌉ 0⋅
   THENA ((UnAbbreviateInConcl `R' THEN RW (AddrC [2;1;1] RecUnfoldTopAbC) 0) THEN Auto)
   ) }

1
1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. R : Base
6. R ~ λinit,X. loop-class-memory(X;init)
7. L : Base
8. L ~ λinit,X. loop-class-state(X;init)
9. R init X ∈ EClass(B)
10. L init X ∈ EClass(B)
11. es : EO+(Info)@i'
12. e : E@i
13. ¬↑first(e)
14. ∀e1:E. ((e1 < e) ⇒ ((R init X es e1) = (Prior(L init X)?init es e1) ∈ bag(B)))
15. (R init X es pred(e)) = (Prior(L init X)?init es pred(e)) ∈ bag(B)
⊢ if 0 <z #(eclass3(X;R init X) es pred(e)) then eclass3(X;R init X) es pred(e) else R init X es pred(e) fi 
= if 0 <z #(L init X es pred(e)) then L init X es pred(e) else Prior(L init X)?init es pred(e) fi 
∈ bag(B)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  B  :  Type
3.  X  :  EClass(B  {}\mrightarrow{}  B)
4.  init  :  Id  {}\mrightarrow{}  bag(B)
5.  R  :  Base
6.  R  \msim{}  \mlambda{}init,X.  loop-class-memory(X;init)
7.  L  :  Base
8.  L  \msim{}  \mlambda{}init,X.  loop-class-state(X;init)
9.  R  init  X  \mmember{}  EClass(B)
10.  L  init  X  \mmember{}  EClass(B)
11.  es  :  EO+(Info)@i'
12.  e  :  E@i
13.  \mneg{}\muparrow{}first(e)
14.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  ((R  init  X  es  e1)  =  (Prior(L  init  X)?init  es  e1)))
15.  (R  init  X  es  pred(e))  =  (Prior(L  init  X)?init  es  pred(e))
\mvdash{}  if  0  <z  \#(eclass3(X;R  init  X)  es  pred(e))
then  eclass3(X;R  init  X)  es  pred(e)
else  Prior(eclass3(X;R  init  X))?init  es  pred(e)
fi 
=  if  0  <z  \#(L  init  X  es  pred(e))  then  L  init  X  es  pred(e)  else  Prior(L  init  X)?init  es  pred(e)  fi 


By

---

Latex:
(Subst  \mkleeneopen{}Prior(eclass3(X;R  init  X))?init  es  pred(e)  \msim{}  R  init  X  es  pred(e)\mkleeneclose{}  0\mcdot{}
  THENA  ((UnAbbreviateInConcl  `R'  THEN  RW  (AddrC  [2;1;1]  RecUnfoldTopAbC)  0)  THEN  Auto)
  )

---

Home Index