---

Step * 1 1 3 1 1 2 of Lemma rec-class-unique


1. Info : Type
2. T : Type
3. G : es:EO+(Info) ⟶ E ⟶ bag(T)
4. F : es:EO+(Info) ⟶ e':E ⟶ T ⟶ {e:E| (e' <loc e)}  ⟶ bag(T)
5. X : EClass(T)
6. ∀es:EO+(Info). ∀e:E.
     ((X es e) = if e ∈b prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi  ∈ bag(T))
7. RecClass(first e
              G[es;e]
            or next e after e' with value v
                F[es;e';v;e]) ∈ EClass(T)
8. es : EO+(Info)
9. e : E@i
10. Z : EClass(T)@i'
11. ∀e1:E. ((e1 < e) ⇒ ((X es e1) = (Z es e1) ∈ bag(T)))@i
12. ↑e ∈b prior(Z)
13. ↑e ∈b prior(X)
14. e' : E@i
15. (prior(X)(e) <loc e') ∨ (prior(Z)(e) <loc e')@i
16. (e' <loc e)@i
17. ↑e' ∈b Z@i
⊢ ↑e' ∈b X
BY
{ (All (RepUR ``in-eclass``) THEN RWO "-7 -7<" (-1) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  T  :  Type
3.  G  :  es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  bag(T)
4.  F  :  es:EO+(Info)  {}\mrightarrow{}  e':E  {}\mrightarrow{}  T  {}\mrightarrow{}  \{e:E|  (e'  <loc  e)\}    {}\mrightarrow{}  bag(T)
5.  X  :  EClass(T)
6.  \mforall{}es:EO+(Info).  \mforall{}e:E.
          ((X  es  e)  =  if  e  \mmember{}\msubb{}  prior(X)  then  let  e'  =  prior(X)(e)  in  F[es;e';X(e');e]  else  G[es;e]  fi  )
7.  RecClass(first  e
                            G[es;e]
                        or  next  e  after  e'  with  value  v
                                F[es;e';v;e])  \mmember{}  EClass(T)
8.  es  :  EO+(Info)
9.  e  :  E@i
10.  Z  :  EClass(T)@i'
11.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  ((X  es  e1)  =  (Z  es  e1)))@i
12.  \muparrow{}e  \mmember{}\msubb{}  prior(Z)
13.  \muparrow{}e  \mmember{}\msubb{}  prior(X)
14.  e'  :  E@i
15.  (prior(X)(e)  <loc  e')  \mvee{}  (prior(Z)(e)  <loc  e')@i
16.  (e'  <loc  e)@i
17.  \muparrow{}e'  \mmember{}\msubb{}  Z@i
\mvdash{}  \muparrow{}e'  \mmember{}\msubb{}  X


By

---

Latex:
(All  (RepUR  ``in-eclass``)  THEN  RWO  "-7  -7<"  (-1)  THEN  Auto)\mcdot{}

---

Home Index