Step * 2 1 of Lemma member-es-before


1. the_es EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. E@i
4. ∀k:E. ((k <loc j)  (∀e:E. ((e ∈ before(k)) ⇐⇒ (e <loc k))))@i
5. E@i
6. ¬↑first(j)
7. (e ∈ before(pred(j))) ⇐⇒ (e <loc pred(j))
⊢ (e ∈ before(pred(j))) ∨ (e pred(j) ∈ E) ∨ False ⇐⇒ (¬↑first(j)) ∧ ((e pred(j) ∈ E) ∨ (e <loc pred(j)))
BY
(Auto
   THEN SplitOrHyps
   THEN ThinTrivial
   THEN Try (((OrRight THENA Auto) THEN Trivial))
   THEN Try (((OrLeft THENA Auto) THEN Trivial))
   THEN Try ((((OrRight THENM OrLeft) THENA Auto) THEN Trivial))) }


Latex:


Latex:

1.  the$_{es}$  :  EO@i'
2.  WellFnd\{i\}(E;x,y.(x  <loc  y))
3.  j  :  E@i
4.  \mforall{}k:E.  ((k  <loc  j)  {}\mRightarrow{}  (\mforall{}e:E.  ((e  \mmember{}  before(k))  \mLeftarrow{}{}\mRightarrow{}  (e  <loc  k))))@i
5.  e  :  E@i
6.  \mneg{}\muparrow{}first(j)
7.  (e  \mmember{}  before(pred(j)))  \mLeftarrow{}{}\mRightarrow{}  (e  <loc  pred(j))
\mvdash{}  (e  \mmember{}  before(pred(j)))  \mvee{}  (e  =  pred(j))  \mvee{}  False
\mLeftarrow{}{}\mRightarrow{}  (\mneg{}\muparrow{}first(j))  \mwedge{}  ((e  =  pred(j))  \mvee{}  (e  <loc  pred(j)))


By


Latex:
(Auto
  THEN  SplitOrHyps
  THEN  ThinTrivial
  THEN  Try  (((OrRight  THENA  Auto)  THEN  Trivial))
  THEN  Try  (((OrLeft  THENA  Auto)  THEN  Trivial))
  THEN  Try  ((((OrRight  THENM  OrLeft)  THENA  Auto)  THEN  Trivial)))




Home Index