Formalize the hopping algorithm, an accelerated version of the iterat…

…ion algorithm, to find the two squares for a tik prime.

examples/fermat/twosq/README.md

@@ -17,3 +17,4 @@ These theories support the formalisation of an algorithm for Fermat's Two Square
 * __twoSquares__, existence, uniqueness and algorithm of two squares theorem.
 * __quarity__, zig and zag, tik and tok, mill structure, and search for two squares.
 * __corner__, an adaptation of a partition proof using corner pieces.
+* __hopping__, ping, pong and pung, with path and nodes justifying the hopping algorithm for two squares.

examples/fermat/twosq/files.txt

@@ -10,16 +10,18 @@
 * helperSet
 * helperFunction
 
-1 windmill       -- definitions of windmill, mill, flip, and zagier.
-0 helperTwosq
-
 1 involute       -- basic properties of involution.
 0 helperTwosq
 
 2 involuteFix    -- pairs and fixes of involution.
 1 involute
 0 helperTwosq
 
+3 windmill       -- definitions of windmill, mill, flip, and zagier.
+2 involuteFix
+1 involute
+0 helperTwosq
+
 2 involuteAction -- involution and group action.
 1 involute
 0 helperTwosq
@@ -41,19 +43,30 @@
 4 twoSquares     -- existence, uniqueness and algorithm (clean version for paper).
 2 involuteFix
 1 involute
-1 windmill
+3 windmill
 3 iterateCompose
 1 iterateCompute
 0 iteration
-0 groupAction
 0 helperTwosq
+* groupAction
 
-2 quarity        -- bound and listing of mills and search for sum of two squares.
-1 windmill
+4 quarity        -- bound and listing of mills and search for sum of two squares.
+3 windmill
 0 helperTwosq
 
 3 corner         -- an adaptation of a partition proof using corner pieces.
 2 quarity
 2 involuteFix
 1 involute
 0 helperTwosq
+
+5 hopping        -- path and nodes justifying the hopping algorithm for two squares.
+3 iterateCompose
+1 iterateCompute
+0 iteration
+2 involuteFix
+1 involute
+3 windmill
+4 quarity
+4 twoSquares
+0 helperTwosq