---

Definition: Spread
Spread(Pos;a.Mv[a]) ==  corec(G.a:Pos × (Mv[a] ⟶ G))

Lemma: Spread_wf
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type].  (Spread(Pos;a.Mv[a]) ∈ Type)

Lemma: spread-ext
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type].  Spread(Pos;a.Mv[a]) ≡ a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a]))

Definition: MoveChoice
MoveChoice(Pos;a.Mv[a]) ==  a:Pos ⟶ (Mv[a]?)

Lemma: MoveChoice_wf
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type].  (MoveChoice(Pos;a.Mv[a]) ∈ Type)

Definition: Play
Play(Pos;a.Mv[a]) ==  ℕ ⟶ MoveChoice(Pos;a.Mv[a])

Lemma: Play_wf
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type].  (Play(Pos;a.Mv[a]) ∈ Type)

Definition: subgame
subgame(g;p;n)
==r if (n =z 0)
    then inl g
    else let a,f = g 
         in case p 0 a of inl(m) => subgame(f m;λi.(p (i + 1));n - 1) | inr(z) => inr z 
    fi 

Lemma: subgame_wf
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type]. ∀[n:ℕ]. ∀[g:Spread(Pos;a.Mv[a])]. ∀[p:ℕn ⟶ MoveChoice(Pos;a.Mv[a])].
  (subgame(g;p;n) ∈ Spread(Pos;a.Mv[a])?)

Definition: sub-spread
s' ≤ s ==  ∃n:ℕ. ∃p:ℕn ⟶ MoveChoice(Pos;a.Mv[a]). (subgame(s;p;n) = (inl s') ∈ (Spread(Pos;a.Mv[a])?))

Lemma: sub-spread_wf
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type]. ∀[s',s:Spread(Pos;a.Mv[a])].  (s' ≤ s ∈ ℙ)

Lemma: sub-spread-transitive
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type].  Trans(Spread(Pos;a.Mv[a]);s',s.s' ≤ s)

Definition: resigned
resigned(x) ==  ↑isr(x)

Lemma: resigned_wf
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type]. ∀[sg:Spread(Pos;a.Mv[a])?].  (resigned(sg) ∈ ℙ)

Definition: shift-play
shift-play(p) ==  λi.(p (i + 1))

Lemma: shift-play_wf
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type]. ∀[n:ℕ]. ∀[p:ℕn ⟶ MoveChoice(Pos;a.Mv[a])].
  (shift-play(p) ∈ ℕn - 1 ⟶ MoveChoice(Pos;a.Mv[a]))

Definition: WfdSpread
WfdSpread(Pos;a.Mv[a]) ==  {g:Spread(Pos;a.Mv[a])| ∀p:ℕ ⟶ MoveChoice(Pos;a.Mv[a]). (↓∃n:ℕ. resigned(subgame(g;p;n)))} 

Lemma: WfdSpread_wf
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type].  (WfdSpread(Pos;a.Mv[a]) ∈ Type)

Lemma: WfdSpread-ext
∀[Pos:Type]
  ∀[Mv:Pos ⟶ Type]. WfdSpread(Pos;a.Mv[a]) ≡ a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])) 
  supposing ∀a,b:Pos.  Dec(a = b ∈ Pos)

Definition: mkW
mkW(a;f) ==  <a, f>

Lemma: mkW_wf
∀[Pos:Type]. ∀[Mv:Pos ⟶ Type]. ∀[a:Pos]. ∀[f:Mv[a] ⟶ WfdSpread(Pos;a.Mv[a])].  (mkW(a;f) ∈ WfdSpread(Pos;a.Mv[a]))

Definition: W_sel
W_sel(w;n;s) ==  subgame(w;s;n)

Lemma: W_sel_wf
∀[Pos:Type]
  ∀[Mv:Pos ⟶ Type]. ∀[n:ℕ]. ∀[w:WfdSpread(Pos;a.Mv[a])]. ∀[s:ℕn ⟶ MoveChoice(Pos;a.Mv[a])].
    (W_sel(w;n;s) ∈ WfdSpread(Pos;a.Mv[a])?) 
  supposing ∀x,y:Pos.  Dec(x = y ∈ Pos)

Lemma: WfdSpread-induction
∀[Pos:Type]
  ((∀a,b:Pos.  Dec(a = b ∈ Pos))
  ⇒ (∀[Mv:Pos ⟶ Type]. ∀[P:WfdSpread(Pos;a.Mv[a]) ⟶ ℙ].
        ((∀a:Pos. ∀f:Mv[a] ⟶ WfdSpread(Pos;a.Mv[a]).  ((∀m:Mv[a]. P[f m]) ⇒ P[mkW(a;f)]))
        ⇒ (∀w:WfdSpread(Pos;a.Mv[a]). P[w]))))

Definition: Spread-family
Spread-family(P;Pos;f;n,p,q.Mv[n;
                               p;
                               q]) ==
  corec-family(λS,p. (a:Pos × (q:P
                              ⟶ Mv[f a;
                                    p;
                                    q]
                              ⟶ (S q))))

Lemma: Spread-family_wf
∀[P,Pos:Type]. ∀[f:Pos ⟶ ℤ]. ∀[Mv:p:ℤ ⟶ P ⟶ P ⟶ Type].  (Spread-family(P;Pos;f;n,p,q.Mv[n;p;q]) ∈ P ⟶ Type)

Lemma: Spread-family-ext
∀[P,Pos:Type]. ∀[f:Pos ⟶ ℤ]. ∀[Mv:ℤ ⟶ P ⟶ P ⟶ Type].
  Spread-family(P;Pos;f;n,p,q.Mv[n;p;q])
  ≡ λp.(a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (Spread-family(P;Pos;f;n,p,q.Mv[n;p;q]) q)))



Home Index