load bintree.maude fmod BIN-SEARCH-TREE is protecting BINTREE-NAT1 . sort BinSearchTree . subsort BinSearchTree < BinTree . var BT : BinTree . vars BST BST1 BST2 : BinSearchTree . vars N M : Nat . cmb BT : BinSearchTree if isSearchTree(BT) = true . op insertSorted : BinSearchTree Nat -> BinSearchTree . eq insertSorted(empty, N) = bintree(empty, N, empty) . eq insertSorted(empty, N) = bintree(empty, N, empty) . ceq insertSorted(bintree(BST1, N, BST2), M) = bintree(BST1, N, insertSorted(BST2, M)) if N <= M = true . ceq insertSorted(bintree(BST1, N, BST2), M) = bintree(insertSorted(BST1, M), N, BST2) if M < N = true . endfm fmod TEST-SEARCH-TREE is protecting BIN-SEARCH-TREE . ops tree1 tree2 : -> BinTree . *** The first one corresponds to one in book eq tree1 = bintree( bintree(empty, s(s(0)), bintree(empty, s(s(s(0))), empty)), s(s(s(s(0)))), bintree( bintree(empty, s(s(s(s(s(s(0)))))), empty), s(s(s(s(s(s(s(0))))))), bintree(empty, s(s(s(s(s(s(s(s(s(0))))))))), empty))) . eq tree2 = bintree( bintree(empty, s(s(0)), bintree(empty, s(s(s(0))), empty)), s(s(s(s(0)))), bintree( bintree(empty, s(s(s(s(s(s(0)))))), empty), s(s(s(s(s(0))))), bintree(empty, s(s(s(s(s(s(s(s(s(0))))))))), empty))) . endfm red tree1 . red tree2 . red insertSorted(tree1, 0) . red insertSorted(tree1, s(0)) . red insertSorted(tree1, s(s(0))) . red insertSorted(tree1, s(s(s(0)))) . red insertSorted(tree1, s(s(s(s(0))))) . red insertSorted(tree1, s(s(s(s(s(0)))))) . red insertSorted(tree1, s(s(s(s(s(s(0))))))) . red insertSorted(tree1, s(s(s(s(s(s(s(0)))))))) . red insertSorted(tree1, s(s(s(s(s(s(s(s(0))))))))) . red insertSorted(tree1, s(s(s(s(s(s(s(s(s(0)))))))))) . red insertSorted(tree1, s(s(s(s(s(s(s(s(s(s(0))))))))))) .