Imagine a stripped down functional programming language, that has the following properties

• The only value type is an integer
• There are no side effects
• Functions are defined as a single expression, value of which becomes the return value of the function.
• Program consists of zero or more function definitions and an expression. The expression can be defined in terms of the previously defined functions. Value of that evaluated expression is the result of the program.
• Aside from simple arithmetic, there is only an if then else fi expression
• The only way to do looping is through recursion

A program can then look like

f(x) = r(x+1,1)
r(x,y) = if x-(y*y) then r(x,y+1) else y*y fi

f(2)

so f() computes the second power of the given argument.

My question is, whether it is possible with current automated tools to prove theorems about such programs without human assistance. And what exactly?

Is it for example possible to automatically say for sure that for two functions f and g for every x: f(x) = g(x) ?