- GAME::= Net{
- N person game.
- Players::Sets=given. Some Players.
- No_of_players::=|Players|.
- N::=No_of_players.
- Position::Sets.
- moves::Position->@Position.
- moves::@Position->@Position=map[P:@Positions]{q:Position|| for some p:P, q in moves(p)}.
- State::Sets. win, loose,draw,undecided::State.
- value::Position->State.
- Won::=win./value.
- Lost::=loose./value.
- Drawn::=draw./value.
- For all p:Position ( p in Won|Lost|Draw iff moves(p)={}).
Winning, Loosing::@Position.

- Won==>Winning. Lost==>Loosing.
- No Winning & Loosing.
- Initial::@Position.
- loops::@= some p:positions( p in moves;do(moves) ).

}=::GAME. - SOLITAIRE::={ A game with one player were there may be a chance of winning and one initial state
- GAME and No_of_players=1.
- For all p:Loosing, p.moves==>Loosing.
- Draw={}.
- possible::@= Initial==>Winning and for all p:Winning, some p.moves & Winning.
- Rubik's cube is a patience game with loops. Solitare card games have no loops.
- Rubik's cube has no Loosing positions, a single Won position, and a finite but large set of Winning positions.
- Call such a game a maze:
- maze::@= Winning=finite Position and |Won|=1.
- 2_PERSON_GAME::= Net{
- |-GAME and No_of_players=2. black,white::Players.
- Winning::=
- { p:Position
- || p in Won
- or p.moves==>Lost
- or for all q:p.moves, some r:q.moves (r in Winning)
- }.
- Loosing::= { p:Position || p in Lost or some p.moves & Winning or for some q:p.moves, all r:q.moves (r in Loosing) }.
- play_alternately::@= For some State:Sets ( Position = Players >< State )
- and for all p:Position, q:moves(p) ( p.1st<>q.1st ).

}=::2_PERSON_GAME. - BOARD_GAME::= Net{
- |-GAME.
- Board::Sets.
- Type_of_piece::Sets.
- |-Position=Board->{empty}|Piece.
- |-Piece=Players><Type_of_piece.
- For Piece p, Board b,
- Add(p,b)::=map[x:Position]{x'||x(b)=empty and x'(b)=p},
- Take(p,b)::=map[x:Position]{x'||x(b)=p and x'(b)=empty},
- Move(p,b1,b2)::=map[x:Position]
- {x'||x(b1)=p and x(b2)=empty and x'(b1)=empty and x'(b2)=p}.

}=::BOARD_GAME. - tictactoe::=$ Net{
- |-BOARDGAME(Position=>Grid).
- |-2_PERSON_GAME(play_alternately).
- |-Type_of_piece={mark}.
- nought::Piece=(black,mark),
- cross::Piece=(white, mark).
- |-Board=1..3><1..3.
- Rows::={ {(r,c):Board||r:1..3}||c:1..3 },
- Cols::={ {(r,c):Board||c:1..3}||r:1..3 },
- Diagonals::={ {(1,1),(2,2),(3,3)} , {(1,3),(2,2),(3,1)} }.
- |-Position=Player><Grid.
- Won::={p:Position
- || for some X:Rows|Cols|Diagonals, q:{nought,cross}, all b:X ( Position(b)=q )
- }.
- (above)|-Won={p:Position
- || for some X:Rows|Cols|Diagonals, q:{nought,cross}( X==>q./Position)
- }.
[click here if you can fill this hole]

}=::tictactoe. - |-BOARDGAME(Position=>Grid).

}=::SOLITAIRE.

. . . . . . . . . ( end of section Games) <<Contents | End>>

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

For a more rigorous description of the standard notations see