---

Step * 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. loop-class-memory(X;init) ∈ EClass(B)
6. loop-class-state(X;init) ∈ EClass(B)
7. R : Base
8. R ~ λinit,X. loop-class-memory(X;init)
9. L : Base
10. L ~ λinit,X. loop-class-state(X;init)
11. R init X ∈ EClass(B)
12. L init X ∈ EClass(B)
⊢ (R init X) = Prior(L init X)?init ∈ EClass(B)
BY
{ Seq [Thin (-7)
      ; Thin (-7)
      ; BLemma `eclass-ext`
      ; Auto
      ; MoveToConcl (-1)
      ; CausalInd'
      ; UnrollAbbreviationInConcl `R'
      ; Reduce 0
      ; RWO "primed-class-opt-cases" 0 THENA Auto
      ; AutoSplit
      ; InstHyp [⌈pred(e)⌉] (-1) 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)
⊢ 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)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  B  :  Type
3.  X  :  EClass(B  {}\mrightarrow{}  B)
4.  init  :  Id  {}\mrightarrow{}  bag(B)
5.  loop-class-memory(X;init)  \mmember{}  EClass(B)
6.  loop-class-state(X;init)  \mmember{}  EClass(B)
7.  R  :  Base
8.  R  \msim{}  \mlambda{}init,X.  loop-class-memory(X;init)
9.  L  :  Base
10.  L  \msim{}  \mlambda{}init,X.  loop-class-state(X;init)
11.  R  init  X  \mmember{}  EClass(B)
12.  L  init  X  \mmember{}  EClass(B)
\mvdash{}  (R  init  X)  =  Prior(L  init  X)?init


By

---

Latex:
Seq  [Thin  (-7)
            ;  Thin  (-7)
            ;  BLemma  `eclass-ext`
            ;  Auto
            ;  MoveToConcl  (-1)
            ;  CausalInd'
            ;  UnrollAbbreviationInConcl  `R'
            ;  Reduce  0
            ;  RWO  "primed-class-opt-cases"  0  THENA  Auto
            ;  AutoSplit
            ;  InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  (-1)  THENA  Auto
            ]
            \mcdot{}

---

Home Index