---

Step * 1 of Lemma run_local_pred_time


1. M : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
⊢ (fst(run-local-pred(r;e2;e1;e1))) ≤ e1
BY
{ ((Assert ∀t:ℕ. ((t ≤ e1) ⇒ ((fst(run-local-pred(r;e2;e1;t))) ≤ e1)) BY
          (InductionOnNat
           THEN RecUnfold `run-local-pred` 0
           THEN (Reduce 0 THEN Auto)
           THEN AutoSplit
           THEN (CallByValueReduce 0 THENA Auto)
           THEN AutoSplit))
   THEN Auto
   ) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])@i
3.  e1  :  \mBbbN{}@i
4.  e2  :  Id@i
\mvdash{}  (fst(run-local-pred(r;e2;e1;e1)))  \mleq{}  e1


By

---

Latex:
((Assert  \mforall{}t:\mBbbN{}.  ((t  \mleq{}  e1)  {}\mRightarrow{}  ((fst(run-local-pred(r;e2;e1;t)))  \mleq{}  e1))  BY
                (InductionOnNat
                  THEN  RecUnfold  `run-local-pred`  0
                  THEN  (Reduce  0  THEN  Auto)
                  THEN  AutoSplit
                  THEN  (CallByValueReduce  0  THENA  Auto)
                  THEN  AutoSplit))
  THEN  Auto
  )

---

Home Index