---

Step * of Lemma once-classrel

∀[Info,A:Type]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].  ∀v:A. uiff(v ∈ (X once)(e);(no X prior to e) ∧ v ∈ X(e))
BY
{ (Unfold `no-prior-classrel` 0
   THEN ((UnivCD THENA Auto)
         THEN D 0
         THEN (D 0 THENA Auto)
         THEN RepUR ``alle-lt`` 0
         THEN Try (Complete (Auto))
         THEN All (Unfold `once-class`)⋅
         THEN InstLemma `until-classrel` [⌈Info⌉;⌈A⌉;⌈A⌉;⌈X⌉;⌈X⌉;⌈es⌉;⌈e⌉;⌈v⌉]⋅
         THEN Auto
         THEN BHyp (-1)
         THEN Auto)
   ) }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    \mforall{}v:A.  uiff(v  \mmember{}  (X  once)(e);(no  X  prior  to  e)  \mwedge{}  v  \mmember{}  X(e))


By

---

Latex:
(Unfold  `no-prior-classrel`  0
  THEN  ((UnivCD  THENA  Auto)
              THEN  D  0
              THEN  (D  0  THENA  Auto)
              THEN  RepUR  ``alle-lt``  0
              THEN  Try  (Complete  (Auto))
              THEN  All  (Unfold  `once-class`)\mcdot{}
              THEN  InstLemma  `until-classrel`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
              THEN  Auto
              THEN  BHyp  (-1)
              THEN  Auto)
  )

---

Home Index