---

Step * 1 2 of Lemma sq-stable-coW-game-legal2


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)@i
6. p2 : copath(a.B[a];w')@i
7. q1 : copath(a.B[a];w)@i
8. q2 : copath(a.B[a];w')@i
9. ↓(((copath-length(q1) = (copath-length(p1) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w;p1;q1) ∧ (p2 = q2 ∈ copath(a.B[a];w')))
    ∨ ((p1 = q1 ∈ copath(a.B[a];w)) ∧ (copath-length(q2) = (copath-length(p2) + 1) ∈ ℤ) ∧ copathAgree(a.B[a];w';p2;q2)))
    ∧ (copath-length(q1) = copath-length(q2) ∈ ℤ)
⊢ copath-length(q1) = copath-length(q2) ∈ ℤ
BY
{ (D -1 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)@i
6.  p2  :  copath(a.B[a];w')@i
7.  q1  :  copath(a.B[a];w)@i
8.  q2  :  copath(a.B[a];w')@i
9.  \mdownarrow{}(((copath-length(q1)  =  (copath-length(p1)  +  1))  \mwedge{}  copathAgree(a.B[a];w;p1;q1)  \mwedge{}  (p2  =  q2))
        \mvee{}  ((p1  =  q1)  \mwedge{}  (copath-length(q2)  =  (copath-length(p2)  +  1))  \mwedge{}  copathAgree(a.B[a];w';p2;q2)))
        \mwedge{}  (copath-length(q1)  =  copath-length(q2))
\mvdash{}  copath-length(q1)  =  copath-length(q2)


By

---

Latex:
(D  -1  THEN  Auto)

---

Home Index