Dixon's Problem
---------------

------
Summary:

------
Definitions:

P0 <-> (P0 <-> P1)
P1 <-> (P1 <-> P2)
...
Pi <-> (Pi <-> P(i+1))
...
Pn <-> (Pn <-> P0)

so something like 

q(N) = forall 0 <= i < N.  p(i) <-> (p(i) <-> p(s(i))) 
                        /\ p(N) <-> (p(N) <-> p(0)) 

------

Theorem:
forall n. q(N) -> p(0)

------
Comments:

Also I have another problem, that I havn't tried in
lambdaClam/Isaplanner yet, but you might find
interesting (it was from the Automath conference).

Interestingly this problem is easy for classical logic, but less easy if
you are using intuitionistic logic (but still true and provable). Either
way induction is a natural way to solve the problem.

------
Source:

Lucas Dixon, Edinburgh MRG group.