Loop Invariant: The Algm will always give the max number of flowers we can put in the first i plots of given flowerbed; and there is no way to move any flower(1) to any previous plot but still get the max result.

Proof:

Base case (All correct):

0, 1 —> 1

00, 10 —> 10

01 —> 01

000, 001, 100, 101 —> 101

010 —>010

Assume the Algm will always give the max number of flowers we can put in the first i plots for all length i <=n;

For i ==n+1;

First we run the algm on the first n elements and get the result.

Case 1: the n’th plot of the result is 0, we can put 1 more flower in n+1 'th plot, the answer must be still correct;

Case 2: the n’th plot of result is 1, n+1 'th plot is empty(0), according to the Algm, there is no way to move any flower(1) to any previous plot but still get the max result, so there is no way to add flower to n+1 th plot.

Case 3: the n’th plot of result is 1, n+1 ‘th plot is flower(1), we must remove the flower in n’th plot. Again, since there is no way to move any flower(1) to any previous plot but still get the max result, there is no way to add extra flower, the answer must be still correct.

```
public class Solution {
public boolean canPlaceFlowers(int[] flowerbed, int n) {
if(n==0) return true;
else if(flowerbed==null || flowerbed.length<n) return false;
int len = flowerbed.length;
for(int i=0; i<len; i++){
//Greedy Algm: Add flower whenever we can if no neighbor has flower
if(flowerbed[i]==0 && (i==0 || flowerbed[i-1]==0) && (i+1==len || flowerbed[i+1]==0)){
flowerbed[i]=1;
n--;
if(n==0) return true;
}
}
return false;
}
}
```