Automatic proofs or model checking in an extremely simplified functional language 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) ?
The ACL2 system includes all of the features of your language, and supports impressive automated theorem proving about program in that language.

In ACL2, you would write the theorem you describe as:

(defthm f-g-equal (equal (f x) (g x)))


having previously defined f and g.