Step
*
1
2
of Lemma
W-type-ext
1. A : Type
2. ∀x,y:A. Dec(x = y ∈ A)
3. B : A ⟶ Type
4. a : A
5. x1 : B[a] ⟶ co-W(A;a.B[a])
6. ∀p:ℕ ⟶ a:A ⟶ (B[a]?). W-bars(<a, x1>;p)
7. b : B[a]
8. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
9. eq : EqDecider(A)
10. n : ℕ
11. ↑isr(W-select(<a, x1>;map(λn.if (n =z 0) then λz.if eq z a then inl b else inr ⋅ fi else p (n - 1) fi ;upto(n))))
12. ¬(n = 0 ∈ ℤ)
⊢ ∃n:ℕ. (↑isr(W-select(x1 b;map(p;upto(n)))))
BY
{ (With ⌜n - 1⌝ (D 0)⋅ THEN Auto)⋅ }
1
1. A : Type
2. ∀x,y:A. Dec(x = y ∈ A)
3. B : A ⟶ Type
4. a : A
5. x1 : B[a] ⟶ co-W(A;a.B[a])
6. ∀p:ℕ ⟶ a:A ⟶ (B[a]?). W-bars(<a, x1>;p)
7. b : B[a]
8. p : ℕ ⟶ a:A ⟶ (B[a]?)@i
9. eq : EqDecider(A)
10. n : ℕ
11. ↑isr(W-select(<a, x1>;map(λn.if (n =z 0) then λz.if eq z a then inl b else inr ⋅ fi else p (n - 1) fi ;upto(n))))
12. ¬(n = 0 ∈ ℤ)
⊢ ↑isr(W-select(x1 b;map(p;upto(n - 1))))
Latex:
Latex:
1. A : Type
2. \mforall{}x,y:A. Dec(x = y)
3. B : A {}\mrightarrow{} Type
4. a : A
5. x1 : B[a] {}\mrightarrow{} co-W(A;a.B[a])
6. \mforall{}p:\mBbbN{} {}\mrightarrow{} a:A {}\mrightarrow{} (B[a]?). W-bars(<a, x1>p)
7. b : B[a]
8. p : \mBbbN{} {}\mrightarrow{} a:A {}\mrightarrow{} (B[a]?)@i
9. eq : EqDecider(A)
10. n : \mBbbN{}
11. \muparrow{}isr(W-select(<a, x1>map(\mlambda{}n.if (n =\msubz{} 0) then \mlambda{}z.if eq z a then inl b else inr \mcdot{} fi else p (n \000C- 1) fi ;
upto(n))))
12. \mneg{}(n = 0)
\mvdash{} \mexists{}n:\mBbbN{}. (\muparrow{}isr(W-select(x1 b;map(p;upto(n)))))
By
Latex:
(With \mkleeneopen{}n - 1\mkleeneclose{} (D 0)\mcdot{} THEN Auto)\mcdot{}
Home
Index