下边是mergesort代码：
01 def head(Q):
02 return Q[0]
03 def tail(Q):
04 return Q[1:]
05 def mergesort(U):
06 if U == [] or tail(U) == []:
07 return U
08 else:
09 L = []
10 R = []
11 while U != [] and tail(U) != []:
12 L = L + [head(U)]
13 U = tail(U)
14 R = R + [head(U)]
15 U = tail(U)
16 L = L + U
17 L = mergesort(L)
18 R = mergesort(R)
19 S = []
20 while L != [] and R != []:
21 if head(L) <= head(R):
22 S = S + [head(L)]
23 L = tail(L)
24 else:
25 S = S + [head(R)]
26 R = tail(R)
27 S = S + L + R
28 return S
要找到一个循环不变量证明循环（line9-16）是正确的，这个循环不变量应该是U，循环开始之前U保持原始状态不变；每次循环迭代后U失去前两个元素分别给L和R，在下次循环开始之前U保持剩余元素不改变；循环结束的条件是U为空或只有一个元素，此时U保持判定false之前的状态依旧不变，若是剩余一个元素，语句L=L+U将其加入到L中，满足将元素依次加到L和R中的功能。
不知道我这样理解对不对，求大佬解答
