---

Step * of Lemma W-uniform-measure-induction

∀[T,A:Type]. ∀[B:A ⟶ Type]. ∀[measure:T ⟶ W(A;a.B[a])]. ∀[P:T ⟶ ℙ].
  ((∀[i:T]. ((∀[j:{j:T| measure[j] <  measure[i]} ]. P[j]) ⇒ P[i])) ⇒ (∀[i:T]. P[i]))
BY
{ TACTIC:(UseWitness ⌜Y⌝⋅
          THEN RepUR ``uall uwellfounded`` 0
          THEN Repeat (ProveMemberIsect)
          THEN Try (Complete (Auto))
          THEN BetterExt⋅
          THEN (((UnivCD THENA Auto) THEN RenameVar `f' (-1) THEN (ProveMemberIsect THENA Auto)) ORELSE Auto)) }

1
1. T : Type
2. A : Type
3. B : A ⟶ Type
4. measure : T ⟶ W(A;a.B[a])
5. P : T ⟶ ℙ
6. f : ⋂i:T. ((⋂j:{j:T| measure[j] <  measure[i]} . P[j]) ⇒ P[i])
7. i : T
⊢ Y f ∈ P[i]

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[measure:T  {}\mrightarrow{}  W(A;a.B[a])].  \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:
TACTIC:(UseWitness  \mkleeneopen{}Y\mkleeneclose{}\mcdot{}
                THEN  RepUR  ``uall  uwellfounded``  0
                THEN  Repeat  (ProveMemberIsect)
                THEN  Try  (Complete  (Auto))
                THEN  BetterExt\mcdot{}
                THEN  (((UnivCD  THENA  Auto)  THEN  RenameVar  `f'  (-1)  THEN  (ProveMemberIsect  THENA  Auto))
                ORELSE  Auto
                ))

---

Home Index