---

Step * 1 1 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)
16. v : bag(B)@i
17. (R init X es pred(e)) = v ∈ bag(B)@i
18. v1 : bag(B)@i
19. (Prior(L init X)?init es pred(e)) = v1 ∈ bag(B)@i
20. v = v1 ∈ bag(B)@i
⊢ if 0 <z #(∪f∈X es pred(e).bag-map(f;v)) then ∪f∈X es pred(e).bag-map(f;v) else v fi 
= if 0 <z #(if pred(e) ∈b X then ∪f∈X es pred(e).bag-map(f;v1) else v1 fi )
  then if pred(e) ∈b X then ∪f∈X es pred(e).bag-map(f;v1) else v1 fi 
  else v1
  fi 
∈ bag(B)
BY
{ (RepUR ``member-eclass`` 0 THEN (GenConclTerm ⌈X es pred(e)⌉⋅ THENA 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)
16. v : bag(B)@i
17. (R init X es pred(e)) = v ∈ bag(B)@i
18. v1 : bag(B)@i
19. (Prior(L init X)?init es pred(e)) = v1 ∈ bag(B)@i
20. v = v1 ∈ bag(B)@i
21. v2 : bag(B ─→ B)@i
22. (X es pred(e)) = v2 ∈ bag(B ─→ B)@i
⊢ if 0 <z #(∪f∈v2.bag-map(f;v)) then ∪f∈v2.bag-map(f;v) else v fi 
= if 0 <z #(if ¬b(#(v2) =z 0) then ∪f∈v2.bag-map(f;v1) else v1 fi )
  then if ¬b(#(v2) =z 0) then ∪f∈v2.bag-map(f;v1) else v1 fi 
  else v1
  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))
16.  v  :  bag(B)@i
17.  (R  init  X  es  pred(e))  =  v@i
18.  v1  :  bag(B)@i
19.  (Prior(L  init  X)?init  es  pred(e))  =  v1@i
20.  v  =  v1@i
\mvdash{}  if  0  <z  \#(\mcup{}f\mmember{}X  es  pred(e).bag-map(f;v))  then  \mcup{}f\mmember{}X  es  pred(e).bag-map(f;v)  else  v  fi 
=  if  0  <z  \#(if  pred(e)  \mmember{}\msubb{}  X  then  \mcup{}f\mmember{}X  es  pred(e).bag-map(f;v1)  else  v1  fi  )
    then  if  pred(e)  \mmember{}\msubb{}  X  then  \mcup{}f\mmember{}X  es  pred(e).bag-map(f;v1)  else  v1  fi 
    else  v1
    fi 


By

---

Latex:
(RepUR  ``member-eclass``  0  THEN  (GenConclTerm  \mkleeneopen{}X  es  pred(e)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index