# Re: [tlaplus] Generating sequences of functions

• From: Isaac DeFrain <isaacdefrain@xxxxxxxxx>
• Date: Mon, 4 Oct 2021 17:16:02 -0600
• References: <CAN3aEu7h=uR+4EJSBNP9qMGWddzpkPFo8bccUjPeKFovob-tsQ@mail.gmail.com>

Hey Pablo,

If you only need an implicit (non-enumerable) definition, this will do the trick:

Seq_n(n, s) == { seq \in Seq(s) : Len(seq) <= n }

If you need an explicit definition, a recursive definition will do the trick:

RECURSIVE seq_n(_, _, _)
seq_n(n, s, acc) ==
IF n = 0 THEN acc
ELSE
LET next == { Append(a, x) : x \in s, a \in acc }
IN seq_n(n - 1, s, acc \cup next)

\* set of sequences of length at most n
Seq_n(n, s) == seq_n(n, s, {<<>>})

I hope this helps!

Best,

Isaac DeFrain

On Mon, Oct 4, 2021 at 4:35 PM pablo fernandez <fernandezpablo85@xxxxxxxxx> wrote:
Hello!

I have a function that represents a transaction:

[user: 1..3, amount: 1..6]

And would like to have the set of all sequences from 0 to 3 transactions, e.g:

{<<>>, <<[user:1, amount: 0]>>, <<[user:1, amount: 0], [user:2, amount: 0]>> ... }

How can I achieve this?

Pablo

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAN3aEu7h%3DuR%2B4EJSBNP9qMGWddzpkPFo8bccUjPeKFovob-tsQ%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAM3xQxHs7AsuL5towz30_6p8eT%3DypJGijnURv2EOg3MX8NBABA%40mail.gmail.com.