Verify that f3 is a meaning of q:
Verify that f3 is a meaning of q:
for any n ? Nat, n equals zero ? one [] f3(n plus one)
= n equals zero ? one [] one
= one
= f3(n)
Similarly we can show that f1 and f2 are meanings fof q.
So which of these functions does q really stand for, if any?
Unfortunately, the tools as currently developed are not
sophisticated enough to answer this question (see section 6).