Step
*
1
1
1
1
2
1
of Lemma
param-W-ext
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pco-W ∈ P ⟶ Type
6. p : P
7. a : A[p]
8. x1 : b:B[p;a] ⟶ (pco-W C[p;a;b])
9. ∀path:Path. (StepAgree(path 0;p;<a, x1>) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
10. <a, x1> ∈ pco-W p
11. b : B[p;a]
12. path : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
13. ∀i:ℕ. StepRel(path i;path (i + 1))
14. p1 : P
15. w : pco-W p1
16. v2 : B[p1;fst(w)]?
17. (path 0) = <p1, w, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
18. p1 = C[p;a;b] ∈ P
19. w = (x1 b) ∈ (pco-W C[p;a;b])
20. n : ℕ
21. 0 < n ∧ let p,w,d = if (n - 1 =z 0) then <p, <a, x1>, inl b> else path (n - 1 - 1) fi in ↑isr(d)
⊢ ∃n:ℕ. Barred(pcw-partial(path;n))
BY
{ (With ⌜n - 1⌝ (D 0))⋅ }
1
.....wf.....
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pco-W ∈ P ⟶ Type
6. p : P
7. a : A[p]
8. x1 : b:B[p;a] ⟶ (pco-W C[p;a;b])
9. ∀path:Path. (StepAgree(path 0;p;<a, x1>) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
10. <a, x1> ∈ pco-W p
11. b : B[p;a]
12. path : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
13. ∀i:ℕ. StepRel(path i;path (i + 1))
14. p1 : P
15. w : pco-W p1
16. v2 : B[p1;fst(w)]?
17. (path 0) = <p1, w, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
18. p1 = C[p;a;b] ∈ P
19. w = (x1 b) ∈ (pco-W C[p;a;b])
20. n : ℕ
21. 0 < n ∧ let p,w,d = if (n - 1 =z 0) then <p, <a, x1>, inl b> else path (n - 1 - 1) fi in ↑isr(d)
⊢ n - 1 ∈ ℕ
2
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pco-W ∈ P ⟶ Type
6. p : P
7. a : A[p]
8. x1 : b:B[p;a] ⟶ (pco-W C[p;a;b])
9. ∀path:Path. (StepAgree(path 0;p;<a, x1>) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
10. <a, x1> ∈ pco-W p
11. b : B[p;a]
12. path : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
13. ∀i:ℕ. StepRel(path i;path (i + 1))
14. p1 : P
15. w : pco-W p1
16. v2 : B[p1;fst(w)]?
17. (path 0) = <p1, w, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
18. p1 = C[p;a;b] ∈ P
19. w = (x1 b) ∈ (pco-W C[p;a;b])
20. n : ℕ
21. 0 < n ∧ let p,w,d = if (n - 1 =z 0) then <p, <a, x1>, inl b> else path (n - 1 - 1) fi in ↑isr(d)
⊢ Barred(pcw-partial(path;n - 1))
3
.....wf.....
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pco-W ∈ P ⟶ Type
6. p : P
7. a : A[p]
8. x1 : b:B[p;a] ⟶ (pco-W C[p;a;b])
9. ∀path:Path. (StepAgree(path 0;p;<a, x1>) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
10. <a, x1> ∈ pco-W p
11. b : B[p;a]
12. path : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
13. ∀i:ℕ. StepRel(path i;path (i + 1))
14. p1 : P
15. w : pco-W p1
16. v2 : B[p1;fst(w)]?
17. (path 0) = <p1, w, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
18. p1 = C[p;a;b] ∈ P
19. w = (x1 b) ∈ (pco-W C[p;a;b])
20. n : ℕ
21. 0 < n ∧ let p,w,d = if (n - 1 =z 0) then <p, <a, x1>, inl b> else path (n - 1 - 1) fi in ↑isr(d)
22. n1 : ℕ
⊢ istype(Barred(pcw-partial(path;n1)))
Latex:
Latex:
1. P : Type
2. A : P {}\mrightarrow{} Type
3. B : p:P {}\mrightarrow{} A[p] {}\mrightarrow{} Type
4. C : p:P {}\mrightarrow{} a:A[p] {}\mrightarrow{} B[p;a] {}\mrightarrow{} P
5. pco-W \mmember{} P {}\mrightarrow{} Type
6. p : P
7. a : A[p]
8. x1 : b:B[p;a] {}\mrightarrow{} (pco-W C[p;a;b])
9. \mforall{}path:Path. (StepAgree(path 0;p;<a, x1>) {}\mRightarrow{} (\mdownarrow{}\mexists{}n:\mBbbN{}. Barred(pcw-partial(path;n))))
10. <a, x1> \mmember{} pco-W p
11. b : B[p;a]
12. path : \mBbbN{} {}\mrightarrow{} pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
13. \mforall{}i:\mBbbN{}. StepRel(path i;path (i + 1))
14. p1 : P
15. w : pco-W p1
16. v2 : B[p1;fst(w)]?
17. (path 0) = <p1, w, v2>
18. p1 = C[p;a;b]
19. w = (x1 b)
20. n : \mBbbN{}
21. 0 < n \mwedge{} let p,w,d = if (n - 1 =\msubz{} 0) then <p, <a, x1>, inl b> else path (n - 1 - 1) fi in \muparrow{}isr(d\000C)
\mvdash{} \mexists{}n:\mBbbN{}. Barred(pcw-partial(path;n))
By
Latex:
(With \mkleeneopen{}n - 1\mkleeneclose{} (D 0))\mcdot{}
Home
Index