---

Step * 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)
⊢ 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)
BY
{ Seq [ DupHyp (-1)
      ; MoveToConcl (-1)
      ; GenConclAtAddr [1;2]
      ; GenConclAtAddr [1;3]
      ; D 0 THENA Auto
      ; UnrollAbbreviationInConcl `L'
      ; Reduce 0
      ; RepUR ``eclass-cond eclass3 class-ap`` 0
      ; Try (HypSubst (-2) 0 THENA Complete Auto)
      ; Try (HypSubst (-4) 0 THENA Complete Auto)
      ; Try (HypSubst (-2) 0 THENA Complete 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
⊢ 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)

---

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  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 


By

---

Latex:
Seq  [  DupHyp  (-1)
            ;  MoveToConcl  (-1)
            ;  GenConclAtAddr  [1;2]
            ;  GenConclAtAddr  [1;3]
            ;  D  0  THENA  Auto
            ;  UnrollAbbreviationInConcl  `L'
            ;  Reduce  0
            ;  RepUR  ``eclass-cond  eclass3  class-ap``  0
            ;  Try  (HypSubst  (-2)  0  THENA  Complete  Auto)
            ;  Try  (HypSubst  (-4)  0  THENA  Complete  Auto)
            ;  Try  (HypSubst  (-2)  0  THENA  Complete  Auto)
            ]\mcdot{}\mcdot{}

---

Home Index