Skip to content

Commit 7925ce0

Browse files
align statement of ReverseSubSeq
1 parent 86c8cd7 commit 7925ce0

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

modules/SequencesExtTheorems.tla

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -144,7 +144,7 @@ THEOREM ReverseSingleton == \A x : Reverse(<< x >>) = << x >>
144144

145145
THEOREM ReverseSubSeq ==
146146
ASSUME NEW S, NEW seq \in Seq(S),
147-
NEW m \in 1..Len(seq), NEW n \in 1..Len(seq)
147+
NEW m \in 1..Len(seq), NEW n \in 0..Len(seq)
148148
PROVE Reverse(SubSeq(seq, m , n)) = SubSeq(Reverse(seq), Len(seq)-n+1, Len(seq)-m+1)
149149

150150
THEOREM ReversePalindrome ==

0 commit comments

Comments
 (0)