---

Step * 1 of Lemma uniform_nat_measure_ind

.....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]))
BY
{ (All (Unfolds ``uall implies``)
   THEN (D 0 THENA Auto)
   THEN NatInd (-1)⋅
   THEN (Auto THEN RW (AddrC [2] UnrollRecursionC) 0 THEN Reduce 0 THEN Auto THEN D -1 THEN Auto')⋅) }

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  measure  :  T  {}\mrightarrow{}  \mBbbN{}
3.  P  :  T  {}\mrightarrow{}  \mBbbP{}
4.  F  :  \mforall{}[i:T].  ((\mforall{}[j:\{j:T|  measure[j]  <  measure[i]\}  ].  P[j])  {}\mRightarrow{}  P[i])
\mvdash{}  \mforall{}m:\mBbbN{}.  \mforall{}i:T.    ((measure[i]  \mleq{}  m)  {}\mRightarrow{}  (fix(F)  \mmember{}  P[i]))


By

---

Latex:
(All  (Unfolds  ``uall  implies``)
  THEN  (D  0  THENA  Auto)
  THEN  NatInd  (-1)\mcdot{}
  THEN  (Auto  THEN  RW  (AddrC  [2]  UnrollRecursionC)  0  THEN  Reduce  0  THEN  Auto  THEN  D  -1  THEN  Auto')\mcdot{})

---

Home Index