in nat-bin-tree.maude fmod NAT-SEARCH-TREE is protecting NAT-BIN-TREE . sorts SearchTree NeSearchTree . subsort NeSearchTree < SearchTree < BinTree . subsort NeSearchTree < NeBinTree . op insert : SearchTree Nat -> SearchTree . op delete : SearchTree Nat -> SearchTree . op find : SearchTree Nat -> Bool . op min : NeSearchTree -> Nat . op max : NeSearchTree -> Nat . vars N M : Nat . vars SL SR : SearchTree . vars NESL NESR : NeSearchTree . mb empty-tree : SearchTree . mb empty-tree [N] empty-tree : NeSearchTree . cmb NESL [N] empty-tree : NeSearchTree if max(NESL) < N . cmb empty-tree [N] NESR : NeSearchTree if N < min(NESR) . cmb NESL [N] NESR : NeSearchTree if max(NESL) < N and N < min(NESR) . eq insert(empty-tree, M) = empty-tree [M] empty-tree . eq insert(SL [N] SR, N) = SL [N] SR . ceq insert(SL [N] SR, M) = insert(SL, M) [N] SR if M < N . ceq insert(SL [N] SR, M) = SL [N] insert(SR, M) if N < M . eq delete(empty-tree, N) = empty-tree . ceq delete(SL [N] SR, M) = delete(SL, M) [N] SR if M < N . ceq delete(SL [N] SR, M) = SL [N] delete(SR, M) if M > N . eq delete(empty-tree [N] SR, N) = SR . eq delete(SL [N] empty-tree, N) = SL . eq delete(NESL [N] NESR, N) = NESL [min(NESR)] delete(NESR, min(NESR)) . eq find(empty-tree, N) = false . eq find(SL [N] SR, N) = true . ceq find(SL [N] SR, M) = find(SL, M) if M < N . ceq find(SL [N] SR, M) = find(SR, M) if M > N . eq min(empty-tree [N] SR) = N . eq min(NESL [N] SR) = min(NESL) . eq max(SL [N] empty-tree) = N . eq max(SL [N] NESR) = max(NESR) . endfm red insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s(0)))))))))), s(s(s(s(s(s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s(s(0))))))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), s(s(s(s(0))))), s(s(0))) . ***( reduce in NAT-SEARCH-TREE : insert(insert(insert(insert( insert(insert(insert(insert(insert(insert(insert(insert( insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s(s(s(s(s(s(s(s(s( s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s(0)))))))))), s(s(s(s(s( s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s(s(0))))))))), s(s(s(s(s( s(s(s(s(s(s(s(0))))))))))))), s(s(s(s(0))))), s(s(0))) . rewrites: 1043 in -10ms cpu (0ms real) (~ rewrites/second) result NeSearchTree: ((empty-tree[0]empty-tree)[s(0)]((empty-tree[ s(s(0))]empty-tree)[s(s(s(0)))](empty-tree[s(s(s(s( 0))))]empty-tree)))[s(s(s(s(s(0)))))]((empty-tree[s(s(s(s(s(s( 0))))))]empty-tree)[s(s(s(s(s(s(s(0)))))))](((empty-tree[s(s( s(s(s(s(s(s(0))))))))]empty-tree)[s(s(s(s(s(s(s(s(s( 0)))))))))](empty-tree[s(s(s(s(s(s(s(s(s(s( 0))))))))))]empty-tree))[s(s(s(s(s(s(s(s(s(s(s(0)))))))))))]( empty-tree[s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))]empty-tree))) *** 5 *** / \ *** / \ *** / \ *** 1 7 *** / \ / \ *** 0 3 6 11 *** / \ / \ *** 2 4 9 12 *** / \ *** 8 10 ) red preorder( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s(0)))))))))), s(s(s(s(s(s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s(s(0))))))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), s(s(s(s(0))))), s(s(0)))) . ***( reduce in NAT-SEARCH-TREE : preorder(insert(insert( insert(insert(insert(insert(insert(insert(insert(insert( insert(insert(insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s( s(s(0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s( s(s(s(s(s(s(s(s(s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s( 0)))))))))), s(s(s(s(s(s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s( s(0))))))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), s(s(s(s( 0))))), s(s(0)))) . rewrites: 1095 in -10ms cpu (0ms real) (~ rewrites/second) result NeList: s(s(s(s(s(0))))) : s(0) : 0 : s(s(s(0))) : s(s(0)) : s(s(s(s(0)))) : s(s(s(s(s(s(s(0))))))) : s(s(s(s(s(s(0)))))) : s(s(s(s(s(s(s(s(s(s(s(0))))))))))) : s(s(s(s(s(s(s(s(s( 0))))))))) : s(s(s(s(s(s(s(s(0)))))))) : s(s(s(s(s(s(s(s(s(s( 0)))))))))) : s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) : [] ) red inorder( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s(0)))))))))), s(s(s(s(s(s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s(s(0))))))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), s(s(s(s(0))))), s(s(0)))) . ***( reduce in NAT-SEARCH-TREE : inorder(insert(insert(insert( insert(insert(insert(insert(insert(insert(insert(insert( insert(insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s(s(s( 0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s(s(s( s(s(s(s(s(s(s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s( 0)))))))))), s(s(s(s(s(s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s( s(0))))))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), s(s(s(s( 0))))), s(s(0)))) . rewrites: 1095 in -10ms cpu (0ms real) (~ rewrites/second) result NeList: 0 : s(0) : s(s(0)) : s(s(s(0))) : s(s(s(s(0)))) : s(s(s(s(s(0))))) : s(s(s(s(s(s(0)))))) : s(s(s(s(s(s(s( 0))))))) : s(s(s(s(s(s(s(s(0)))))))) : s(s(s(s(s(s(s(s(s( 0))))))))) : s(s(s(s(s(s(s(s(s(s(0)))))))))) : s(s(s(s(s(s(s( s(s(s(s(0))))))))))) : s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) : [] ) red postorder( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s(0)))))))))), s(s(s(s(s(s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s(s(0))))))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), s(s(s(s(0))))), s(s(0)))) . ***( reduce in NAT-SEARCH-TREE : postorder(insert(insert(insert( insert(insert(insert(insert(insert(insert(insert(insert( insert(insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s(s(s( 0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s(s(s( s(s(s(s(s(s(s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s( 0)))))))))), s(s(s(s(s(s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s( s(0))))))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), s(s(s(s( 0))))), s(s(0)))) . rewrites: 1126 in -10ms cpu (0ms real) (~ rewrites/second) result NeList: 0 : s(s(0)) : s(s(s(s(0)))) : s(s(s(0))) : s(0) : s(s(s(s(s(s(0)))))) : s(s(s(s(s(s(s(s(0)))))))) : s(s(s(s(s(s( s(s(s(s(0)))))))))) : s(s(s(s(s(s(s(s(s(0))))))))) : s(s(s(s( s(s(s(s(s(s(s(s(0)))))))))))) : s(s(s(s(s(s(s(s(s(s(s( 0))))))))))) : s(s(s(s(s(s(s(0))))))) : s(s(s(s(s(0))))) : [] ) red leaves( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s(0)))))))))), s(s(s(s(s(s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s(s(0))))))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), s(s(s(s(0))))), s(s(0)))) . ***( reduce in NAT-SEARCH-TREE : leaves(insert(insert(insert( insert(insert(insert(insert(insert(insert(insert(insert( insert(insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s(s(s( 0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s(s(s( s(s(s(s(s(s(s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s( 0)))))))))), s(s(s(s(s(s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s( s(0))))))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), s(s(s(s( 0))))), s(s(0)))) . rewrites: 1071 in -10ms cpu (0ms real) (~ rewrites/second) result NeList: 0 : s(s(0)) : s(s(s(s(0)))) : s(s(s(s(s(s(0)))))) : s(s(s(s(s(s(s(s(0)))))))) : s(s(s(s(s(s(s(s(s(s(0)))))))))) : s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) : [] ) red depth( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert( insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s(0)))))))))), s(s(s(s(s(s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s(s(0))))))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), s(s(s(s(0))))), s(s(0)))) . ***( reduce in NAT-SEARCH-TREE : depth(insert(insert(insert( insert(insert(insert(insert(insert(insert(insert(insert( insert(insert(empty-tree, s(s(s(s(s(0)))))), s(s(s(s(s(s(s( 0)))))))), s(0)), s(s(s(s(s(s(0))))))), s(s(s(0)))), s(s(s(s( s(s(s(s(s(s(s(0)))))))))))), 0), s(s(s(s(s(s(s(s(s( 0)))))))))), s(s(s(s(s(s(s(s(s(s(0))))))))))), s(s(s(s(s(s(s( s(0))))))))), s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), s(s(s(s( 0))))), s(s(0)))) . rewrites: 1182 in -10ms cpu (0ms real) (~ rewrites/second) result NzNat: s(s(s(s(s(0))))) )