[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Function domains in TLAPS

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.