---

Step * 1 of Lemma run_local_pred_loc


1. M : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
⊢ (snd(run-local-pred(r;e2;e1;e1))) = e2 ∈ Id
BY
{ ((Assert ∀t:ℕ. ((snd(run-local-pred(r;e2;e1;t))) = e2 ∈ Id) BY
          (InductionOnNat
           THEN RecUnfold `run-local-pred` 0
           THEN Reduce 0
           THEN ((Fold `member` 0 THEN Auto) ORELSE (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{}  (snd(run-local-pred(r;e2;e1;e1)))  =  e2


By

---

Latex:
((Assert  \mforall{}t:\mBbbN{}.  ((snd(run-local-pred(r;e2;e1;t)))  =  e2)  BY
                (InductionOnNat
                  THEN  RecUnfold  `run-local-pred`  0
                  THEN  Reduce  0
                  THEN  ((Fold  `member`  0  THEN  Auto)
                  ORELSE  (AutoSplit  THEN  (CallByValueReduce  0  THENA  Auto)  THEN  AutoSplit)
                  )))
  THEN  Auto
  )

---

Home Index