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


1. Info Type
2. Type
3. EClass(B ─→ B)
4. init Id ─→ bag(B)
5. Base
6. ~ λinit,X. loop-class-memory(X;init)
7. Base
8. ~ λinit,X. loop-class-state(X;init)
9. init X ∈ EClass(B)
10. init X ∈ EClass(B)
11. es EO+(Info)@i'
12. E@i
13. ¬↑first(e)
14. ∀e1:E. ((e1 < e)  ((R init es e1) (Prior(L init X)?init es e1) ∈ bag(B)))
15. (R init es pred(e)) (Prior(L init X)?init es pred(e)) ∈ bag(B)
⊢ if 0 <#(eclass3(X;R init X) es pred(e)) then eclass3(X;R init X) es pred(e) else init es pred(e) fi 
if 0 <#(L init es pred(e)) then init 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]
      THENA Auto
      UnrollAbbreviationInConcl `L'
      Reduce 0
      RepUR ``eclass-cond eclass3 class-ap`` 0
      Try (HypSubst (-2) THENA Complete Auto)
      Try (HypSubst (-4) THENA Complete Auto)
      Try (HypSubst (-2) THENA Complete Auto)
      ]⋅⋅ }

1
1. Info Type
2. Type
3. EClass(B ─→ B)
4. init Id ─→ bag(B)
5. Base
6. ~ λinit,X. loop-class-memory(X;init)
7. Base
8. ~ λinit,X. loop-class-state(X;init)
9. init X ∈ EClass(B)
10. init X ∈ EClass(B)
11. es EO+(Info)@i'
12. E@i
13. ¬↑first(e)
14. ∀e1:E. ((e1 < e)  ((R init es e1) (Prior(L init X)?init es e1) ∈ bag(B)))
15. (R init es pred(e)) (Prior(L init X)?init es pred(e)) ∈ bag(B)
16. bag(B)@i
17. (R init 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. v1 ∈ bag(B)@i
⊢ if 0 <#(∪f∈es pred(e).bag-map(f;v)) then ∪f∈es pred(e).bag-map(f;v) else fi 
if 0 <#(if pred(e) ∈b then ∪f∈es pred(e).bag-map(f;v1) else v1 fi )
  then if pred(e) ∈b then ∪f∈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