Step
*
1
2
1
2
1
1
2
of Lemma
copathAgree-last
1. n1 : ℕ
2. A : 𝕌'
3. B : A ⟶ Type
4. n : ℤ
5. 0 < n
6. ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
(((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing
((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and
copathAgree(a.B[a];w;p;q) and
(copath-length(q) ≤ (n - 1)))
7. w : coW(A;a.B[a])
8. t1 : coW-dom(a.B[a];w)
9. p2 : coPath(a.B[a];coW-item(w;t1);n1 - 1)
10. t : coW-dom(a.B[a];w)
11. q2 : coPath(a.B[a];coW-item(w;t);n1)
12. (n1 + 1) ≤ n
13. (t1 = t ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];n1 - 1;coW-item(w;t1);p2;q2)
14. ¬(n1 = 0 ∈ ℤ)
15. (fst(copath-last(coW-item(w;t);<n1, q2>))) = copath-at(coW-item(w;t);<n1 - 1, p2>) ∈ coW(A;a.B[a])
16. copath-at(coW-item(w;t);<n1, q2>) = coW-item(copath-at(coW-item(w;t);<n1 - 1, p2>);snd(copath-last(coW-item(w;t);<n1\000C, q2>))) ∈ coW(A;a.B[a])
⊢ coPath-at(n1;coW-item(w;t);q2) = coW-item(coPath-at(n1;w;<t1, p2>);snd(copath-last(coW-item(w;t);<n1, q2>))) ∈ coW(A;a\000C.B[a])
BY
{ (RepUR ``copath-at`` -1 THEN NthHypEqTrans (-1) THEN EqCDA) }
1
.....implicit subterm.....
1. n1 : ℕ
2. A : 𝕌'
3. B : A ⟶ Type
4. n : ℤ
5. 0 < n
6. ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
(((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing
((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and
copathAgree(a.B[a];w;p;q) and
(copath-length(q) ≤ (n - 1)))
7. w : coW(A;a.B[a])
8. t1 : coW-dom(a.B[a];w)
9. p2 : coPath(a.B[a];coW-item(w;t1);n1 - 1)
10. t : coW-dom(a.B[a];w)
11. q2 : coPath(a.B[a];coW-item(w;t);n1)
12. (n1 + 1) ≤ n
13. (t1 = t ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];n1 - 1;coW-item(w;t1);p2;q2)
14. ¬(n1 = 0 ∈ ℤ)
15. (fst(copath-last(coW-item(w;t);<n1, q2>))) = copath-at(coW-item(w;t);<n1 - 1, p2>) ∈ coW(A;a.B[a])
16. coPath-at(n1;coW-item(w;t);q2) = coW-item(coPath-at(n1 - 1;coW-item(w;t);p2);snd(copath-last(coW-item(w;t);<n1, q2>)\000C)) ∈ coW(A;a.B[a])
⊢ λ2a.B[a] = λ2a.B[a] ∈ (A ⟶ Type)
2
.....subterm..... T:t
1:n
1. n1 : ℕ
2. A : 𝕌'
3. B : A ⟶ Type
4. n : ℤ
5. 0 < n
6. ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
(((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing
((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and
copathAgree(a.B[a];w;p;q) and
(copath-length(q) ≤ (n - 1)))
7. w : coW(A;a.B[a])
8. t1 : coW-dom(a.B[a];w)
9. p2 : coPath(a.B[a];coW-item(w;t1);n1 - 1)
10. t : coW-dom(a.B[a];w)
11. q2 : coPath(a.B[a];coW-item(w;t);n1)
12. (n1 + 1) ≤ n
13. (t1 = t ∈ coW-dom(a.B[a];w)) ∧ coPathAgree(a.B[a];n1 - 1;coW-item(w;t1);p2;q2)
14. ¬(n1 = 0 ∈ ℤ)
15. (fst(copath-last(coW-item(w;t);<n1, q2>))) = copath-at(coW-item(w;t);<n1 - 1, p2>) ∈ coW(A;a.B[a])
16. coPath-at(n1;coW-item(w;t);q2) = coW-item(coPath-at(n1 - 1;coW-item(w;t);p2);snd(copath-last(coW-item(w;t);<n1, q2>)\000C)) ∈ coW(A;a.B[a])
⊢ coPath-at(n1 - 1;coW-item(w;t);p2) = coPath-at(n1;w;<t1, p2>) ∈ coW(A;a.B[a])
3
1. n1 : ℕ
2. A : 𝕌'
3. B : A ⟶ Type
4. n : ℤ
5. 0 < n
6. ∀[w:coW(A;a.B[a])]. ∀[p,q:copath(a.B[a];w)].
(((fst(copath-last(w;q))) = copath-at(w;p) ∈ coW(A;a.B[a]))
∧ (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))) ∈ coW(A;a.B[a]))) supposing
((copath-length(q) = (copath-length(p) + 1) ∈ ℤ) and
copathAgree(a.B[a];w;p;q) and
(copath-length(q) ≤ (n - 1)))
7. w : coW(A;a.B[a])
8. t1 : coW-dom(a.B[a];w)
9. p2 : coPath(a.B[a];coW-item(w;t1);n1 - 1)
10. t : coW-dom(a.B[a];w)
11. q2 : coPath(a.B[a];coW-item(w;t);n1)
12. (n1 + 1) ≤ n
13. t1 = t ∈ coW-dom(a.B[a];w)
14. coPathAgree(a.B[a];n1 - 1;coW-item(w;t1);p2;q2)
15. ¬(n1 = 0 ∈ ℤ)
16. (fst(copath-last(coW-item(w;t);<n1, q2>))) = copath-at(coW-item(w;t);<n1 - 1, p2>) ∈ coW(A;a.B[a])
17. coPath-at(n1;coW-item(w;t);q2) = coW-item(coPath-at(n1 - 1;coW-item(w;t);p2);snd(copath-last(coW-item(w;t);<n1, q2>)\000C)) ∈ coW(A;a.B[a])
⊢ 0 < copath-length(<n1, q2>)
Latex:
Latex:
1. n1 : \mBbbN{}
2. A : \mBbbU{}'
3. B : A {}\mrightarrow{} Type
4. n : \mBbbZ{}
5. 0 < n
6. \mforall{}[w:coW(A;a.B[a])]. \mforall{}[p,q:copath(a.B[a];w)].
(((fst(copath-last(w;q))) = copath-at(w;p))
\mwedge{} (copath-at(w;q) = coW-item(copath-at(w;p);snd(copath-last(w;q))))) supposing
((copath-length(q) = (copath-length(p) + 1)) and
copathAgree(a.B[a];w;p;q) and
(copath-length(q) \mleq{} (n - 1)))
7. w : coW(A;a.B[a])
8. t1 : coW-dom(a.B[a];w)
9. p2 : coPath(a.B[a];coW-item(w;t1);n1 - 1)
10. t : coW-dom(a.B[a];w)
11. q2 : coPath(a.B[a];coW-item(w;t);n1)
12. (n1 + 1) \mleq{} n
13. (t1 = t) \mwedge{} coPathAgree(a.B[a];n1 - 1;coW-item(w;t1);p2;q2)
14. \mneg{}(n1 = 0)
15. (fst(copath-last(coW-item(w;t);<n1, q2>))) = copath-at(coW-item(w;t);<n1 - 1, p2>)
16. copath-at(coW-item(w;t);<n1, q2>) = coW-item(copath-at(coW-item(w;t);<n1 - 1, p2>);snd(copath-la\000Cst(coW-item(w;t);<n1, q2>)))
\mvdash{} coPath-at(n1;coW-item(w;t);q2) = coW-item(coPath-at(n1;w;<t1, p2>);snd(copath-last(coW-item(w;t);<\000Cn1, q2>)))
By
Latex:
(RepUR ``copath-at`` -1 THEN NthHypEqTrans (-1) THEN EqCDA)
Home
Index