---

Step * 2 of Lemma coW-pos-agree_transitivity


1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. [w] : coW(A;a.B[a])
4. [w'] : coW(A;a.B[a])
5. p1 : copath(a.B[a];w)
6. p2 : copath(a.B[a];w')
7. q1 : copath(a.B[a];w)
8. q2 : copath(a.B[a];w')
9. r1 : copath(a.B[a];w)
10. r2 : copath(a.B[a];w')
11. copath-length(p1) ≤ copath-length(q1)
12. copathAgree(a.B[a];w;p1;q1)
13. copath-length(p2) ≤ copath-length(q2)
14. copathAgree(a.B[a];w';p2;q2)
15. copath-length(q1) ≤ copath-length(r1)
16. copathAgree(a.B[a];w;q1;r1)
17. copath-length(q2) ≤ copath-length(r2)
18. copathAgree(a.B[a];w';q2;r2)
19. copath-length(p1) ≤ copath-length(r1)
20. copathAgree(a.B[a];w;p1;r1)
21. copath-length(p2) ≤ copath-length(r2)
⊢ copathAgree(a.B[a];w';p2;r2)
BY
{ (FLemma `copathAgree_transitivity` [14;18] THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  \mBbbU{}'
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  [w]  :  coW(A;a.B[a])
4.  [w']  :  coW(A;a.B[a])
5.  p1  :  copath(a.B[a];w)
6.  p2  :  copath(a.B[a];w')
7.  q1  :  copath(a.B[a];w)
8.  q2  :  copath(a.B[a];w')
9.  r1  :  copath(a.B[a];w)
10.  r2  :  copath(a.B[a];w')
11.  copath-length(p1)  \mleq{}  copath-length(q1)
12.  copathAgree(a.B[a];w;p1;q1)
13.  copath-length(p2)  \mleq{}  copath-length(q2)
14.  copathAgree(a.B[a];w';p2;q2)
15.  copath-length(q1)  \mleq{}  copath-length(r1)
16.  copathAgree(a.B[a];w;q1;r1)
17.  copath-length(q2)  \mleq{}  copath-length(r2)
18.  copathAgree(a.B[a];w';q2;r2)
19.  copath-length(p1)  \mleq{}  copath-length(r1)
20.  copathAgree(a.B[a];w;p1;r1)
21.  copath-length(p2)  \mleq{}  copath-length(r2)
\mvdash{}  copathAgree(a.B[a];w';p2;r2)


By

---

Latex:
(FLemma  `copathAgree\_transitivity`  [14;18]  THEN  Auto)

---

Home Index