more theorems about folds

[muenchnerkindl]

This PR mainly adds theorems about folds on functions and sequences.

I haven't tried to include running proofs as part of the CI.

[muenchnerkindl]

Happy New Year to everybody! Would somebody have some time to look at this PR?

[kape1395]

I can try.

[muenchnerkindl]

I added some more functions, in particular about folding a function, and I believe this is now in a state that can be merged into the master branch.

[kape1395]

This fails for me with tlapm from the current main:

File "./FunctionTheorems_proofs.tla", line 882, characters 3-4:
[ERROR]: Could not prove or check:
           ASSUME Surjection(S, T) ==
                    {M \in [S -> T] : \A t \in T : \E s \in S : M[s] = t},
                  Bijection(S, T) == Injection(S, T) \cap Surjection(S, T),
                  NEW CONSTANT S,
                  NEW CONSTANT f \in 
                  Bijection(1..1, S),
                  1..1 = {1} 
           PROVE  \E s : S = {s}
File "./FunctionTheorems_proofs.tla", line 1, character 1 to line 1412, character 77:
[ERROR]: 1/732 obligations failed.

[muenchnerkindl]

This fails for me with tlapm from the current main:

File "./FunctionTheorems_proofs.tla", line 882, characters 3-4:
[ERROR]: Could not prove or check:
           ASSUME Surjection(S, T) ==
                    {M \in [S -> T] : \A t \in T : \E s \in S : M[s] = t},
                  Bijection(S, T) == Injection(S, T) \cap Surjection(S, T),
                  NEW CONSTANT S,
                  NEW CONSTANT f \in 
                  Bijection(1..1, S),
                  1..1 = {1} 
           PROVE  \E s : S = {s}
File "./FunctionTheorems_proofs.tla", line 1, character 1 to line 1412, character 77:
[ERROR]: 1/732 obligations failed.

That's annoying, in particular since I did not at all touch that proof (and of course tlapm --cleanfp FunctionTheorems_proofs.tla reports no error on my side). I just rebuilt tlapm (471b481-dirty) on MacOS 26.2, and Z3 proves the obligation in no time (0.3s). How can we track and fix such spurious errors?