rename LemmaRepeatCommutative

viperproject · Dec 4, 2024 · 1da4e70 · 1da4e70
1 parent c87b588
commit 1da4e70
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/bytes/repeat_lemmas.gobra b/bytes/repeat_lemmas.gobra
@@ -27,7 +27,7 @@ ghost
 requires n >= 0
 ensures  b ++ Repeat(b, n) == Repeat(b, n) ++ b
 decreases
-func LemmaRepeatCommutative(b seq[byte], n int) {
+func LemmaRepeatCommutesWithConcat(b seq[byte], n int) {
 	assert b ++ Repeat(b, n) == Repeat(b, n+1)
 	lemmaRepeatFlip(b, n+1)
 }
@@ -42,7 +42,7 @@ func LemmaRepeatDoubled(b seq[byte], n int) {
 		assert Repeat(b, n) ++ Repeat(b, n) == b ++ Repeat(b, n - 1) ++ b ++ Repeat(b, n - 1)
 		// order of repeating doesn't matter because it's always the same element that is repeated
 		assert b ++ Repeat(b, n - 1) ++ b ++ Repeat(b, n - 1) == b ++ (Repeat(b, n - 1) ++ b) ++ Repeat(b, n - 1)
-		LemmaRepeatCommutative(b, n - 1)
+		LemmaRepeatCommutesWithConcat(b, n - 1)
 		assert b ++ (Repeat(b, n - 1) ++ b) ++ Repeat(b, n - 1) == b ++ (b ++ Repeat(b, n - 1)) ++ Repeat(b, n - 1)
 		assert b ++ Repeat(b, n - 1) ++ b ++ Repeat(b, n - 1) == b ++ b ++ Repeat(b, n - 1) ++ Repeat(b, n - 1)
 		LemmaRepeatDoubled(b, n - 1)