---

Step * 1 of Lemma es-rec-class_wf


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. es : EO+(Info)
6. e : E@i
7. ∀e1:E. ((e1 < e) ⇒ (RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e1 ∈ bag(T)))
⊢ if (#(case last(λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =z 1)) e
      of inl(e') =>
      {e'}
      | inr(x) =>
      {}) =z 1)
  then F[es;only(case last(λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =z 1)) 
                      e
        of inl(e') =>
        {e'}
        | inr(x) =>
        {});only(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es 
                 only(case last(λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es 
                                      e) =z 1)) 
                           e
                  of inl(e') =>
                  {e'}
                  | inr(x) =>
                  {}));e]
  else G[es;e]
  fi  ∈ bag(T)
BY
{ ((GenConclAtAddr [2;1;1;1;1] THENM (Reduce (-2) THEN D -2 THEN Reduce 0 THEN Try (Complete (Auto))))
   THENA (Try (BLemma `es-local-pred_wf2`) THEN Auto THEN GenConclAtAddrType ⌈bag(T)⌉ [2;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. es : EO+(Info)
6. e : E@i
7. ∀e1:E. ((e1 < e) ⇒ (RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e1 ∈ bag(T)))
8. x : ∃e':{E| ((e' <loc e)
               ∧ (↑(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e') =z 1))
               ∧ (∀e'':E
                    ((e' <loc e'')
                    ⇒ (e'' <loc e)
                    ⇒ (¬↑(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es 
                             e'') =z 1)))))}@i
9. (last(λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =z 1)) e)
= (inl x)
∈ ((∃e':{E| ((e' <loc e)
            ∧ (↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =z 1)) e'))
            ∧ (∀e'':E
                 ((e' <loc e'')
                 ⇒ (e'' <loc e)
                 ⇒ (¬↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =z 1)) 
                        e'')))))})
  ∨ (¬(∃e':{E| ((e' <loc e)
               ∧ (↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =z 1)) 
                    e')))})))@i
⊢ F[es;x;only(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es x);e] ∈ 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.  es  :  EO+(Info)
6.  e  :  E@i
7.  \mforall{}e1:E
          ((e1  <  e)
          {}\mRightarrow{}  (RecClass(first  e    G[es;e]or  next  e  after  e'  with  value  v        F[es;e';v;e])  es  e1  \mmember{}  bag(T)))
\mvdash{}  if  (\#(case  last(\mlambda{}e.(\#(RecClass(first  e
                                                                      G[es;e]
                                                                  or  next  e  after  e'  with  value  v
                                                                          F[es;e';v;e]) 
                                                es 
                                                e)  =\msubz{}  1)) 
                          e
            of  inl(e')  =>
            \{e'\}
            |  inr(x)  =>
            \{\})  =\msubz{}  1)
    then  F[es;only(case  last(\mlambda{}e.(\#(RecClass(first  e
                                                                                        G[es;e]
                                                                                    or  next  e  after  e'  with  value  v
                                                                                            F[es;e';v;e]) 
                                                                  es 
                                                                  e)  =\msubz{}  1)) 
                                            e
                of  inl(e')  =>
                \{e'\}
                |  inr(x)  =>
                \{\});only(RecClass(first  e    G[es;e]or  next  e  after  e'  with  value  v        F[es;e';v;e])  es 
                                  only(case  last(\mlambda{}e.(\#(RecClass(first  e
                                                                                                  G[es;e]
                                                                                              or  next  e  after  e'  with  value  v
                                                                                                      F[es;e';v;e]) 
                                                                            es 
                                                                            e)  =\msubz{}  1)) 
                                                      e
                                    of  inl(e')  =>
                                    \{e'\}
                                    |  inr(x)  =>
                                    \{\}));e]
    else  G[es;e]
    fi    \mmember{}  bag(T)


By

---

Latex:
((GenConclAtAddr  [2;1;1;1;1]  THENM  (Reduce  (-2)  THEN  D  -2  THEN  Reduce  0  THEN  Try  (Complete  (Auto))))
  THENA  (Try  (BLemma  `es-local-pred\_wf2`)
                THEN  Auto
                THEN  GenConclAtAddrType  \mkleeneopen{}bag(T)\mkleeneclose{}  [2;1]\mcdot{}
                THEN  Auto)\mcdot{}
  )

---

Home Index