---

Step * of Lemma coW-pos-agree_transitivity

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])].
  ∀p,q,r:Pos(coW-game(a.B[a];w;w')).
    (coW-pos-agree(a.B[a];w;w';p;q) ⇒ coW-pos-agree(a.B[a];w;w';q;r) ⇒ coW-pos-agree(a.B[a];w;w';p;r))
BY
{ (Auto
   THEN All (RepUR ``sg-pos coW-game coW-pos-agree``)
   THEN DVar `p'
   THEN DVar `q'
   THEN DVar `r'
   THEN All Reduce
   THEN Auto) }

1
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)
⊢ copathAgree(a.B[a];w;p1;r1)

2
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)

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w,w':coW(A;a.B[a])].
    \mforall{}p,q,r:Pos(coW-game(a.B[a];w;w')).
        (coW-pos-agree(a.B[a];w;w';p;q)
        {}\mRightarrow{}  coW-pos-agree(a.B[a];w;w';q;r)
        {}\mRightarrow{}  coW-pos-agree(a.B[a];w;w';p;r))


By

---

Latex:
(Auto
  THEN  All  (RepUR  ``sg-pos  coW-game  coW-pos-agree``)
  THEN  DVar  `p'
  THEN  DVar  `q'
  THEN  DVar  `r'
  THEN  All  Reduce
  THEN  Auto)

---

Home Index