---

Step * 1 1 3 4 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. ¬↑e ∈b prior(X)
11. Z : EClass(T)@i'
12. ¬↑e ∈b prior(Z)
13. ∀e1:E. ((e1 < e) ⇒ ((X es e1) = (Z es e1) ∈ bag(T)))@i
14. (X es e) = G[es;e] ∈ bag(T)
⊢ G[es;e] = G[es;e] ∈ bag(T)
BY
{ 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.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  prior(X)
11.  Z  :  EClass(T)@i'
12.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  prior(Z)
13.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  ((X  es  e1)  =  (Z  es  e1)))@i
14.  (X  es  e)  =  G[es;e]
\mvdash{}  G[es;e]  =  G[es;e]


By

---

Latex:
Auto

---

Home Index