---

Step * 1 1 of Lemma W-uwellfounded_witness


1. A : Type
2. B : A ⟶ Type
3. P : W(A;a.B[a]) ⟶ ℙ
4. f : ⋂j:W(A;a.B[a]). ((⋂k:{k:W(A;a.B[a])| k <  j} . P[k]) ⇒ P[j])
5. a : A
6. f1 : B[a] ⟶ W(A;a.B[a])
7. ∀w:W(A;a.B[a]). ((w <  Wsup(a;f1)) ⇒ (fix(f) ∈ P[w]))
⊢ ∀w:W(A;a.B[a]). ∀v:w ≤  Wsup(a;f1).  (fix(f) ∈ P[w])
BY
{ ((UnivCD THENA Auto) THEN RW (SweepUpC UnrollRecursionC) 0) }

1
1. A : Type
2. B : A ⟶ Type
3. P : W(A;a.B[a]) ⟶ ℙ
4. f : ⋂j:W(A;a.B[a]). ((⋂k:{k:W(A;a.B[a])| k <  j} . P[k]) ⇒ P[j])
5. a : A
6. f1 : B[a] ⟶ W(A;a.B[a])
7. ∀w:W(A;a.B[a]). ((w <  Wsup(a;f1)) ⇒ (fix(f) ∈ P[w]))
8. w : W(A;a.B[a])
9. v : w ≤  Wsup(a;f1)
⊢ f fix(f) ∈ P[w]

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  P  :  W(A;a.B[a])  {}\mrightarrow{}  \mBbbP{}
4.  f  :  \mcap{}j:W(A;a.B[a]).  ((\mcap{}k:\{k:W(A;a.B[a])|  k  <    j\}  .  P[k])  {}\mRightarrow{}  P[j])
5.  a  :  A
6.  f1  :  B[a]  {}\mrightarrow{}  W(A;a.B[a])
7.  \mforall{}w:W(A;a.B[a]).  ((w  <    Wsup(a;f1))  {}\mRightarrow{}  (fix(f)  \mmember{}  P[w]))
\mvdash{}  \mforall{}w:W(A;a.B[a]).  \mforall{}v:w  \mleq{}    Wsup(a;f1).    (fix(f)  \mmember{}  P[w])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RW  (SweepUpC  UnrollRecursionC)  0)

---

Home Index