The array `H` is indexed from `5` to `m+2`.
Write a predicate saying that a smallest element of `H` is `2`. array_claim H[5...m+2] f_nodes 30 (EE i; 5 <= i <= m+2: H[i] = 2) /\ !(EE i; 5 <= i <= m+2: H[i] < 2) <=>
end_of_answer
Write a predicate saying that the smallest element of `H` is `2`. array_claim H[5...m+2] f_nodes 40 EE i; 5 <= i <= m+2: H[i] = 2 /\ AA j; 5 <= j <= m+2 /\ j != i: H[j] > 2 <=>
end_of_answer no_next_URL
or
This file was generated 2017-08-16 12:27:48 UTC.