The problem that the GLUT-maker faces is that she knows the human’s function, h(x,y)=z, and she must create a GLUT function, y=g(x), such that g(x)=h(x,g(x)) for all x. I presume that there is math out there which says what features h(x,y) must have in order for this to be possible, but I don’t know it.
What about Exists y: h(x,y) = y? If this holds, take Forall x: g(x) = y and we are done.
Edit: to be more general, we can let y depend on x, which gives Forall x: Exists y(x): h(x,y(x)) = y(x), but that is actually the original statement with the letter y standing in place of the original g. I doubt there is anything more to say about such functions, at least in general.
What about Exists y: h(x,y) = y? If this holds, take Forall x: g(x) = y and we are done.
Edit: to be more general, we can let y depend on x, which gives Forall x: Exists y(x): h(x,y(x)) = y(x), but that is actually the original statement with the letter y standing in place of the original g. I doubt there is anything more to say about such functions, at least in general.