AA树中节点的插入或删除
AA树是在一般的二叉树结点中增加了level这一属性。同时规定：
1、每个叶子的level是1；
2、每个左孩子的level是其父结点的level减1；
3、每个右孩子的level等于其父结点的level或等于其父结点的level减1；
4、每个右孙子的level一定比其祖父的level小；
5、每个level大于1的结点有两个孩子。
当对AA树进行节点插入或节点删除时，根据以上条件可以用来标记和调整AA树的结构，使其每个结点满足level值的规定。
左旋和右旋是用于调整AA树结构的方法，当连续三个右孩子level值相同时使用左旋操作，当连续两个左孩子level值相同时使用右旋操作。（验证时间约为 3560sec）
验证特点：AA树，内置谓词 \tree，自定义谓词，引理，逻辑变量，幽灵形参，\assert断言
标注说明：
这里只给出插入和删除函数的简单说明，其他函数请参见各函数的标注。
（1）插入函数 AAinsert。
函数前条件：t是一个AA树，t和它右子树的高度（level）分别为m和n，要插入的数据为data。
逻辑变量 oldt 记录函数入口处根节点实参的值。
函数后条件：返回值 \result 为一个AA树。描述新节点插入后AA树的各种情况，\result 为空树、
节点插在树根或其他中间或叶子节点。
（2）删除函数 AAdelete。
函数前条件：t是一个AA树，要删除节点的数据为data。
函数后条件：返回值 \result 为一个AA树。描述节点删除后AA树的各种情况：原树为空树，
原树只有一个节点且被删除，根节点或其它节点被删除等。
程序样例 
