Step
*
1
of Lemma
pes-axioms
1. the_es : EO@i'
β’ Trans(E;e,e'.(e <loc e'))
BY
{ ((InstLemma `es-causl_transitivity` [βthe_esβ]β
THENA Auto)
THEN Fold `trans` (-1)
THEN RepeatFor 6 ((ParallelLast THENA (D -1 THEN Auto)))
THEN D 0
THEN Auto) }
Latex:
1. the$_{es}$ : EO@i'
\mvdash{} Trans(E;e,e'.(e <loc e'))
By
((InstLemma `es-causl\_transitivity` [\mkleeneopen{}the$_{es}$\mkleeneclose{}]\mcdot{} THENA Auto)
THEN Fold `trans` (-1)
THEN RepeatFor 6 ((ParallelLast THENA (D -1 THEN Auto)))
THEN D 0
THEN Auto)
Home
Index