---

Step * of Lemma coW-game-step-isom

∀[A:𝕌']
  ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]). ∀t:coW-dom(a.B[a];w). ∀b:coW-dom(a.B[a];w').
    sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))) ≅ coW-game(a.B[a];w;w')@<copath-cons(t;())
                                                                                        , copath-cons(b;())
                                                                                        >
BY
{ (Auto
   THEN (Assert λp.let u,v = p 
                   in <copath-cons(t;u), copath-cons(b;v)>
                ∈ Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
                ⟶ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>) BY
               (Auto THEN (RepUR ``sg-pos sg-change-init`` 0 THEN MemTypeCD) THEN Auto))
   ) }

1
.....set predicate..... 
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. t : coW-dom(a.B[a];w)
6. b : coW-dom(a.B[a];w')
7. p1 : copath(a.B[a];coW-item(w;t))
8. p2 : copath(a.B[a];coW-item(w';b))
9. sg-reachable(coW-game(a.B[a];coW-item(w;t);coW-item(w';b));InitialPos(coW-game(a.B[a];coW-item(w;t);...));<p1, p2>)
⊢ sg-reachable(coW-game(a.B[a];w;w');<copath-cons(t;()), copath-cons(b;())>;<copath-cons(t;p1), copath-cons(b;p2)>)

2
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. t : coW-dom(a.B[a];w)
6. b : coW-dom(a.B[a];w')
7. λp.let u,v = p 
      in <copath-cons(t;u), copath-cons(b;v)> ∈ Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
   ⟶ Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()), copath-cons(b;())>)
⊢ sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))) ≅ coW-game(a.B[a];w;w')@<copath-cons(t;())
                                                                                      , copath-cons(b;())
                                                                                      >

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}']
    \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}w,w':coW(A;a.B[a]).  \mforall{}t:coW-dom(a.B[a];w).  \mforall{}b:coW-dom(a.B[a];w').
        sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))  \mcong{}
        coW-game(a.B[a];w;w')@<copath-cons(t;()),  copath-cons(b;())>


By

---

Latex:
(Auto
  THEN  (Assert  \mlambda{}p.let  u,v  =  p 
                                  in  <copath-cons(t;u),  copath-cons(b;v)>
                            \mmember{}  Pos(sg-normalize(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
                            {}\mrightarrow{}  Pos(coW-game(a.B[a];w;w')@<copath-cons(t;()),  copath-cons(b;())>)  BY
                          (Auto  THEN  (RepUR  ``sg-pos  sg-change-init``  0  THEN  MemTypeCD)  THEN  Auto))
  )

---

Home Index