Step
*
1
1
1
1
1
2
1
of Lemma
es-pplus-first-since
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [Q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. ∀e:{e:E| loc(e) = loc(e1) ∈ Id} . Dec(Q[e])@i
6. e1 ≤loc e2 @i
7. Q[e2]@i
8. d : ℕ
9. ∀d:ℕd. ∀e,e':E.
     ((loc(e) = loc(e1) ∈ Id) 
⇒ (||[e, e']|| ≤ d) 
⇒ e ≤loc e'  
⇒ Q[e'] 
⇒ [e,e']~([a,b].b = first e ≥ a.Q[e])+)@i
10. e : E@i
11. e' : E@i
12. loc(e) = loc(e1) ∈ Id@i
13. ||[e, e']|| ≤ d@i
14. e ≤loc e' @i
15. Q[e']@i
16. a : E
17. e ≤loc a 
18. (a <loc e')
19. Q[a]
20. b : E
21. ¬↑first(b)
22. a = pred(b) ∈ E
23. b ≤loc e' 
⊢ [e,e']~([a,b].b = first e ≥ a.Q[e])+
BY
{ ((Assert (pred(b) <loc b) BY
          Auto)
   THEN (Assert (e <loc b) BY
               Auto)
   THEN ((InstLemma `es-interval-partition` [⌈es⌉; ⌈e'⌉; ⌈e⌉; ⌈b⌉])⋅ THENA Auto)
   THEN ((RevHypSubst (-5) (-1)) THENA Auto)) }
1
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [Q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. ∀e:{e:E| loc(e) = loc(e1) ∈ Id} . Dec(Q[e])@i
6. e1 ≤loc e2 @i
7. Q[e2]@i
8. d : ℕ
9. ∀d:ℕd. ∀e,e':E.
     ((loc(e) = loc(e1) ∈ Id) 
⇒ (||[e, e']|| ≤ d) 
⇒ e ≤loc e'  
⇒ Q[e'] 
⇒ [e,e']~([a,b].b = first e ≥ a.Q[e])+)@i
10. e : E@i
11. e' : E@i
12. loc(e) = loc(e1) ∈ Id@i
13. ||[e, e']|| ≤ d@i
14. e ≤loc e' @i
15. Q[e']@i
16. a : E
17. e ≤loc a 
18. (a <loc e')
19. Q[a]
20. b : E
21. ¬↑first(b)
22. a = pred(b) ∈ E
23. b ≤loc e' 
24. (pred(b) <loc b)
25. (e <loc b)
26. [e, e'] = ([e, a] @ [b, e']) ∈ (E List)
⊢ [e,e']~([a,b].b = first e ≥ a.Q[e])+
Latex:
1.  es  :  EO@i'
2.  e1  :  E@i
3.  e2  :  \{e:E|  loc(e)  =  loc(e1)\}  @i
4.  [Q]  :  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}e:\{e:E|  loc(e)  =  loc(e1)\}  .  Dec(Q[e])@i
6.  e1  \mleq{}loc  e2  @i
7.  Q[e2]@i
8.  d  :  \mBbbN{}
9.  \mforall{}d:\mBbbN{}d.  \mforall{}e,e':E.
          ((loc(e)  =  loc(e1))
          {}\mRightarrow{}  (||[e,  e']||  \mleq{}  d)
          {}\mRightarrow{}  e  \mleq{}loc  e' 
          {}\mRightarrow{}  Q[e']
          {}\mRightarrow{}  [e,e']\msim{}([a,b].b  =  first  e  \mgeq{}  a.Q[e])+)@i
10.  e  :  E@i
11.  e'  :  E@i
12.  loc(e)  =  loc(e1)@i
13.  ||[e,  e']||  \mleq{}  d@i
14.  e  \mleq{}loc  e'  @i
15.  Q[e']@i
16.  a  :  E
17.  e  \mleq{}loc  a 
18.  (a  <loc  e')
19.  Q[a]
20.  b  :  E
21.  \mneg{}\muparrow{}first(b)
22.  a  =  pred(b)
23.  b  \mleq{}loc  e' 
\mvdash{}  [e,e']\msim{}([a,b].b  =  first  e  \mgeq{}  a.Q[e])+
By
((Assert  (pred(b)  <loc  b)  BY
                Auto)
  THEN  (Assert  (e  <loc  b)  BY
                          Auto)
  THEN  ((InstLemma  `es-interval-partition`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((RevHypSubst  (-5)  (-1))  THENA  Auto))
Home
Index