Step
*
1
of Lemma
run_local_pred_maximal
1. M : Type ─→ Type@i'
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
5. ↑is-run-event(r;e1;e2)@i
6. x1 : ℕ@i
7. x2 : Id@i
8. ↑is-run-event(r;x1;x2)@i
9. x1 < e1@i
10. fst(run-local-pred(r;e2;e1;e1)) < x1@i
⊢ ¬(run-event-loc(<x1, x2>) = run-event-loc(<e1, e2>) ∈ Id)
BY
{ (RepUR ``run-event-loc`` 0
THEN (D 0 THENA Auto)
THEN (Assert ⌈∀t:ℕ. (x1 < t
⇒ (x1 ≤ (fst(run-local-pred(r;e2;e1;t)))))⌉⋅ THENM (InstHyp [⌈e1⌉] (-1)⋅ THEN Auto))) }
1
.....assertion.....
1. M : Type ─→ Type@i'
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
5. ↑is-run-event(r;e1;e2)@i
6. x1 : ℕ@i
7. x2 : Id@i
8. ↑is-run-event(r;x1;x2)@i
9. x1 < e1@i
10. fst(run-local-pred(r;e2;e1;e1)) < x1@i
11. x2 = e2 ∈ Id@i
⊢ ∀t:ℕ. (x1 < t
⇒ (x1 ≤ (fst(run-local-pred(r;e2;e1;t)))))
Latex:
Latex:
1. M : Type {}\mrightarrow{} Type@i'
2. r : pRunType(P.M[P])@i
3. e1 : \mBbbN{}@i
4. e2 : Id@i
5. \muparrow{}is-run-event(r;e1;e2)@i
6. x1 : \mBbbN{}@i
7. x2 : Id@i
8. \muparrow{}is-run-event(r;x1;x2)@i
9. x1 < e1@i
10. fst(run-local-pred(r;e2;e1;e1)) < x1@i
\mvdash{} \mneg{}(run-event-loc(<x1, x2>) = run-event-loc(<e1, e2>))
By
Latex:
(RepUR ``run-event-loc`` 0
THEN (D 0 THENA Auto)
THEN (Assert \mkleeneopen{}\mforall{}t:\mBbbN{}. (x1 < t {}\mRightarrow{} (x1 \mleq{} (fst(run-local-pred(r;e2;e1;t)))))\mkleeneclose{}\mcdot{}
THENM (InstHyp [\mkleeneopen{}e1\mkleeneclose{}] (-1)\mcdot{} THEN Auto)
))
Home
Index