in nat-list.maude fmod NAT-BIN-TREE is protecting NAT-LIST . sorts NeBinTree BinTree . subsort NeBinTree < BinTree . op empty-tree : -> BinTree . op _[_]_ : BinTree Nat BinTree -> NeBinTree . op left : NeBinTree -> BinTree . op right : NeBinTree -> BinTree . op root : NeBinTree -> Nat . op depth : BinTree -> Nat . op leaves : BinTree -> List . op preorder : BinTree -> List . op inorder : BinTree -> List . op postorder : BinTree -> List . vars N M : Nat . vars L R : BinTree . vars NEL NER : NeBinTree . eq left(L [N] R) = L . eq right(L [N] R) = R . eq root(L [N] R) = N . eq depth(empty-tree) = 0 . eq depth(L [N] R) = s(0) + max(depth(L), depth(R)) . eq leaves(empty-tree) = [] . eq leaves(empty-tree [N] empty-tree) = N : [] . eq leaves(NEL [N] R) = leaves(NEL) ++ leaves(R) . eq leaves(L [N] NER) = leaves(L) ++ leaves(NER) . eq preorder(empty-tree) = [] . eq preorder(L [N] R) = N : (preorder(L) ++ preorder(R)) . eq inorder(empty-tree) = [] . eq inorder(L [N] R) = inorder(L) ++ (N : inorder(R)) . eq postorder(empty-tree) = [] . eq postorder(L [N] R) = postorder(L) ++ (postorder(R) ++ (N : [])) . endfm *** 5 *** / \ *** / \ *** / \ *** 1 7 *** / \ / \ *** 0 3 6 11 *** / \ / \ *** 2 4 9 12 *** / \ *** 8 10 red preorder( ((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)))) . ***( reduce in NAT-BIN-TREE : preorder(((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)))) . rewrites: 52 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)))))))))))) : [] *** 5 : 1 : 0 : 3 : 2 : 4 : 7 : 6 : 11 : 9 : 8 : 10 : 12 ) red inorder( ((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)))) . ***( reduce in NAT-BIN-TREE : inorder(((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)))) . rewrites: 52 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)))))))))))) : [] *** 0 : 1 : 2 : 3 : 4 : 5 : 6 : 7 : 8 : 9 : 10 : 11 : 12 ) red postorder( ((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)))) . ***( reduce in NAT-BIN-TREE : postorder(((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)))) . rewrites: 83 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))))) : [] *** 0 : 2 : 4 : 3 : 1 : 6 : 8 : 10 : 9 : 12 : 11 : 7 : 5 ) red leaves( ((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)))) . ***( reduce in NAT-BIN-TREE : leaves(((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)))) . rewrites: 28 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)))))))))))) : [] *** 0 : 2 : 4 : 6 : 8 : 10 : 12 ) red depth( ((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)))) . ***( reduce in NAT-BIN-TREE : depth(((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)))) . rewrites: 139 in -10ms cpu (0ms real) (~ rewrites/second) result NzNat: s(s(s(s(s(0))))) *** 5 )