## TinyChess — the proofs.
##
## LAWS.bend states the laws; this file fills them, one def per law, under
## the alias the import gives them. `bend PROOF.bend` is the gate: it prints
## "All terms check." once every law holds, a TODO count while any is open,
## and a counterexample when one is false.
##
## Every proof here is {==}. Each law is about one position, so the checker
## settles it by running the search rather than by being argued with. The
## seven laws about every square and every board are still open, so this
## file stops at the TODO count until somebody writes the induction.

import Base
import ./LAWS.bend as Laws

def Laws.white_cannot_win_on_the_first_turn():
  {==}

def Laws.queens_for_both_keep_the_law():
  {==}

def Laws.a_queen_for_white_alone_wins():
  {==}

def Laws.a_knight_for_white_alone_does_not():
  {==}

def Laws.c3_is_check_but_not_mate():
  {==}