Go backward to Lifted Domains Go up to Top |
Recursive function definitions need not define a function uniquely!
q(x) = (equals x zero) -> one [] q(plus x one)
f1(x)={
one if x = zero _|_ otherwise f2(x)={
one if x = zero two otherwise f3(x) = one
How to formmalize that q yields the intended denotation f1?
(the problem will be handled later)
(same with recursive domain definitions)