---

Step * of Lemma primed-class-opt-exists

∀[Info,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(B)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E].
  ((↓∃x:B. x ↓∈ init loc(e)) ⇒ (↓∃b:B. b ∈ Prior(X)?init(e)))
BY
{ ((UnivCD THENA Auto)
   THEN MoveToConcl (-2)
   THEN CausalInd'
   THEN Unfold `classrel` 0
   THEN (RWO "primed-class-opt-cases" 0 THENA Auto)
   THEN (SplitOnConclITE THENA Auto)
   THEN Auto
   THEN SquashExRepD
   THEN Try (Complete ((D 0 THEN InstConcl [⌜x⌝]⋅ THEN Auto)))
   THEN (SplitOnConclITE THENA Auto)
   THEN Try (Complete ((BLemma `bag-size-bag-member` THEN Auto)))
   THEN (InstHyp [⌜pred(e)⌝] (-5)⋅ THENA Auto)) }

1
1. Info : Type
2. B : Type
3. es : EO+(Info)
4. X : EClass(B)
5. init : Id ⟶ bag(B)
6. e : E@i
7. ∀e1:E. ((e1 < e) ⇒ (↓∃x:B. x ↓∈ init loc(e1)) ⇒ (↓∃b:B. b ∈ Prior(X)?init(e1)))
8. ¬↑first(e)
9. x : B@i
10. x ↓∈ init loc(e)@i
11. #(X es pred(e)) ≤ 0
12. ↓∃b:B. b ∈ Prior(X)?init(pred(e))
⊢ ↓∃b:B. b ↓∈ Prior(X)?init es pred(e)

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(B)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[e:E].
    ((\mdownarrow{}\mexists{}x:B.  x  \mdownarrow{}\mmember{}  init  loc(e))  {}\mRightarrow{}  (\mdownarrow{}\mexists{}b:B.  b  \mmember{}  Prior(X)?init(e)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  CausalInd'
  THEN  Unfold  `classrel`  0
  THEN  (RWO  "primed-class-opt-cases"  0  THENA  Auto)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Auto
  THEN  SquashExRepD
  THEN  Try  (Complete  ((D  0  THEN  InstConcl  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)))
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Complete  ((BLemma  `bag-size-bag-member`  THEN  Auto)))
  THEN  (InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto))

---

Home Index