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