Step
*
1
1
of Lemma
coPathAgree_transitivity
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. n : ℤ
4. n ≠ 0
5. [%1] : 0 < n
6. ∀[w:coW(A;a.B[a])]
∀p,q,r:coPath(a.B[a];w;n - 1).
(coPathAgree(a.B[a];n - 1;w;p;q)
⇒ coPathAgree(a.B[a];n - 1;w;q;r)
⇒ coPathAgree(a.B[a];n - 1;w;p;r))
7. [w] : coW(A;a.B[a])
8. t : coW-dom(a.B[a];w)
9. p1 : coPath(a.B[a];coW-item(w;t);n - 1)
10. t1 : coW-dom(a.B[a];w)
11. q1 : coPath(a.B[a];coW-item(w;t1);n - 1)
12. t2 : coW-dom(a.B[a];w)
13. r1 : coPath(a.B[a];coW-item(w;t2);n - 1)
14. t = t1 ∈ coW-dom(a.B[a];w)
15. coPathAgree(a.B[a];n - 1;coW-item(w;t);p1;q1)
16. t1 = t2 ∈ coW-dom(a.B[a];w)
17. coPathAgree(a.B[a];n - 1;coW-item(w;t1);q1;r1)
18. t = t2 ∈ coW-dom(a.B[a];w)
⊢ coPathAgree(a.B[a];n - 1;coW-item(w;t);p1;r1)
BY
{ (InstHyp [⌜coW-item(w;t)⌝;⌜p1⌝;⌜q1⌝;⌜r1⌝] 6⋅ THEN Auto) }
1
.....antecedent.....
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. n : ℤ
4. n ≠ 0
5. [%1] : 0 < n
6. ∀[w:coW(A;a.B[a])]
∀p,q,r:coPath(a.B[a];w;n - 1).
(coPathAgree(a.B[a];n - 1;w;p;q)
⇒ coPathAgree(a.B[a];n - 1;w;q;r)
⇒ coPathAgree(a.B[a];n - 1;w;p;r))
7. [w] : coW(A;a.B[a])
8. t : coW-dom(a.B[a];w)
9. p1 : coPath(a.B[a];coW-item(w;t);n - 1)
10. t1 : coW-dom(a.B[a];w)
11. q1 : coPath(a.B[a];coW-item(w;t1);n - 1)
12. t2 : coW-dom(a.B[a];w)
13. r1 : coPath(a.B[a];coW-item(w;t2);n - 1)
14. t = t1 ∈ coW-dom(a.B[a];w)
15. coPathAgree(a.B[a];n - 1;coW-item(w;t);p1;q1)
16. t1 = t2 ∈ coW-dom(a.B[a];w)
17. coPathAgree(a.B[a];n - 1;coW-item(w;t1);q1;r1)
18. t = t2 ∈ coW-dom(a.B[a];w)
⊢ coPathAgree(a.B[a];n - 1;coW-item(w;t);q1;r1)
Latex:
Latex:
1. [A] : \mBbbU{}'
2. [B] : A {}\mrightarrow{} Type
3. n : \mBbbZ{}
4. n \mneq{} 0
5. [\%1] : 0 < n
6. \mforall{}[w:coW(A;a.B[a])]
\mforall{}p,q,r:coPath(a.B[a];w;n - 1).
(coPathAgree(a.B[a];n - 1;w;p;q)
{}\mRightarrow{} coPathAgree(a.B[a];n - 1;w;q;r)
{}\mRightarrow{} coPathAgree(a.B[a];n - 1;w;p;r))
7. [w] : coW(A;a.B[a])
8. t : coW-dom(a.B[a];w)
9. p1 : coPath(a.B[a];coW-item(w;t);n - 1)
10. t1 : coW-dom(a.B[a];w)
11. q1 : coPath(a.B[a];coW-item(w;t1);n - 1)
12. t2 : coW-dom(a.B[a];w)
13. r1 : coPath(a.B[a];coW-item(w;t2);n - 1)
14. t = t1
15. coPathAgree(a.B[a];n - 1;coW-item(w;t);p1;q1)
16. t1 = t2
17. coPathAgree(a.B[a];n - 1;coW-item(w;t1);q1;r1)
18. t = t2
\mvdash{} coPathAgree(a.B[a];n - 1;coW-item(w;t);p1;r1)
By
Latex:
(InstHyp [\mkleeneopen{}coW-item(w;t)\mkleeneclose{};\mkleeneopen{}p1\mkleeneclose{};\mkleeneopen{}q1\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{}] 6\mcdot{} THEN Auto)
Home
Index