# Prove that a recursive program satisfies a logic predicate with implication and quantifiers by induction

i have this program to prove:

given the ex3 method below
Suppose that the formal parameter "a" has always at least 2 elements and that a.length > i >= 1
Prove that ex3 satisfies the following predicate:

ex3 (a, i) <==> (for all k 1 <= k <= i ==> a [k-1] == a [k] +1)

public static boolean ex3 (int[] a, int i) {
if (i == 1) {
return a[0]==a[1]+1;
}
else {
return ex3(a, i-1) && a[i-1]==a[i]+1;
}

}

1) Write explicitly the basic case P(1) for the proving by induction
2) Write explicitly the inductive case for the proving by induction
3) Prove that the base case P(1) of the proving by induction is true
4) Prove that the inductive case of the proving by induction is true


I made an attempt to prove with induction, but i don't know if it's correct.

The goal is to prove that a recursive function satisfies the given predicate.

For the first request i replaced the index with the min value

For the second request i write the induction case starting from i - 1 to i because is a recursive function

For the third request, i tried to prove the base case in this way:

Link to the image of the proof of the case base part 2

For the last request, i tried to prove the inductive case in this way:

Can somebody say to me if it's correct or what's wrong? Thanks