---

Step * of Lemma uniform_nat_measure_ind

∀[T:Type]. ∀[measure:T ⟶ ℕ]. ∀[P:T ⟶ ℙ].
  ((∀[i:T]. ((∀[j:{j:T| measure[j] < measure[i]} ]. P[j]) ⇒ P[i])) ⇒ (∀[i:T]. P[i]))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN UseWitness ⌜λF.fix(F)⌝
   THEN (MemCD THENA Auto)
   THEN Assert ⌜∀m:ℕ. ∀i:T.  ((measure[i] ≤ m) ⇒ (fix(F) ∈ P[i]))⌝⋅
   THEN Try ((Unfold `uall` 0 THEN MemTypeCD THEN Auto THEN InstHyp [⌜measure[i]⌝;⌜i⌝] (-2)⋅ THEN Auto))) }

1
.....assertion..... 
1. T : Type
2. measure : T ⟶ ℕ
3. P : T ⟶ ℙ
4. F : ∀[i:T]. ((∀[j:{j:T| measure[j] < measure[i]} ]. P[j]) ⇒ P[i])
⊢ ∀m:ℕ. ∀i:T.  ((measure[i] ≤ m) ⇒ (fix(F) ∈ P[i]))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[measure:T  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}[i:T].  ((\mforall{}[j:\{j:T|  measure[j]  <  measure[i]\}  ].  P[j])  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  (\mforall{}[i:T].  P[i]))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  UseWitness  \mkleeneopen{}\mlambda{}F.fix(F)\mkleeneclose{}
  THEN  (MemCD  THENA  Auto)
  THEN  Assert  \mkleeneopen{}\mforall{}m:\mBbbN{}.  \mforall{}i:T.    ((measure[i]  \mleq{}  m)  {}\mRightarrow{}  (fix(F)  \mmember{}  P[i]))\mkleeneclose{}\mcdot{}
  THEN  Try  ((Unfold  `uall`  0
                        THEN  MemTypeCD
                        THEN  Auto
                        THEN  InstHyp  [\mkleeneopen{}measure[i]\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  (-2)\mcdot{}
                        THEN  Auto)))

---

Home Index