---

Step * of Lemma primed-class-opt-classrel

∀[T,Info:Type]. ∀[X:EClass(T)]. ∀[init:Id ⟶ bag(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].
  uiff(v ∈ Prior(X)?init(e);↓(∃e':E. ((es-p-local-pred(es;λe'.(↓∃w:T. w ∈ X(e'))) e e') ∧ v ∈ X(e')))
                             ∨ ((∀e':E. ((e' <loc e) ⇒ (∀w:T. (¬w ∈ X(e'))))) ∧ v ↓∈ init loc(e)))
BY
{ ((UnivCD THENA Auto)
   THEN Try ((Unhide THENA Auto))
   THEN RepUR ``primed-class-opt classrel`` 0
   THEN (GenConcl ⌜(λe'.0 <z #(X es e')) = P ∈ (E ⟶ 𝔹)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(λe'.(↓∃w:T. w ↓∈ X es e')) = Q ∈ (E ⟶ ℙ)⌝⋅ THENA Auto)
   THEN (InstLemma `es-local-pred-cases` [⌜Info⌝;⌜es⌝;⌜e⌝]⋅ THENA Auto)
   THEN (SimpleInstHyp ⌜P⌝ (-1)⋅ THENA Auto)
   THEN Thin (-2)
   THEN MoveToConcl (-1)
   THEN RepUR ``can-apply do-apply`` 0
   THEN GenConclAtAddr [2;1;3;1]
   THEN D (-2)
   THEN Reduce 0
   THEN (D 0 THENA Auto)⋅) }

1
1. T : Type
2. Info : Type
3. X : EClass(T)
4. init : Id ⟶ bag(T)
5. es : EO+(Info)
6. e : E
7. v : T
8. P : E ⟶ 𝔹@i
9. (λe'.0 <z #(X es e')) = P ∈ (E ⟶ 𝔹)@i
10. Q : E ⟶ ℙ@i'
11. (λe'.(↓∃w:T. w ↓∈ X es e')) = Q ∈ (E ⟶ ℙ)@i'
12. x : ∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))}@i
13. (last(P) e)
= (inl x)
∈ ((∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))})
  ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))})))@i
14. (¬↑first(e))
    ∧ (((↑(P pred(e))) ∧ (x = pred(e) ∈ E))
      ∨ ((¬↑(P pred(e))) ∧ (↑isl(last(P) pred(e))) ∧ (x = outl(last(P) pred(e)) ∈ E))) 
    supposing True@i
⊢ uiff(v ↓∈ X es x;↓(∃e':E. ((es-p-local-pred(es;Q) e e') ∧ v ↓∈ X es e'))
                    ∨ ((∀e':E. ((e' <loc e) ⇒ (∀w:T. (¬w ↓∈ X es e')))) ∧ v ↓∈ init loc(e)))

2
1. T : Type
2. Info : Type
3. X : EClass(T)
4. init : Id ⟶ bag(T)
5. es : EO+(Info)
6. e : E
7. v : T
8. P : E ⟶ 𝔹@i
9. (λe'.0 <z #(X es e')) = P ∈ (E ⟶ 𝔹)@i
10. Q : E ⟶ ℙ@i'
11. (λe'.(↓∃w:T. w ↓∈ X es e')) = Q ∈ (E ⟶ ℙ)@i'
12. y : ¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))})@i
13. (last(P) e)
= (inr y )
∈ ((∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))})
  ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))})))@i
14. (¬↑first(e))
    ∧ (((↑(P pred(e))) ∧ (⊥ = pred(e) ∈ E))
      ∨ ((¬↑(P pred(e))) ∧ (↑isl(last(P) pred(e))) ∧ (⊥ = outl(last(P) pred(e)) ∈ E))) 
    supposing False@i
⊢ uiff(v ↓∈ init loc(e);↓(∃e':E. ((es-p-local-pred(es;Q) e e') ∧ v ↓∈ X es e'))
                         ∨ ((∀e':E. ((e' <loc e) ⇒ (∀w:T. (¬w ↓∈ X es e')))) ∧ v ↓∈ init loc(e)))

---

Latex:

---

Latex:
\mforall{}[T,Info:Type].  \mforall{}[X:EClass(T)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:T].
    uiff(v  \mmember{}  Prior(X)?init(
                      e);\mdownarrow{}(\mexists{}e':E.  ((es-p-local-pred(es;\mlambda{}e'.(\mdownarrow{}\mexists{}w:T.  w  \mmember{}  X(e')))  e  e')  \mwedge{}  v  \mmember{}  X(e')))
                              \mvee{}  ((\mforall{}e':E.  ((e'  <loc  e)  {}\mRightarrow{}  (\mforall{}w:T.  (\mneg{}w  \mmember{}  X(e')))))  \mwedge{}  v  \mdownarrow{}\mmember{}  init  loc(e)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Try  ((Unhide  THENA  Auto))
  THEN  RepUR  ``primed-class-opt  classrel``  0
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}e'.0  <z  \#(X  es  e'))  =  P\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}e'.(\mdownarrow{}\mexists{}w:T.  w  \mdownarrow{}\mmember{}  X  es  e'))  =  Q\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `es-local-pred-cases`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (SimpleInstHyp  \mkleeneopen{}P\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2)
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``can-apply  do-apply``  0
  THEN  GenConclAtAddr  [2;1;3;1]
  THEN  D  (-2)
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)\mcdot{})

---

Home Index