---

Step * 1 of Lemma sq-stable-coW-game-legal1


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(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))
BY
{ (Decide ⌜copath-length(q1) = (copath-length(p1) + 1) ∈ ℤ⌝⋅ THENA 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)@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))
10. copath-length(q1) = (copath-length(p1) + 1) ∈ ℤ
⊢ ((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))

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)@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))
10. ¬(copath-length(q1) = (copath-length(p1) + 1) ∈ ℤ)
⊢ ((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))

---

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))
\mvdash{}  ((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))


By

---

Latex:
(Decide  \mkleeneopen{}copath-length(q1)  =  (copath-length(p1)  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index