---

Step * 1 of Lemma retracer_wf


1. Info : Type
2. es : EO+(Info)
3. Q : E ⟶ E ⟶ ℙ
4. X : EClass(Top)
5. p1 : ∀e,e':E.  ((Q e e') ⇒ ((↑e ∈b X) ∧ (↑e' ∈b X)))
6. p3 : ∀e,e':E(X).  ((Q e e') ∨ (e = e' ∈ E) ∨ (Q e' e))
7. p4 : ∀e':E. ∃L:E List. ((∀e:E. ((e ∈ L) ⇐⇒ Q e e')) ∧ (∀e1,e2:E.  (e1 before e2 ∈ L ⇒ (Q e1 e2))))
8. e' : E@i
9. L : E List@i
10. v2 : ∀e:E. ((e ∈ L) ⇐⇒ Q e e')@i
11. v3 : ∀e1,e2:E.  (e1 before e2 ∈ L ⇒ (Q e1 e2))@i
12. (p4 e') = <L, v2, v3> ∈ (∃L:E List. ((∀e:E. ((e ∈ L) ⇐⇒ Q e e')) ∧ (∀e1,e2:E.  (e1 before e2 ∈ L ⇒ (Q e1 e2)))))@i
13. i : ℕ||L||@i
⊢ ↑L[i] ∈b X
BY
{ ((Assert Q L[i] e' BY (BHyp -4  THEN Auto)) THEN (InstHyp [⌜L[i]⌝; ⌜e'⌝] 5)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  Q  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
4.  X  :  EClass(Top)
5.  p1  :  \mforall{}e,e':E.    ((Q  e  e')  {}\mRightarrow{}  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\muparrow{}e'  \mmember{}\msubb{}  X)))
6.  p3  :  \mforall{}e,e':E(X).    ((Q  e  e')  \mvee{}  (e  =  e')  \mvee{}  (Q  e'  e))
7.  p4  :  \mforall{}e':E
                    \mexists{}L:E  List.  ((\mforall{}e:E.  ((e  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  Q  e  e'))  \mwedge{}  (\mforall{}e1,e2:E.    (e1  before  e2  \mmember{}  L  {}\mRightarrow{}  (Q  e1  e2))))
8.  e'  :  E@i
9.  L  :  E  List@i
10.  v2  :  \mforall{}e:E.  ((e  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  Q  e  e')@i
11.  v3  :  \mforall{}e1,e2:E.    (e1  before  e2  \mmember{}  L  {}\mRightarrow{}  (Q  e1  e2))@i
12.  (p4  e')  =  <L,  v2,  v3>@i
13.  i  :  \mBbbN{}||L||@i
\mvdash{}  \muparrow{}L[i]  \mmember{}\msubb{}  X


By

---

Latex:
((Assert  Q  L[i]  e'  BY  (BHyp  -4    THEN  Auto))  THEN  (InstHyp  [\mkleeneopen{}L[i]\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{}]  5)\mcdot{}  THEN  Auto)

---

Home Index