Step
*
of Lemma
es-causl-swellfnd
∀es:EO. SWellFounded((e < e'))
BY
{ (InstLemma `es-causl-swellfnd-base` []⋅ THEN RepeatFor 5 (ParallelLast)) }
Latex:
\mforall{}es:EO.  SWellFounded((e  <  e'))
By
(InstLemma  `es-causl-swellfnd-base`  []\mcdot{}  THEN  RepeatFor  5  (ParallelLast))
Home
Index