---

Step * of Lemma run-local-pred_wf

∀[M:Type ⟶ Type]. ∀r:pRunType(P.M[P]). ∀i:Id. ∀t',t:ℕ.  (run-local-pred(r;i;t;t') ∈ ℕ × Id)
BY
{ ((InductionOnNat THEN Auto) THEN RecUnfold `run-local-pred` 0 THEN Reduce 0 THEN (AutoSplit ORELSE Auto)) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}r:pRunType(P.M[P]).  \mforall{}i:Id.  \mforall{}t',t:\mBbbN{}.    (run-local-pred(r;i;t;t')  \mmember{}  \mBbbN{}  \mtimes{}  Id)


By

---

Latex:
((InductionOnNat  THEN  Auto)
  THEN  RecUnfold  `run-local-pred`  0
  THEN  Reduce  0
  THEN  (AutoSplit  ORELSE  Auto))

---

Home Index