---

Step * 1 of Lemma run_local_pred_wf

.....set predicate..... 
1. M : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
5. ↑is-run-event(r;e1;e2)@i
⊢ ↑is-run-event(r;fst(run-local-pred(r;e2;e1;e1));snd(run-local-pred(r;e2;e1;e1)))
BY
{ ((Assert ⌈∀t:ℕ. ((t ≤ e1) ⇒ (↑is-run-event(r;fst(run-local-pred(r;e2;e1;t));snd(run-local-pred(r;e2;e1;t)))))⌉⋅
   THENM (BHyp -1  THEN Auto)
   )
   THEN (D 0 THENA Auto)
   ) }

1
1. M : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
5. ↑is-run-event(r;e1;e2)@i
6. t : ℕ@i
⊢ (t ≤ e1) ⇒ (↑is-run-event(r;fst(run-local-pred(r;e2;e1;t));snd(run-local-pred(r;e2;e1;t))))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])@i
3.  e1  :  \mBbbN{}@i
4.  e2  :  Id@i
5.  \muparrow{}is-run-event(r;e1;e2)@i
\mvdash{}  \muparrow{}is-run-event(r;fst(run-local-pred(r;e2;e1;e1));snd(run-local-pred(r;e2;e1;e1)))


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}t:\mBbbN{}
                        ((t  \mleq{}  e1)
                        {}\mRightarrow{}  (\muparrow{}is-run-event(r;fst(run-local-pred(r;e2;e1;t));snd(run-local-pred(r;e2;e1;t)))))\mkleeneclose{}\mcdot{}
  THENM  (BHyp  -1    THEN  Auto)
  )
  THEN  (D  0  THENA  Auto)
  )

---

Home Index