Note: "Tatami" are natural fiber mats used in traditional Japanese homes. The size of a room is measured by the number of tatami on its floor, where each tatami is a rectangle, about 5 by 3 feet. Thus a 2 tatami room, like a 2 tatami proof, is pretty small, an 8 tatami room (or proof) is ok, but a 12 tatami room (or proof) is getting large, and should probably be subdivided.

Tatami are cool, refreshing and aromatic; we hope you find the tatami backgrounds helpful while browsing our proofs.

• Algebraic Semantics of Imperative Programs.
• Theorem Proving and Algebra.

• Tutorial material on hidden algebra, induction, first order logic, etc.;
• "A Hidden Agenda" for complete details; and
• "Extended Abstract of a Hidden Agenda" for a brief but precise overview.

1. An inductive proof that 1+...+ n = n(n+1) / 2.
2. A coinductive proof of a behavioral property of a simple flag object.
3. A proof of behavioral correctness of array-with-pointer implementation of stack, using coinduction.
4. An inductive proof for lists that the reverse of the reverse of a list is the list, plus some lemmas, including that append is associative.
5. A behavioral refinement proof of the correctness of implementing sets with lists, using attribute coinduction.
6. An inductive proof of a formula for the sum of the squares of the first n natural numbers.
7. A coinductive correctness proof for the tatami protocol, which maintains the consistency of distributed cooperative proofs that are built using the tatami system.