Step * 1 1 1 1 1 of Lemma global-eo-before


1. (Id × Top) List
2. : ℕ
3. ∀n:ℕn. (n < ||L||  (before(n) filter(λn@0.loc(n@0) loc(n);upto(n)) ∈ (ℕList)))
4. n < ||L||@i
5. n ∈ E
6. ↑first(n)
⊢ (∀x∈upto(n).¬↑loc(x) loc(n))
BY
(RWO "global-eo-first" (-1) THEN Auto) }

1
1. (Id × Top) List
2. : ℕ
3. ∀n:ℕn. (n < ||L||  (before(n) filter(λn@0.loc(n@0) loc(n);upto(n)) ∈ (ℕList)))
4. n < ||L||@i
5. n ∈ E
6. ↑(∀x∈upto(n).¬bloc(x) loc(n))_b
⊢ (∀x∈upto(n).¬↑loc(x) loc(n))


Latex:



Latex:

1.  L  :  (Id  \mtimes{}  Top)  List
2.  n  :  \mBbbN{}
3.  \mforall{}n:\mBbbN{}n.  (n  <  ||L||  {}\mRightarrow{}  (before(n)  =  filter(\mlambda{}n@0.loc(n@0)  =  loc(n);upto(n))))
4.  n  <  ||L||@i
5.  n  \mmember{}  E
6.  \muparrow{}first(n)
\mvdash{}  (\mforall{}x\mmember{}upto(n).\mneg{}\muparrow{}loc(x)  =  loc(n))


By


Latex:
(RWO  "global-eo-first"  (-1)  THEN  Auto)




Home Index