diff --git a/prompts/humaneval-dafny-cot/steps/002/examples/002/answer.txt b/prompts/humaneval-dafny-cot/steps/002/examples/001/answer.txt
similarity index 100%
rename from prompts/humaneval-dafny-cot/steps/002/examples/002/answer.txt
rename to prompts/humaneval-dafny-cot/steps/002/examples/001/answer.txt
diff --git a/prompts/humaneval-dafny-cot/steps/002/examples/002/question.txt b/prompts/humaneval-dafny-cot/steps/002/examples/001/question.txt
similarity index 100%
rename from prompts/humaneval-dafny-cot/steps/002/examples/002/question.txt
rename to prompts/humaneval-dafny-cot/steps/002/examples/001/question.txt
diff --git a/prompts/humaneval-dafny-cot/steps/003/001/answer.txt b/prompts/humaneval-dafny-cot/steps/003/001/answer.txt
new file mode 100644
index 0000000..8fc2cd2
--- /dev/null
+++ b/prompts/humaneval-dafny-cot/steps/003/001/answer.txt
@@ -0,0 +1,15 @@
+As we've seen, the loop in the `sum_loop` function goes over the elements of the array `numbers` and adds them to the `s` variable, which is equal to the `sum(numbers[..i])` for all `i`, such that `0 <= i <= |numbers|`. This means that during the execution of the loop the following invariant holds:
+1. `0 <= i <= |numbers|`
+2. `s == sum(numbers[..i])`
+
+The second invariant might be a bit difficult to prove, as it adds the last element of the array to the sum, while, as I've said before, the `sum` function is defined as `sum(a) == a[0] + sum(a[1..])`. However, as we've seen, it's possible to use the `sum_prop` function to prove that this invariant holds.
+Let's work out how to use it. If applied to the `numbers[..i + 1]`, we get:
+`sum(numbers[..i + 1]) == sum(numbers[..i + 1][..i]) + numbers[i]`. It might be difficult for dafny to prove that `sum(numbers[..i + 1][..i]) == sum(numbers[..i])`, so I'd suggest adding an assertion before calling `sum_prop` to make sure that this is the case, namely `assert numbers[..i + 1][..i] == numbers[..i]`.
+So, to use the `sum_prop`, I'd suggest the following code:
+```
+assert numbers[..i + 1][..i] == numbers[..i];
+sum_prop(numbers[..i + 1][..i]);
+assert sum(numbers[..i + 1]) == sum(numbers[..i + 1][..i]) + numbers[i];
+```
+
+In conclusion, we can say that two invariants hold and the second one could be proved using the `sum_prop` function.
diff --git a/prompts/humaneval-dafny-cot/steps/003/001/question.txt b/prompts/humaneval-dafny-cot/steps/003/001/question.txt
new file mode 100644
index 0000000..0079663
--- /dev/null
+++ b/prompts/humaneval-dafny-cot/steps/003/001/question.txt
@@ -0,0 +1,27 @@
+As we've already analyzed the specifications and the loops, it's time to try to analyze what invariants and patterns hold during the execution of the program. Go over the found loops in the following program in the code and try to find out what invariants and patterns they hold.
+```dafny
+function sum(s: seq<int>) : int {
+    if |s| == 0 then 0 else s[0] + sum(s[1..])
+}
+
+lemma sum_prop(s: seq<int>)
+    requires |s| > 0
+    ensures sum(s) == sum(s[..|s| - 1]) + s[ |s| - 1 ]
+{
+    if (|s| > 1) {
+        assert (s[1..][..|s[1..]| - 1]) == s[1..|s| - 1];
+    }
+}
+method sum_loop(numbers: seq<int>) returns (s: int)
+    ensures s == sum(numbers)
+{
+    s := 0;
+    var i := 0;
+    while (i < |numbers|)
+    {
+        s := s + numbers[i];
+
+        i := i + 1;
+    }
+}
+```
diff --git a/prompts/humaneval-dafny-cot/steps/003/question.txt b/prompts/humaneval-dafny-cot/steps/003/question.txt
new file mode 100644
index 0000000..d2236e0
--- /dev/null
+++ b/prompts/humaneval-dafny-cot/steps/003/question.txt
@@ -0,0 +1,4 @@
+As we've already analyzed the specifications and the loops, it's time to try to analyze what invariants and patterns hold during the execution of the program. Go over the found loops in the following program in the code and try to find out what invariants and patterns they hold.
+```dafny
+{program}
+```