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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Tue, 14 Jun 2016 07:34:48 -0700 (PDT)*References*: <c9f9a016-fcd1-4d87-abc0-1b594b6455f0@googlegroups.com> <FEFF636D-58CE-42CF-AC5D-A01D63E11D45@gmail.com> <de4b10c7-87c0-4a96-bf3e-0727c2a8bb9f@googlegroups.com> <CC3A0CEB-C75B-4152-B2DC-A2CD2EF62F61@gmail.com>

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 kindf \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.

**Follow-Ups**:**Re: [tlaplus] Function domains in TLAPS***From:*Ron Pressler

**References**:**Function domains in TLAPS***From:*Ron Pressler

**Re: [tlaplus] Function domains in TLAPS***From:*Stephan Merz

**Re: [tlaplus] Function domains in TLAPS***From:*Ron Pressler

**Re: [tlaplus] Function domains in TLAPS***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Function domains in TLAPS** - Next by Date:
**Re: [tlaplus] Function domains in TLAPS** - Previous by thread:
**Re: [tlaplus] Function domains in TLAPS** - Next by thread:
**Re: [tlaplus] Function domains in TLAPS** - Index(es):