# Re: [tlaplus] Function domains in TLAPS

BTW, just to provide some context:
Inspired by the discussion of FL's algebraic stack, I defined an iterated function application operator like so:

RECURSIVE Yn(_, _, _)

Yn(X, f, n) == \* apply f, n times; X is the identity domain, i.e. X = DOMAIN Yn(X, f, 0)

LET Yn1 == Yn(X, f, n-1)

D   == {x \in DOMAIN Yn1 : Yn1[x] \in DOMAIN f} IN

IF n = 0 THEN [x \in X |-> x]

ELSE [x \in D |-> f[Yn1[x]]]

Then (mostly as an exercise to learn TLAPS) I wanted to see how many axioms specifying Yn are required to be able to deduce various theorems about it; e.g.:

THEOREM \A f, X : \A m, n \in Nat : n >= m => DOMAIN Yn(X, f, n) \subseteq DOMAIN Yn(X, f, m)

THEOREM \A f, X : \A n \in Nat : \A x \in DOMAIN Yn(X, f, n+1) :

f[Yn(X, f, n)[x]] = Yn(X, f, n)[f[x]]

It turns out you need quite a few (at least I couldn't do it with less than five or so)...