induction - proving a function's correctness -

1 def recmin(a): 2 if len(a) == 1: 3   return a[0] 4 else: 5   m = len(a) // 2 6   min1 = recmin(a[0..m-1]) 7   min2 = recmin(a[m..len(a)-1]) 8   return min(min1, min2) 

i'm trying prove partial correctness of function, figured out predicate of p(i):for array a=[0..i], len(a)=i+1 , when recmin[a]is called,then call terminates , returns t such 0<=t<=i a[t] min value

but feel predicate wrong , how prove postcondition a[0] min value