Thank you for finding time to respond.
I'm not sure though I understand how the above can work out. Model verification for Limit=1 yields
```
The first argument of >= should be an integer, but instead it is:
0..1
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 22, column 5 to line 23, column 22 in chnumerals
1. Line 22, column 8 to line 22, column 15 in chnumerals
2. Line 23, column 8 to line 23, column 22 in chnumerals
3. Line 18, column 5 to line 19, column 35 in chnumerals
4. Line 18, column 8 to line 18, column 34 in chnumerals
5. Line 18, column 15 to line 18, column 34 in chnumerals
6. Line 18, column 15 to line 18, column 31 in chnumerals
7. Line 9, column 30 to line 9, column 64 in chnumerals
8. Line 9, column 33 to line 9, column 42 in chnumerals
```
and it also gives warnings about SetNext - `SetNext is never enabled` and the same for ComputationComplete.
I see that in my spec I made a mistake of passing L as a set, it seems it better be defined a parameter instead.
In Church encoding `succ` function is defined as follows:
```
succ = λ n . λ s . λ z . s (n s z)
```
so, in order to make it work successor function must be extended with one more argument. It seems plausible that the type of argument `s` could be [MyNat -> MyNat] (a function taking a number and returning a number `0..Limit`) and a type of `z` could be just `MyNat`.
Recalling definition of any n-th Church numeral (number of s invocations in the functions body equals to the integer that numeral corresponds to):
```
Cn = λ s . λ z . s (s ... (s z))) - n invocations of s
```
so given definition in the spec the type of Church numeral should rather be [MyInt -> MyInt] -> [MyInt -> MyInt] - lets call it ChurchT for brevity, as a signature of "reduceable" church numeral could be represented as follows, argument type highlighted in yellow:
```
Cn = λ s : (integer -> integer) . λ z : integer . s (s ... (s z))) - n invocations of s
```
So in order to make it work only one missing piece remains - define a proper type for argument `n`.
But we know that successor function takes a Church numeral and returns back Church numeral, so given this its definition should be `ChurchT -> ChurchT` or, in other words
```
[
[[MyInt -> MyInt] -> [MyInt -> MyInt]]
->
[[MyInt -> MyInt] -> [MyInt -> MyInt]]
]
```
attempt to define this as
```
LSucc == \* Successor function for generating next Church numeral
[n \in [[[MyInt -> MyInt] -> [MyInt -> MyInt]] -> [[MyInt -> MyInt] -> [MyInt -> MyInt]]] |->
[s \in [MyNat -> MyNat] |->
[z \in MyNat |-> s[n[s][z]] ]
]
]
```
yields the following warning:
```
Unknown operator: `MyInt'.
```
So, it brings the following questions:
* Is it possible to have a some sort of type aliasing for function declarations? I.e. is it possible to somehow define `ChurchT` type?
* How can type of argument n could be fixed in the declaration of LSucc?
My full spec now looks as follows:
```