Fixed Points of Factorial Function
First, let's simplify your F a bit. Instead of

if (s x = 1): F g s = s[x -&gt;1]
otherwise:    F g s = g s[y -&gt; y*x, x -&gt; x -1]


we can equivalently write

if (s x = 1): F g s = s
otherwise:    F g s = g s[y -&gt; y*x, x -&gt; x -1]


since s is the same as s[x-&gt;1] in the case s x = 1.

Second, we need to be more precise. We can't write s[y -&gt; y*x, ...] since at the left of -&gt; we need a value, and y*x is not a value but an expression. More in detail, y is a variable name whose value (in the current state) is s y. So, we should write instead s[y -&gt; s y * s x, ...]. We get:

if (s x = 1): F g s = s
otherwise:    F g s = g s[y -&gt; s y * s x, x -&gt; s x - 1]


Now, let's check your fixed point claim. Let g be defined as follows:

if (s x &gt;=1): g s = s[x -&gt; 1]
otherwise:    g s = undefined


and let's compute F g s, aiming to check whether F g s = g s for all s.

F g s
= { definition of F }
if (s x = 1): s
otherwise:    g s[y -&gt; s y * s x, x -&gt; s x - 1]
= { let's call s' the last state }
if (s x = 1): s
otherwise:    g s'
      where s' = s[y -&gt; s y * s x, x -&gt; s x - 1]
= { definition of g }
if (s x = 1): s
otherwise:    if (s' x &gt;= 1): s'[x -&gt; 1]
              otherwise:      undefined
      where s' = s[y -&gt; s y * s x, x -&gt; s x - 1]
= { definition of s' }
if (s x = 1): s
otherwise:    if (s x - 1 &gt;= 1): s[y -&gt; s y * s x, x -&gt; 1]
              otherwise:      undefined
= { arithmetics }
if (s x = 1): s
otherwise:    if (s x &gt;= 2): s[y -&gt; s y * s x, x -&gt; 1]
              otherwise:      undefined


This looks quite different to g s! Indeed, your g is not a fixed point.

Intuitively, that code computes the factorial of x (times the original value of y) inside y, 
and loops forever on nonpositive x,
so I would expect a fixed point to be

g s = if (s x &gt;= 1):  s[y -&gt; (s y) * (s x)!, x -&gt; 1]
      otherwise:      undefined