---

Step * of Lemma retracer_wf

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[Q:E ─→ E ─→ ℙ]. ∀[X:EClass(Top)]. ∀[p:retrace(es;Q;X)].
  (retracer(p) ∈ E ─→ (E(X) List))
BY
{ (ProveWfLemma
   THEN (RepeatFor 2 (D (-2)) THEN Reduce 0)
   THEN GenConclAtAddr [2]
   THEN D -2
   THEN Reduce 0
   THEN MemCD
   THEN Try (Trivial)
   THEN Unfold `es-E-interface` 0
   THEN BLemma `list-set-type2`
   THEN Auto
   THEN D 0
   THEN Auto) }

1
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

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[Q:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[X:EClass(Top)].  \mforall{}[p:retrace(es;Q;X)].
    (retracer(p)  \mmember{}  E  {}\mrightarrow{}  (E(X)  List))


By

---

Latex:
(ProveWfLemma
  THEN  (RepeatFor  2  (D  (-2))  THEN  Reduce  0)
  THEN  GenConclAtAddr  [2]
  THEN  D  -2
  THEN  Reduce  0
  THEN  MemCD
  THEN  Try  (Trivial)
  THEN  Unfold  `es-E-interface`  0
  THEN  BLemma  `list-set-type2`
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index