# Library problem

# Puzzle: The Sum Game

A valid change in state is one which is between 1 and 10.

A definition of what it means for the current player
to lose or win from a current state.

Inductive LoseFrom : state → Prop :=

| AllWin : ∀ n,

(∀ n', action n n' → WinFrom n') →

LoseFrom n

with WinFrom : nat → Prop :=

| CanForce : ∀ n n',

action n n' →

LoseFrom n' →

WinFrom n.

| AllWin : ∀ n,

(∀ n', action n n' → WinFrom n') →

LoseFrom n

with WinFrom : nat → Prop :=

| CanForce : ∀ n n',

action n n' →

LoseFrom n' →

WinFrom n.

The total target cumulative sum, which is also the starting
state.

The formal problem statement: Does the first player to play
win or lose?