Commit 82082f1f authored by Kirill Smelkov's avatar Kirill Smelkov

.

parent d82ed1a5
......@@ -143,7 +143,7 @@ RECURSIVE SeqDecreasing(_)
SeqDecreasing(S) ==
CASE S = << >> -> TRUE
[] Len(S) = 1 -> TRUE
[] OTHER -> (S[2] =< S[1]) /\ SeqDecreasing(Tail(S))
[] OTHER -> (S[2] < S[1]) /\ SeqDecreasing(Tail(S))
\* SeqSet converts sequence S to set of its values.
SeqSet(S) == {S[x]: x \in DOMAIN S}
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment