On Tuesday, June 14, 2016 at 5:29:29 PM UTC+3, Stephan Merz wrote:
Correct, this is still too unspecific because f[3] denotes some value even if 3 is not an element of the domain of f. I was thinking of assumptions of the kind
f \in [ 0 .. 10 -> Nat ]
that help you reduce DOMAIN f to a specific set.
Oh, OK. Thanks. Unfortunately, I can't specify the function's domain because the function (and its domain) is computed by a recursive operator (and as TLAPS doesn't support recursive operators, I also specified the function with axioms), but had trouble proving things unless I stated separate axioms and theorems about the function's domain, in addition to the mapping.