---

Step * 1 of Lemma W-induction


1. [A] : Type
2. [B] : A ⟶ Type
3. [Q] : W(A;a.B[a]) ⟶ ℙ
4. F : ∀a:A. ∀f:B[a] ⟶ W(A;a.B[a]).  ((∀b:B[a]. Q[f b]) ⇒ Q[Wsup(a;f)])@i
5. w : W(A;a.B[a])@i
⊢ Q[w]
BY
{ (InstLemma `W_ind_wf` [⌜A⌝;⌜B⌝;⌜Q⌝;⌜F⌝;⌜w⌝]⋅ THENA Auto) }

1
1. [A] : Type
2. [B] : A ⟶ Type
3. [Q] : W(A;a.B[a]) ⟶ ℙ
4. F : ∀a:A. ∀f:B[a] ⟶ W(A;a.B[a]).  ((∀b:B[a]. Q[f b]) ⇒ Q[Wsup(a;f)])@i
5. w : W(A;a.B[a])@i
6. W_ind(F;w) ∈ Q[w]
⊢ Q[w]

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  [Q]  :  W(A;a.B[a])  {}\mrightarrow{}  \mBbbP{}
4.  F  :  \mforall{}a:A.  \mforall{}f:B[a]  {}\mrightarrow{}  W(A;a.B[a]).    ((\mforall{}b:B[a].  Q[f  b])  {}\mRightarrow{}  Q[Wsup(a;f)])@i
5.  w  :  W(A;a.B[a])@i
\mvdash{}  Q[w]


By

---

Latex:
(InstLemma  `W\_ind\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index