Step
*
2
of Lemma
existse-before-iff
1. es : EO@i'
2. e' : E@i
3. [P] : {e:E| loc(e) = loc(e') ∈ Id} ─→ ℙ
4. e : E@i
5. (e <loc e')@i
6. P[e]@i
⊢ P[pred(e')] ∨ (∃e:E. ((e <loc pred(e')) c∧ P[e]))
BY
{ OnMaybeHyp 5 (\h. (RWO "es-locl-iff" h
THEN Auto
THEN (ParallelOp (h+1))
THEN Auto
THEN Try (((InstConcl [⌈e⌉])⋅ THEN Auto))
THEN (StrongRevHypSubst (h+1) 0)
THEN Auto)) }
Latex:
1. es : EO@i'
2. e' : E@i
3. [P] : \{e:E| loc(e) = loc(e')\} {}\mrightarrow{} \mBbbP{}
4. e : E@i
5. (e <loc e')@i
6. P[e]@i
\mvdash{} P[pred(e')] \mvee{} (\mexists{}e:E. ((e <loc pred(e')) c\mwedge{} P[e]))
By
OnMaybeHyp 5 (\mbackslash{}h. (RWO "es-locl-iff" h
THEN Auto
THEN (ParallelOp (h+1))
THEN Auto
THEN Try (((InstConcl [\mkleeneopen{}e\mkleeneclose{}])\mcdot{} THEN Auto))
THEN (StrongRevHypSubst (h+1) 0)
THEN Auto))
Home
Index