Very strange behaviour of definition evaluation (partial functions (& constructors?))

[Bart Bogaerts]

See attached file: in_dir and neighbor should be interpreted equal after evaluating the functions. However, they are not. Somehow, if we remove some of the rules defining neighbor, we get "good" behaviour again.

VERY WEIRD!

This theory should probably have no models since we are referring to pos(x,y+1) with y the max y coordinate. Still, for some reason this behaviour does not show if there are a lot of defining rules.