1
$\begingroup$

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

enter image description here

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

enter image description here

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

enter image description here

enter image description here

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:

enter image description here

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

$\endgroup$
  • 4
    $\begingroup$ I'm voting to close this question as off-topic because it's a check-my-work kind of thing. $\endgroup$ – Rick Decker Aug 26 at 20:58