| Hi Francesco, as far as I can tell, your function is not well specified for an empty set of sequences, so I'll assume that the function need produce the correct result only when the input set is non-empty. I'll also assume that all sequences have the same length. Then you can write something like the following (* Auxiliary function to sum the i-th components of all sequences in S *) sumi(i,S) == LET s[T \in SUBSET S] == IF T = {} THEN 0 ELSE LET x == CHOOSE x \in T : TRUE IN x[i] + s[T \ {x}] IN s[S] SumSet(S) == LET l == Len(CHOOSE x \in S : TRUE) IN [i \in 1 .. l |-> sumi(i,S)] (Of course, you can put the definition of sumi inside the LET in the definition of SumSet if you don't want that operator to be visible on the top level.) I used TLC to check that SumSet({<<1,2,3>>, <<3,4,6>>) = <<4,6,9>> and SumSet({<<1,2,3>>, <<1,2,3>>, <<1,2,3>>}) = <<1,2,3>> Best, Stephan
|