---

Step * of Lemma rec-class-val

∀[Info,T:Type]. ∀[G:es:EO+(Info) ⟶ E ⟶ bag(T)]. ∀[F:es:EO+(Info) ⟶ e':E ⟶ T ⟶ {e:E| (e' <loc e)}  ⟶ bag(T)].
∀[es:EO+(Info)]. ∀[e:E].
  RecClass(first e
             G[es;e]
           or next e after e' with value v
               F[es;e';v;e])(e)
  = if e ∈b prior(RecClass(first e
                             G[es;e]
                           or next e after e' with value v
                               F[es;e';v;e]))
    then let e' = prior(RecClass(first e
                                   G[es;e]
                                 or next e after e' with value v
                                     F[es;e';v;e]))(e) in
             only(F[es;e';RecClass(first e
                                     G[es;e]
                                   or next e after e' with value v
                                       F[es;e';v;e])(e');e])
    else only(G[es;e])
    fi 
  ∈ T 
  supposing ↑e ∈b RecClass(first e
                             G[es;e]
                           or next e after e' with value v
                               F[es;e';v;e])
BY
{ WithCumulativity (RemoveUniform Auto ((InstLemma `es-rec-class_wf` [⌜Info⌝;⌜T⌝;⌜G⌝;⌜F⌝]⋅ THEN Auto))⋅
                    THEN RepeatFor 6 ((D 0 THENA Auto))
                    THEN RW (AddrC [1] (RecUnfoldC `es-rec-class`)) 0⋅
                    THEN RW (AddrC [2;2] (RecUnfoldC `es-rec-class`)) 0⋅
                    THEN RepUR ``in-eclass eclass-val can-apply do-apply let`` 0
                    THEN (GenConcl ⌜RecClass(first e
                                               G[es;e]
                                             or next e after e' with value v
                                                 F[es;e';v;e])
                                    = X
                                    ∈ EClass(T)⌝⋅
                          THENA Auto
                          )
                    THEN All Thin
                    THEN Fold `eclass-val` 0)⋅ }

1
1. Info : Type@i'
2. T : Type@i'
3. G : es:EO+(Info) ⟶ E ⟶ bag(T)@i'
4. F : es:EO+(Info) ⟶ e':E ⟶ T ⟶ {e:E| (e' <loc e)}  ⟶ bag(T)@i'
5. es : EO+(Info)@i'
6. e : E@i
7. X : EClass(T)@i'
⊢ only(if (#(prior(X) es e) =z 1) then F[es;prior(X)(e);X(prior(X)(e));e] else G[es;e] fi )
  = if (#(prior(X) es e) =z 1) then only(F[es;prior(X)(e);X(prior(X)(e));e]) else only(G[es;e]) fi 
  ∈ T 
  supposing ↑(#(if (#(prior(X) es e) =z 1) then F[es;prior(X)(e);X(prior(X)(e));e] else G[es;e] fi ) =z 1)

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[G:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  bag(T)].  \mforall{}[F:es:EO+(Info)
                                                                                                            {}\mrightarrow{}  e':E
                                                                                                            {}\mrightarrow{}  T
                                                                                                            {}\mrightarrow{}  \{e:E|  (e'  <loc  e)\} 
                                                                                                            {}\mrightarrow{}  bag(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    RecClass(first  e
                          G[es;e]
                      or  next  e  after  e'  with  value  v
                              F[es;e';v;e])(e)
    =  if  e  \mmember{}\msubb{}  prior(RecClass(first  e
                                                          G[es;e]
                                                      or  next  e  after  e'  with  value  v
                                                              F[es;e';v;e]))
        then  let  e'  =  prior(RecClass(first  e
                                                                      G[es;e]
                                                                  or  next  e  after  e'  with  value  v
                                                                          F[es;e';v;e]))(e)  in
                          only(F[es;e';RecClass(first  e
                                                                          G[es;e]
                                                                      or  next  e  after  e'  with  value  v
                                                                              F[es;e';v;e])(e');e])
        else  only(G[es;e])
        fi   
    supposing  \muparrow{}e  \mmember{}\msubb{}  RecClass(first  e
                                                          G[es;e]
                                                      or  next  e  after  e'  with  value  v
                                                              F[es;e';v;e])


By

---

Latex:
WithCumulativity  (RemoveUniform  Auto  ((InstLemma  `es-rec-class\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THEN  Auto))
                                    \mcdot{}
                                    THEN  RepeatFor  6  ((D  0  THENA  Auto))
                                    THEN  RW  (AddrC  [1]  (RecUnfoldC  `es-rec-class`))  0\mcdot{}
                                    THEN  RW  (AddrC  [2;2]  (RecUnfoldC  `es-rec-class`))  0\mcdot{}
                                    THEN  RepUR  ``in-eclass  eclass-val  can-apply  do-apply  let``  0
                                    THEN  (GenConcl  \mkleeneopen{}RecClass(first  e
                                                                                          G[es;e]
                                                                                      or  next  e  after  e'  with  value  v
                                                                                              F[es;e';v;e])
                                                                    =  X\mkleeneclose{}\mcdot{}
                                                THENA  Auto
                                                )
                                    THEN  All  Thin
                                    THEN  Fold  `eclass-val`  0)\mcdot{}

---

Home Index