author nipkow Thu, 08 Jun 2006 13:49:53 +0200 changeset 19824 fafceecebef0 parent 19823 9e4573eaacb3 child 19825 bb5357536621
```--- a/src/HOL/ex/PresburgerEx.thy	Thu Jun 08 13:49:39 2006 +0200
+++ b/src/HOL/ex/PresburgerEx.thy	Thu Jun 08 13:49:53 2006 +0200
@@ -88,4 +88,18 @@
theorem "(\<exists>m::int. n = 2 * m) --> (n + 1) div 2 = n div 2"
by presburger

+text{* This following theorem proves that all solutions to the
+recurrence relation \$x_{i+2} = |x_{i+1}| - x_i\$ are periodic with
+period 9.  The example was brought to our attention by John
+Harrison. It does does not require Presburger arithmetic but merely
+quantifier-free linear arithmetic and holds for the rationals as well.
+
+Warning: it takes (in 2006) over 5 minutes! *}
+
+lemma "\<lbrakk> x3 = abs x2 - x1; x4 = abs x3 - x2; x5 = abs x4 - x3;
+         x6 = abs x5 - x4; x7 = abs x6 - x5; x8 = abs x7 - x6;
+         x9 = abs x8 - x7; x10 = abs x9 - x8; x11 = abs x10 - x9 \<rbrakk>
+ \<Longrightarrow> x1 = x10 & x2 = (x11::int)"
+by arith
+
end```