有序单向链表的插入（链表有序性的谓词描述）
将一个新节点插入到有序单向链表中，使链表的有序性保持不变。 （验证时间约104sec）
[Back to Index]
验证特点：有序单向链表、表段的归纳谓词描述，引理。
标注说明：函数前条件：head指向长为m的有序单向链表；
函数后条件：返回值\result 指向长为m+1的有序单向链表，根据新节点在链表中的插入位置，分别给出了\result与oldhead之间的对应关系。
程序样例 
