Step
*
1
1
1
1
1
2
1
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'
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])+
BY
{ (AssertBY ⌈0 < ||[e, a]||⌉
(BLemma `es-interval-non-zero` THEN Auto)⋅
THEN AssertBY ⌈0 < ||[b, e']||⌉
(BLemma `es-interval-non-zero` THEN Auto)⋅
THEN AssertBY ⌈||[e, e']|| = (||[e, a]|| + ||[b, e']||) ∈ ℤ⌉
(((HypSubst (-3) 0) THENM RWO "length-append" 0) THEN Auto)⋅
THEN (AssertBY ⌈[e,a]~([a,b].b = first e ≥ a.Q[e])+⌉
AllHyps h.((InstHyp [⌈||[e, a]||⌉; ⌈e⌉; ⌈a⌉] h)⋅ THEN Complete (Auto')) )⋅
THEN (AssertBY ⌈[b,e']~([a,b].b = first e ≥ a.Q[e])+⌉
AllHyps h.((InstHyp [⌈||[b, e']||⌉; ⌈b⌉; ⌈e'⌉] h)⋅ THEN Auto' THEN Complete (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)
27. 0 < ||[e, a]||
28. 0 < ||[b, e']||
29. ||[e, e']|| = (||[e, a]|| + ||[b, e']||) ∈ ℤ
30. [e,a]~([a,b].b = first e ≥ a.Q[e])+
31. [b,e']~([a,b].b = first e ≥ a.Q[e])+
⊢ [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'
24. (pred(b) <loc b)
25. (e <loc b)
26. [e, e'] = ([e, a] @ [b, e'])
\mvdash{} [e,e']\msim{}([a,b].b = first e \mgeq{} a.Q[e])+
By
(AssertBY \mkleeneopen{}0 < ||[e, a]||\mkleeneclose{}
(BLemma `es-interval-non-zero` THEN Auto)\mcdot{}
THEN AssertBY \mkleeneopen{}0 < ||[b, e']||\mkleeneclose{}
(BLemma `es-interval-non-zero` THEN Auto)\mcdot{}
THEN AssertBY \mkleeneopen{}||[e, e']|| = (||[e, a]|| + ||[b, e']||)\mkleeneclose{}
(((HypSubst (-3) 0) THENM RWO "length-append" 0) THEN Auto)\mcdot{}
THEN (AssertBY \mkleeneopen{}[e,a]\msim{}([a,b].b = first e \mgeq{} a.Q[e])+\mkleeneclose{}
AllHyps h.((InstHyp [\mkleeneopen{}||[e, a]||\mkleeneclose{}; \mkleeneopen{}e\mkleeneclose{}; \mkleeneopen{}a\mkleeneclose{}] h)\mcdot{} THEN Complete (Auto')) )\mcdot{}
THEN (AssertBY \mkleeneopen{}[b,e']\msim{}([a,b].b = first e \mgeq{} a.Q[e])+\mkleeneclose{}
AllHyps h.((InstHyp [\mkleeneopen{}||[b, e']||\mkleeneclose{}; \mkleeneopen{}b\mkleeneclose{}; \mkleeneopen{}e'\mkleeneclose{}] h)\mcdot{} THEN Auto' THEN Complete (Auto)) )\mcdot{})
Home
Index