---

Step * of Lemma is-rec-class

∀[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.
    (↑e ∈b RecClass(first e
                      G[es;e]
                    or next e after e' with value v
                        F[es;e';v;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
                 #(F[es;e';RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e])(e');e]) = 1 ∈ ℤ
        else #(G[es;e]) = 1 ∈ ℤ
        fi )
BY
{ WithCumulativity((RepeatFor 6 ((D 0 THENA Auto))
                    THEN RW (AddrC [1] (RecUnfoldC `es-rec-class`)) 0
                    THEN RepUR ``in-eclass`` 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 (GenConcl ⌜(prior(X) es e) = B ∈ bag(E(X))⌝⋅
                          THENA (Auto
                                 THEN (InstLemma `es-prior-interface_wf` [⌜Info⌝;⌜X⌝]⋅ THENA Auto)
                                 THEN Unfold `eclass` -1
                                 THEN Auto)
                          )
                    THEN Try ((AutoSplit THEN RepUR ``let`` 0)))) }

1
1. [Info] : Type
2. [T] : Type
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'
8. B : bag(E(X))@i
9. (prior(X) es e) = B ∈ bag(E(X))@i
10. #(B) = 1 ∈ ℤ
⊢ ↑(#(F[es;prior(X)(e);X(prior(X)(e));e]) =z 1) ⇐⇒ #(F[es;prior(X)(e);X(prior(X)(e));e]) = 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.
        (\muparrow{}e  \mmember{}\msubb{}  RecClass(first  e
                                            G[es;e]
                                        or  next  e  after  e'  with  value  v
                                                F[es;e';v;e])
        \mLeftarrow{}{}\mRightarrow{}  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
                                  \#(F[es;e';RecClass(first  e
                                                                            G[es;e]
                                                                        or  next  e  after  e'  with  value  v
                                                                                F[es;e';v;e])(e');e])
                                  =  1
                else  \#(G[es;e])  =  1
                fi  )


By

---

Latex:
WithCumulativity((RepeatFor  6  ((D  0  THENA  Auto))
                                    THEN  RW  (AddrC  [1]  (RecUnfoldC  `es-rec-class`))  0
                                    THEN  RepUR  ``in-eclass``  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
                                                )\mcdot{}
                                    THEN  All  Thin
                                    THEN  (GenConcl  \mkleeneopen{}(prior(X)  es  e)  =  B\mkleeneclose{}\mcdot{}
                                                THENA  (Auto
                                                              THEN  (InstLemma  `es-prior-interface\_wf`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                                              THEN  Unfold  `eclass`  -1
                                                              THEN  Auto)
                                                )
                                    THEN  Try  ((AutoSplit  THEN  RepUR  ``let``  0))))

---

Home Index