---

Definition: GameA
GameA{i:l}() ==  Type × Type

Lemma: GameA_wf
GameA{i:l}() ∈ 𝕌'

Definition: GameB
GameB(p) ==  let L,R = p in L + R

Lemma: GameB_wf
∀[p:GameA{i:l}()]. (GameB(p) ∈ Type)

Definition: Game
Game ==  W(GameA{i:l}();p.GameB(p))

Lemma: Game_wf
Game ∈ 𝕌'

Lemma: Game_ext
Game ≡ LR:GameA{i:l}() × (GameB(LR) ⟶ Game)

Lemma: Game_subtype
Game ⊆r (LR:GameA{i:l}() × (GameB(LR) ⟶ Game))

Definition: left-indices
left-indices(g) ==  fst(fst(g))

Lemma: left-indices_wf
∀[g:Game]. (left-indices(g) ∈ Type)

Definition: right-indices
right-indices(g) ==  snd(fst(g))

Lemma: right-indices_wf
∀[g:Game]. (right-indices(g) ∈ Type)

Definition: left-move
left-move(g;x) ==  (snd(g)) (inl x)

Lemma: left-move_wf
∀[g:Game]. ∀[x:left-indices(g)].  (left-move(g;x) ∈ Game)

Definition: right-move
right-move(g;x) ==  (snd(g)) (inr x )

Lemma: right-move_wf
∀[g:Game]. ∀[x:right-indices(g)].  (right-move(g;x) ∈ Game)

Definition: left-option
left-option{i:l}(g;m) ==  ∃x:left-indices(g). (m = left-move(g;x) ∈ Game)

Lemma: left-option_wf
∀[m,g:Game].  (left-option{i:l}(g;m) ∈ ℙ')

Definition: right-option
right-option{i:l}(g;m) ==  ∃x:right-indices(g). (m = right-move(g;x) ∈ Game)

Lemma: right-option_wf
∀[m,g:Game].  (right-option{i:l}(g;m) ∈ ℙ')

Lemma: Game-induction
∀[P:Game ⟶ ℙ']
  ((∀g:Game. ((∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ P[m])) ⇒ P[g])) ⇒ {∀g:Game. P[g]})

Definition: mkGame
{mkGame(f[a] with a:L | g[b] with b:R} ==  Wsup(<L, R>;λx.case x of inl(a) => f[a] | inr(b) => g[b])

Lemma: mkGame_wf
∀[L,R:Type]. ∀[f:L ⟶ Game]. ∀[g:R ⟶ Game].  ({mkGame(f[a] with a:L | g[b] with b:R} ∈ Game)

Definition: mk-Game
{L | R} ==  {mkGame(L[i] with i:ℕ||L|| | R[j] with j:ℕ||R||}

Lemma: mk-Game_wf
∀[L,R:Game List].  ({L | R} ∈ Game)

Definition: Game0
0 ==  {[] | []}

Lemma: Game0_wf
0 ∈ Game

Definition: Game-minus
-(G) ==  {mkGame(-(right-move(G;i)) with i:right-indices(G) | -(left-move(G;i)) with i:left-indices(G)}

Lemma: Game-minus_wf
∀[G:Game]. (-(G) ∈ Game)

Lemma: left_move_minus_lemma
∀x,G:Top.  (left-move(-(G);x) ~ -(right-move(G;x)))

Lemma: right_move_minus_lemma
∀x,G:Top.  (right-move(-(G);x) ~ -(left-move(G;x)))

Lemma: left_indices_minus_lemma
∀G:Top. (left-indices(-(G)) ~ right-indices(G))

Lemma: right_indices_minus_lemma
∀G:Top. (right-indices(-(G)) ~ left-indices(G))

Definition: Game-add
G ⊕ H ==
  {mkGame(case x
   of inl(a) =>
   left-move(G;a) ⊕ H
   | inr(b) =>
   G ⊕ left-move(H;b) with x:left-indices(G) + left-indices(H) | case y
   of inl(a) =>
   right-move(G;a) ⊕ H
   | inr(b) =>
   G ⊕ right-move(H;b) with y:right-indices(G) + right-indices(H)}

Lemma: Game-add_wf
∀[G,H:Game].  (G ⊕ H ∈ Game)

Lemma: left_indices_add_lemma
∀H,G:Top.  (left-indices(G ⊕ H) ~ left-indices(G) + left-indices(H))

Lemma: right_indices_add_lemma
∀H,G:Top.  (right-indices(G ⊕ H) ~ right-indices(G) + right-indices(H))

Lemma: left_move_add_inl_lemma
∀x,H,G:Top.  (left-move(G ⊕ H;inl x) ~ left-move(G;x) ⊕ H)

Lemma: left_move_add_inr_lemma
∀x,H,G:Top.  (left-move(G ⊕ H;inr x ) ~ G ⊕ left-move(H;x))

Lemma: right_move_add_inl_lemma
∀x,H,G:Top.  (right-move(G ⊕ H;inl x) ~ right-move(G;x) ⊕ H)

Lemma: right_move_add_inr_lemma
∀x,H,G:Top.  (right-move(G ⊕ H;inr x ) ~ G ⊕ right-move(H;x))

Definition: eq-Game
G ≡ H ==
  ((∀i:left-indices(G). ∃j:left-indices(H). left-move(G;i) ≡ left-move(H;j))
  ∧ (∀i:right-indices(G). ∃j:right-indices(H). right-move(G;i) ≡ right-move(H;j)))
  ∧ (∀i:left-indices(H). ∃j:left-indices(G). left-move(H;i) ≡ left-move(G;j))
  ∧ (∀i:right-indices(H). ∃j:right-indices(G). right-move(H;i) ≡ right-move(G;j))

Lemma: eq-Game_wf
∀[G,H:Game].  (G ≡ H ∈ ℙ)

Lemma: eq-Game_weakening
∀G,H:Game.  ((G = H ∈ Game) ⇒ G ≡ H)

Lemma: eq-Game_inversion
∀G,H:Game.  (G ≡ H ⇒ H ≡ G)

Lemma: eq-Game_transitivity
∀G,H,K:Game.  (G ≡ H ⇒ H ≡ K ⇒ G ≡ K)

Lemma: Game-add-Game0
∀G:Game. 0 ⊕ G ≡ G

Lemma: Game-add-comm
∀G,H:Game.  G ⊕ H ≡ H ⊕ G

Lemma: Game-add-assoc
∀G,H,K:Game.  G ⊕ H ⊕ K ≡ G ⊕ H ⊕ K

Lemma: Game-add_functionality
∀G1,H1,G2,H2:Game.  (G1 ≡ G2 ⇒ H1 ≡ H2 ⇒ G1 ⊕ H1 ≡ G2 ⊕ H2)

Lemma: Game-minus_functionality
∀G1,G2:Game.  (G1 ≡ G2 ⇒ -(G1) ≡ -(G2))

Lemma: Game-minus-minus
∀G:Game. -(-(G)) ≡ G



Home Index