Step
*
1
2
1
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. p1 : coPath(a.B[a];w;n1)
9. q1 : coPath(a.B[a];w;n1 + 1)
10. (n1 + 1) ≤ n
11. coPathAgree(a.B[a];n1;w;p1;q1)
⊢ ((fst(copath-last(w;<n1 + 1, q1>))) = copath-at(w;<n1, p1>) ∈ coW(A;a.B[a])) ∧ (copath-at(w;<n1 + 1, q1>) = coW-item(c\000Copath-at(w;<n1, p1>);snd(copath-last(w;<n1 + 1, q1>))) ∈ coW(A;a.B[a]))
BY
{ (Unfold `coPath` -3
THEN (SplitOnHypITE -3 THENA Auto)
THEN Try (Complete (Auto))
THEN D -4
THEN RepUR ``copath-at`` 0
THEN RW (AddrC [2;2] UnfoldTopAbC) 0
THEN (SplitOnConclITE THENA Auto)
THEN Try (Trivial)
THEN Reduce 0
THEN Unfold `copath-last` 0
THEN RepUR ``copath-length`` 0
THEN (SplitOnConclITE THENA Auto)
THEN (Subst' (n1 + 1) - 1 ~ n1 0 THENA Auto)
THEN (Subst' (n1 + 1) - 1 ~ n1 -6 THENA Auto)) }
1
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. p1 : coPath(a.B[a];w;n1)
9. t : coW-dom(a.B[a];w)
10. q2 : coPath(a.B[a];coW-item(w;t);n1)
11. (n1 + 1) ≤ n
12. coPathAgree(a.B[a];n1;w;p1;<t, q2>)
13. ¬((n1 + 1) = 0 ∈ ℤ)
14. ¬((n1 + 1) = 0 ∈ ℤ)
15. (n1 + 1) = 1 ∈ ℤ
⊢ ((fst(<w, copath-hd(<n1 + 1, t, q2>)>)) = coPath-at(n1;w;p1) ∈ coW(A;a.B[a]))
∧ (coPath-at(n1;coW-item(w;t);q2) = coW-item(coPath-at(n1;w;p1);snd(<w, copath-hd(<n1 + 1, t, q2>)>)) ∈ coW(A;a.B[a]))
2
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. p1 : coPath(a.B[a];w;n1)
9. t : coW-dom(a.B[a];w)
10. q2 : coPath(a.B[a];coW-item(w;t);n1)
11. (n1 + 1) ≤ n
12. coPathAgree(a.B[a];n1;w;p1;<t, q2>)
13. ¬((n1 + 1) = 0 ∈ ℤ)
14. ¬((n1 + 1) = 0 ∈ ℤ)
15. ¬((n1 + 1) = 1 ∈ ℤ)
⊢ ((fst(copath-last(coW-item(w;copath-hd(<n1 + 1, t, q2>));copath-tl(<n1 + 1, t, q2>)))) = coPath-at(n1;w;p1) ∈ coW(A;a.\000CB[a]))
∧ (coPath-at(n1;coW-item(w;t);q2) = coW-item(coPath-at(n1;w;p1);snd(copath-last(coW-item(w;copath-hd(<n1 + 1, t, q2>));c\000Copath-tl(<n1 + 1, t, q2>)))) ∈ coW(A;a.B[a]))
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. p1 : coPath(a.B[a];w;n1)
9. q1 : coPath(a.B[a];w;n1 + 1)
10. (n1 + 1) \mleq{} n
11. coPathAgree(a.B[a];n1;w;p1;q1)
\mvdash{} ((fst(copath-last(w;<n1 + 1, q1>))) = copath-at(w;<n1, p1>)) \mwedge{} (copath-at(w;<n1 + 1, q1>) = coW-it\000Cem(copath-at(w;<n1, p1>);snd(copath-last(w;<n1 + 1, q1>))))
By
Latex:
(Unfold `coPath` -3
THEN (SplitOnHypITE -3 THENA Auto)
THEN Try (Complete (Auto))
THEN D -4
THEN RepUR ``copath-at`` 0
THEN RW (AddrC [2;2] UnfoldTopAbC) 0
THEN (SplitOnConclITE THENA Auto)
THEN Try (Trivial)
THEN Reduce 0
THEN Unfold `copath-last` 0
THEN RepUR ``copath-length`` 0
THEN (SplitOnConclITE THENA Auto)
THEN (Subst' (n1 + 1) - 1 \msim{} n1 0 THENA Auto)
THEN (Subst' (n1 + 1) - 1 \msim{} n1 -6 THENA Auto))
Home
Index