The Python function mergesort recursively sorts a list of numbers U using a recursive divide-and-conquer algorithm, then returns a sorted list S. The function head returns the first element of a nonempty list Q, and the function tail returns all but the first element of a nonempty list Q. Lines 0607 detect if U is trivially sorted. Lines 0916 split U into two halves, L and R, of approximately equal lengths. Lines 1718 recursively sort L and R. Lines 1928 merge the sorted L and R back into a sorted list S.

Prove that mergesorts splitting loop is correct (lines 09-16). Do not prove that the rest of the mergesort is correct. You must use a loop invariant. Your proof must have three parts: initialization, maintenance and termination.

1. Find a loop invariant for the splitting loop
2. Use loop invariant to prove the initialization part
3. Use loop invariant to prove the maintenance part
4. Use loop invariant to prove the termination part
5. Find the worst case run time of mergesorts merging loop(lines 19-28). Do not find the run time for the rest of mergesort. Your answer must define T(n) where n is the number of elements to be sorted.

01 def head (Q): 02 return QI0] 03 def tail(Q): 04 return Q[1:] 05 def mergesort (U): 06 if U-= [ ] or tail (U)-[]: 07 08 else: 09 10 return U while U != [ ] and tai l (U) !- [): 12 13 14 15 16 17 18 19 20 21 L-L + [head (U)] U-tail(U) R-R + [head(U) ] U-tail(U) L = mergesort (L) R mergesort (R) while L != [ ] and R !- []: if head (L) head (R): = S = S + [head (L)] L- tail(L) 23 24 25 26 27 28 else: S = S + [head (R)] R = tail(R) S=S+L+R return S