Step * 1 2 of Lemma es-interval-eq


1. es EO
2. E
3. filter(λev.e ≤loc ev;before(e)) [] ∈ (E List)
⊢ filter(λev.e ≤loc ev;before(e)) []
BY
((((MoveToConcl (-1)) THEN (GenConclAtAddr [1; 2])) THENA Auto) THEN (Thin (-1))) }

1
1. es EO
2. E
3. List@i
⊢ (v [] ∈ (E List))  (v [])


Latex:



1.  es  :  EO
2.  e  :  E
3.  filter(\mlambda{}ev.e  \mleq{}loc  ev;before(e))  =  []
\mvdash{}  filter(\mlambda{}ev.e  \mleq{}loc  ev;before(e))  \msim{}  []


By

((((MoveToConcl  (-1))  THEN  (GenConclAtAddr  [1;  2]))  THENA  Auto)  THEN  (Thin  (-1)))




Home Index