---

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

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w,w':coW(A;a.B[a])].  ∀p,q:Pos(coW-game(a.B[a];w;w')).  SqStable(Legal1(p;q))
BY
{ ((Auto THEN (D 0 THENA Auto)) THEN All (RepUR ``sg-pos sg-legal1 coW-game``) THEN DProds THEN All Reduce) }

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))
⊢ ((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:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w,w':coW(A;a.B[a])].
    \mforall{}p,q:Pos(coW-game(a.B[a];w;w')).    SqStable(Legal1(p;q))


By

---

Latex:
((Auto  THEN  (D  0  THENA  Auto))
  THEN  All  (RepUR  ``sg-pos  sg-legal1  coW-game``)
  THEN  DProds
  THEN  All  Reduce)

---

Home Index