---

Step * of Lemma seteqweaken1_ext

∀s1,s2:coSet{i:l}.  ((s1 = s2 ∈ coSet{i:l}) ⇒ seteq(s1;s2))
BY
{ Extract of Obid: seteqweaken1
  not unfolding  play-item play-len copath-length 
  finishing with Auto
  normalizes to:
  
  λ_,_,_,moves. let u,v = moves[||moves|| - 2] 
                in let u',v' = moves[||moves|| - 1] 
                   in if copath-length(u) <z copath-length(u') then <u', u'> else <v', v'> fi  }

---

Latex:

---

Latex:
\mforall{}s1,s2:coSet\{i:l\}.    ((s1  =  s2)  {}\mRightarrow{}  seteq(s1;s2))


By

---

Latex:
Extract  of  Obid:  seteqweaken1
not  unfolding    play-item  play-len  copath-length 
finishing  with  Auto
normalizes  to:

\mlambda{}$_{}$,$_{}$,$_{}$,moves.  let  u,v  =  move\000Cs[||moves||  -  2] 
                      in  let  u',v'  =  moves[||moves||  -  1] 
                            in  if  copath-length(u)  <z  copath-length(u')  then  <u',  u'>  else  <v',  v'>  fi 

---

Home Index