---

Step * 1 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))
⊢ X = RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) ∈ EClass(T)
BY
{ ((InstLemma `es-rec-class_wf` [⌈Info⌉;⌈T⌉;⌈G⌉;⌈F⌉]⋅ THENA Auto)
   THEN (Unfold `eclass` 0
         THEN (ExtWith [`es'] [⌈es:EO+(Info) ─→ e:E ─→ bag(T)⌉]⋅ THENA Auto)
         THEN (ExtWith [`e'] [⌈e:E ─→ bag(T)⌉]⋅ THENA Auto))
   THEN MoveToConcl (-1)
   THEN CausalInd'
   THEN (RecUnfold `es-rec-class` 0 THEN Reduce 0)⋅
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [2;3;1;2;1]
   THEN Thin (-1)
   THEN RenameVar `Z' (-1)
   THEN Auto)⋅ }

1
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
⊢ (X es e) = if e ∈b prior(Z) then let e' = prior(Z)(e) in F[es;e';Z(e');e] else G[es;e] fi  ∈ bag(T)

---

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  )
\mvdash{}  X  =  RecClass(first  e    G[es;e]or  next  e  after  e'  with  value  v        F[es;e';v;e])


By

---

Latex:
((InstLemma  `es-rec-class\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Unfold  `eclass`  0
              THEN  (ExtWith  [`es']  [\mkleeneopen{}es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(T)\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (ExtWith  [`e']  [\mkleeneopen{}e:E  {}\mrightarrow{}  bag(T)\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  MoveToConcl  (-1)
  THEN  CausalInd'
  THEN  (RecUnfold  `es-rec-class`  0  THEN  Reduce  0)\mcdot{}
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [2;3;1;2;1]
  THEN  Thin  (-1)
  THEN  RenameVar  `Z'  (-1)
  THEN  Auto)\mcdot{}

---

Home Index