Rewrite Engines Competition
From FSL
[edit] (Unconditional) Term Rewrite Systems
[edit] Permutations
Operations:
z(0),suc(1),nil(0),cons(2), perm(1),insert0(2),insert1(2),map-cons(2),count(1)
- The result of count should be built-in naturals.
Specification:
append(P ; Ps,Ps') --> P ; append(Ps,Ps') append(nilP,Ps') --> Ps'
perm(z) --> nil ; nilP perm(suc(z)) --> (suc(z),nil) ; nilP perm(suc(N)) --> insert1(suc(N), perm(N))
insert1(N, (P ; Ps)) --> append(insert0(N,P) , insert1(N,Ps)) insert1(N,nilP) --> nilP
insert0(N, (M,P')) --> (N,M,P') ; map-cons(M, insert0(N,P')) insert0(N, nil) --> (N,nil) ; nilP
map-cons(M, (P ; Ps)) --> (M, P) ; map-cons(M, Ps) map-cons(M, nilP) --> nilP
count(nilP) --> 0 count(P ; Ps) --> s(count(Ps))
[edit] Factorial
Operations (assume numbers (0, s, *) are already specified or built-in ):
fact(1)
Specification:
fact(0) --> s(0) fact(s(n)) --> s(n) * fact(n)
[edit] Fibbonaci
Operations (assume numbers (0, s, +) are already specified or built-in ):
fibb(1)
Specification:
fibb(0) --> s(0) fibb(1) --> s(0) fibb(s(s(n))) --> fibb(s(n)) + fibb(n)
[edit] Merge-sort
Operations (assume integers with comaration predicates are specified of built-in):
nil,pair(2),cons(2),split(1),merge(2),mergesort(1)
Specification:
merge(nil,L) --> L merge(cons(x,Lx),cons(y,Ly)) --> cons(x,merge(Lx,cons(y,Ly))) if x < y merge(cons(x,Lx),cons(y,Ly)) --> cons(y,merge(cons(x,Lx),Ly)) if x >= y split(cons(x,cons(y,L))) --> pair(cons(x,Lx),cons(y,Ly)) if split(L) --> pair(Lx,Ly) split(nil) --> pair(nil,nil) split(cons(x,nil)) --> pair(cons(x,nil),nil) mergesort(nil) --> nil mergesort(cons(x,nil)) --> cons(x,nil) mergesort(cons(x,cons(y,L))) --> merge(mergesort(cons(x,Lx)),mergesort(cons(y,Ly))) if split(L) --> pair(Lx,Ly)
[edit] Garbage collection test
Operations:
0,1,m,n,f(5) c(2) : S S S S S -> S .
Specification:
1 --> s(0) m --> s(s(s(s(0)))) n --> s(s(s(0))) p --> s(s(s(s(s(0))))) c(0,Y) --> Y c(s(X),Y) --> s(c(X,Y)) f(X,Y,s(Z),T,U) --> f(X,Y,Z,c(T,T),U) f(X,s(Y),0,T,U) --> f(X,Y,p,T,T) f(s(X),0,0,T,U) --> f(X,n,p,1,0) f(0,0,0,T,U) --> T
Test: try to reduce a term of the form (definitions for m,n and p may be change to get relevant results
f(m,n,p,0,1) .
[edit] Rewriting modulo equations
[edit] (A) Permutations
Operations:
z(0),suc(1),nil(0),cons(2), perm(1),insert0(2),insert1(2),map-cons(2),count(1)
- Result of count should be built-in naturals
Specification:
append(P ; Ps,Ps') --> P ; append(Ps,Ps') append(nilP,Ps') --> Ps'
perm(z) --> nil ; nilP perm(suc(z)) --> (suc(z),nil) ; nilP perm(suc(N)) --> insert1(suc(N), perm(N))
insert1(N, (P ; Ps)) --> append(insert0(N,P) , insert1(N,Ps)) insert1(N,nilP) --> nilP
insert0(N, (M,P')) --> (N,M,P') ; map-cons(M, insert0(N,P')) insert0(N, nil) --> (N,nil) ; nilP
map-cons(M, (P ; Ps)) --> (M, P) ; map-cons(M, Ps) map-cons(M, nilP) --> nilP
count(nilP) --> 0 count(P ; Ps) --> s(count(Ps))
[edit] (AU) List Length
Operations (assumes built in natural numbers with 0 and successor s):
elt(1),cons(2),nil(0), length(1)
Specification: cons is associative with identity nil and
length(nil) --> 0 length(cons(elt(X),L)) --> s(length(L))
[edit] (AC) Satisfiability checker
Operations:
true(0),false(0),not(1), and(2), xor(2), or(2), implies(2)
Specification: and, or and xor are associative and commutative and
and(true,A) --> A and(false,A) -->false and(A,A) --> A xor(false,A) --> A xor(A,A) --> false and(A,xor(B,C)) --> xor(and(A,B),and(A,C)) not(A) --> xor(A,true) or(A,B) --> xor(xor(and(A,B),A),B) implies(A,B) --> not(xor(A,and(A,B)))
[edit] Conditional Term Rewrite Systems
[edit] Bubble-sort
Operations (assume built in integers with an less than (<) operator on them):
cons(2)
Specification:
cons(x,cons(y,L)) --> cons(y,cons(x,L)) if y < x
[edit] Odd/Even
Operations:
true,false,0,s(1),odd(1),even(1)
Specification:
odd(0) --> false even(0) --> true odd(s(x)) --> true if even(x) --> true even(s(x)) --> true if odd(x) --> true odd(s(x)) --> false if even(x) --> false even(s(x)) --> false if odd(x) --> false
[edit] Quick-sort
Operations (assuming built in integers with comparation predicates on them):
pair(2), cons(2), split(2), qsort(1)
Specification:
split(x,cons(y,L)) --> pair(LTx,cons(y,GTx)) if x < y and split(x,L) --> pair(LTx,GTx) split(x,cons(y,L)) --> pair(cons(y,LTx),GTx) if x >= y and split(x,L) --> pair(LTx,GTx) split(x,nil) --> pair(nil,nil) qsort(nil) = nil qsort(cons(x,L)) = append(qsort(LTx), cons(x,qsort(GTx)) if split(x,L) --> pair(LTx,GTx)
[edit] Marchiori
Operations:
a,b,c,d,e,k,l,m,A,B,f(1),h(2),g(3)
Specification:
a --> c a --> d b --> c b --> d c --> e c --> l d --> m k --> l k --> m A --> h(f(a),f(b)) g(d,x,x) --> B h(x,x) --> g(x,x,f(k)) f(x) --> x if x --> e B --> A
Test:
- does A rewrites to B (implying non-termination)?
[edit] Confluence
Operations:
0,f(1),g(1)
Specification:
f(g(x)) --> x if x --> 0 g(g(x)) --> g(x)
Test:
- Get all normal forms of f(g(g(0)))
[edit] Soundness of parallel engines
Operations:
0,f(1),g(1)
Specification:
f(g(x)) --> x if x --> s(0) g(s(x)) --> g(x)
Test:
- normal form for f(g(s(0)))
[edit] Search in conditions?
Operations:
true,false,a,not(1)
Specification (order matters):
a --> true a --> false not(x) --> true if x --> false
Test:
- does not(a) rewrites to true?
[edit] Termination, reachability?
Operations:
a,b,c
Specification (order matters):
a --> c if a --> b a --> b b --> c
Test:
- get a normal form for a
- test whether a rewrites to b?
[edit] ASF/SDF Benchmark
- We are grateful to professor Mark van der Brand for providing us this benchmark.
[edit] Informal specification
- In the sequel, identifiers starting with capital letters denote variables. All other denote operations. Also, this benchmark assumes the rewrite engine supports a default strategy to handle otherwise untreated cases.
[edit] Boolean equations
or(true, Bool) --> true or(false, Bool) --> Bool
and(true, Bool) --> Bool and(false, Bool) --> false
not ( false ) --> true not ( true ) --> false
[edit] Normal operations on naturals
plus(X,z) --> X plus(X,s(Y)) --> s(plus(X,Y))
mult(X,z) --> z mult(X,s(Y)) --> plus(mult(X,Y),X)
exp(X,z) --> s(z) exp(X,s(Y)) --> mult(X,exp(X,Y))
equal(X, X) --> true [default] equal(X, Y) --> false
less(z, X) --> true less(s(X),s(Y)) --> less(X,Y) [default] less(X,Y) --> false
[edit] We are working modulo 17
succ17(s(s(s(s(s(s(s(s(s(s(s(s(
s(s(s(s(z))))))))))))))))) --> z
[default] succ17(X) --> s(X)
pred17(s(X)) --> X
pred17(z) --> s(s(s(s(s(s(s(s(s(s(s(s(
s(s(s(s(z))))))))))))))))
[edit] Operations on naturals modulo 17
plus17(X,z) --> X plus17(X,s(Y)) --> succ17(plus17(X,Y))
mult17(X,z) --> z mult17(X,s(Y)) --> plus17(X,mult17(X,Y))
[mod-7] exp17(X,z) --> succ17(z) [mod-8] exp17(X,s(Y)) --> mult17(X,exp17(X,Y))
[edit] Complete evaluation of expressions
eval(exz) --> z eval(exs(Xs)) --> s(eval(Xs)) eval(explus(Xs,Ys)) --> plus(eval(Xs), eval(Ys)) eval(exmult(Xs,Ys)) --> mult(eval(Xs), eval(Ys)) eval(exexp(Xs,Ys)) --> exp(eval(Xs), eval(Ys))
[edit] Fast evaluation modulo 17
eval17(exz) --> z eval17(exs(Xs)) --> succ17(eval17(Xs)) eval17(explus(Xs,Ys)) --> plus17(eval17(Xs),eval17(Ys)) eval17(exmult(Xs,Ys)) --> mult17(eval17(Xs),eval17(Ys)) eval17(exexp(Xs,Ys)) --> exp17(eval17(Xs),eval(Ys))
[edit] Some symbolic natural constants
one --> exs(exz) two --> exs(one) three --> exs(two) four --> exs(three) five --> exs(four) six --> exs(five) seven --> exs(six) eight --> exs(seven) nine --> exs(eight) ten --> exs(nine) eleven --> exs(ten) twelve --> exs(eleven) thirteen --> exs(twelve) fourteen --> exs(thirteen) fifteen --> exs(fourteen) sixteen --> exs(fifteen) seventeen --> exs(sixteen) eighteen --> exs(seventeen) nineteen --> exs(eighteen) twenty --> exs(nineteen) twentyone --> exs(twenty) twentytwo --> exs(twentyone) twentythree --> exs(twentytwo) twentyfour --> exs(twentythree) twentyfive --> exs(twentyfour) twentysix --> exs(twentyfive) twentyseven --> exs(twentysix) twentyeight --> exs(twentyseven) twentynine --> exs(twentyeight) thirty --> exs(twentynine) thirtyone --> exs(thirty) thirtytwo --> exs(thirtyone) thirtythree --> exs(thirtytwo) thirtyfour --> exs(thirtythree) thirtyfive --> exs(thirtyfour)
[edit] Translation from naturals to symbolic naturals
nat2sym(z) --> exz nat2sym(s(X)) --> exs(nat2sym(X))
[edit] Some natural constants
0 --> z 1 --> s(0) 2 --> s(1) 3 --> s(2) 4 --> s(3) 5 --> s(4) 6 --> s(5) 7 --> s(6) 8 --> s(7) 9 --> s(8) 10 --> s(9) 11 --> s(10) 12 --> s(11) 13 --> s(12) 14 --> s(13) 15 --> s(14) 16 --> s(15) 17 --> s(16)
[edit] Symbolic evaluation of expressions modulo 17
evalsym17(exz) --> z evalsym17(exs(Xs)) --> succ17(evalsym17(Xs))
evalsym17(explus(Xs,Ys)) --> plus17(evalsym17(Xs),evalsym17(Ys))
evalsym17(exmult(Xs,exz)) --> z
evalsym17(exmult(Xs,exs(Ys))) -->
evalsym17(explus(exmult(Xs,Ys),Xs))
evalsym17(exmult(Xs,explus(Ys,Zs))) -->
evalsym17(explus(exmult(Xs,Ys),exmult(Xs,Zs)))
evalsym17(exmult(Xs,exmult(Ys,Zs))) -->
evalsym17(exmult(exmult(Xs,Ys),Zs))
evalsym17(exmult(Xs,exexp(Ys,Zs))) -->
evalsym17(exmult(Xs,dec(exexp(Ys,Zs))))
dec(exexp(Xs,exz)) --> exs(exz)
dec(exexp(Xs,exs(Ys))) --> exmult(exexp(Xs,Ys),Xs)
dec(exexp(Xs,explus(Ys,Zs))) -->
exmult(exexp(Xs,Ys),exexp(Xs,Zs))
dec(exexp(Xs,exmult(Ys,Zs))) -->
dec(exexp(exexp(Xs,Ys),Zs))
dec(exexp(Xs,exexp(Ys,Zs))) -->
dec(exexp(Xs, dec(exexp(Ys,Zs))))
evalsym17(exexp(Xs,exz)) --> succ17(z)
evalsym17(exexp(Xs,exs(Ys))) -->
evalsym17(exmult(exexp(Xs,Ys),Xs))
evalsym17(exexp(Xs,explus(Ys,Zs))) -->
evalsym17(exmult(exexp(Xs,Ys),exexp(Xs,Zs)))
evalsym17(exexp(Xs,exmult(Ys,Zs))) -->
evalsym17(exexp(exexp(Xs,Ys),Zs))
evalsym17(exexp(Xs,exexp(Ys,Zs))) -->
evalsym17(exexp(Xs,dec(exexp(Ys,Zs))))
[edit] Symbolic evaluation after expansion
evalexp17(Xs) --> eval17(expand(Xs))
expand(exz) --> exz expand(exs(Xs)) --> explus(exs(exz),expand(Xs))
expand(explus(Xs2,Ys2)) --> explus(expand(Xs2),expand(Ys2))
expand(exmult(Xs,exz)) --> exz
expand(exmult(Xs,exs(exz))) --> expand(Xs)
expand(exmult(Xs,explus(Ys,Zs))) -->
expand(explus(exmult(Xs,Ys),exmult(Xs,Zs)))
[default] expand(exmult(Xs1,Ys1)) -->
expand(exmult(Xs1,expand(Ys1)))
expand(exexp(Xs,exz)) --> exs(exz)
expand(exexp(Xs,exs(exz))) --> expand(Xs)
expand(exexp(Xs,explus(Ys,Zs))) -->
expand(exmult(exexp(Xs,Ys),exexp(Xs,Zs)))
[default] expand(exexp(Xs,Ys)) --> expand(exexp(Xs, expand(Ys)))
[edit] Tree benchmark
getval(leaf(Val)) --> Val getval(node(Val,Max,Left,Right)) --> Val
getmax(leaf(Val)) --> Val getmax(node(Val,Max,Left,Right)) --> Max
buildtree(z, Val) --> leaf(Val)
buildtree(s(X), Y) --> node(Val, Max, Left, Right) if
Left <-- buildtree(X, Y),
Max' <-- getmax(Left),
Right <-- buildtree(X, succ17(Max')),
Val' <-- getval(Left),
Val <-- getval(Right),
Val <-- plus17(Val', Val),
Max <-- getmax(Right)
calctree17(X) --> mult17(I,J) if
I <-- exp17(s(s(z)), pred17(X)),
J <-- pred17(exp17(s(s(z)),X))
[edit] Benchmark equations
bench-evalsym17(Xs) --> equal(eval17(Zs),evalsym17(Zs)) if
Zs <-- exexp(two,Xs)
bench-evalexp17(Xs) --> equal(eval17(Zs),evalexp17(Zs)) if
Zs <-- exexp(two,Xs)
bench-evaltree17(Xs) --> equal(calctree17(X),
getval(buildtree(X, z))) if X <-- eval(Xs)
[edit] Particular rewrite engines specifications
[edit] ASF/SDF Sources
- SDF source
module Benchmark
imports Layout
exports sorts Nat SNat Bool Tree
context-free syntax
"true" -> Bool
"false" -> Bool
"or" "(" Bool "," Bool ")" -> Bool
"and" "(" Bool "," Bool ")" -> Bool
"not" "(" Bool ")" -> Bool
"z" -> Nat
"s" "(" Nat ")" -> Nat
"equal" "(" Nat "," Nat ")" -> Bool
"less" "(" Nat "," Nat ")" -> Bool
"plus" "(" Nat "," Nat ")" -> Nat
"mult" "(" Nat "," Nat ")" -> Nat
"exp" "(" Nat "," Nat ")" -> Nat
"succ17" "(" Nat ")" -> Nat
"pred17" "(" Nat ")" -> Nat
"plus17" "(" Nat "," Nat ")" -> Nat
"mult17" "(" Nat "," Nat ")" -> Nat
"exp17" "(" Nat "," Nat ")" -> Nat
"exz" -> SNat %% The constant 0
"exs" "(" SNat ")" -> SNat %% successor
"explus" "(" SNat "," SNat ")" -> SNat
"exmult" "(" SNat "," SNat ")" -> SNat
"exexp" "(" SNat "," SNat ")" -> SNat
"leaf" "(" Nat ")" -> Tree
"node" "(" Nat "," Nat "," Tree "," Tree ")" -> Tree
"buildtree" "(" Nat "," Nat ")" -> Tree
"calctree17" "(" Nat ")" -> Nat
"getmax" "(" Tree ")" -> Nat
"getval" "(" Tree ")" -> Nat
%% Several eval functions
"eval" "(" SNat ")" -> Nat
"eval17" "(" SNat ")" -> Nat
"evalsym17" "(" SNat ")" -> Nat
"evalexp17" "(" SNat ")" -> Nat
%% The benchmarks
"bench-evalsym17" "(" SNat ")" -> Bool
"bench-evalexp17" "(" SNat ")" -> Bool
"bench-evaltree17" "(" SNat ")" -> Bool
%% Some constants "zero" -> SNat "one" -> SNat "two" -> SNat "three" -> SNat "four" -> SNat "five" -> SNat "six" -> SNat "seven" -> SNat "eight" -> SNat "nine" -> SNat "ten" -> SNat "eleven" -> SNat "twelve" -> SNat "thirteen" -> SNat "fourteen" -> SNat "fifteen" -> SNat "sixteen" -> SNat "seventeen" -> SNat "eighteen" -> SNat "nineteen" -> SNat "twenty" -> SNat "twentyone" -> SNat "twentytwo" -> SNat "twentythree" -> SNat "twentyfour" -> SNat "twentyfive" -> SNat "twentysix" -> SNat "twentyseven" -> SNat "twentyeight" -> SNat "twentynine" -> SNat "thirty" -> SNat "thirtyone" -> SNat "thirtytwo" -> SNat "thirtythree" -> SNat "thirtyfour" -> SNat "thirtyfive" -> SNat
%% Test constants "0" -> Nat "1" -> Nat "2" -> Nat "3" -> Nat "4" -> Nat "5" -> Nat "6" -> Nat "7" -> Nat "8" -> Nat "9" -> Nat "10" -> Nat "11" -> Nat "12" -> Nat "13" -> Nat "14" -> Nat "15" -> Nat "16" -> Nat "17" -> Nat
variables "Bool"[0-9\']* -> Bool "X"[0-9\']* -> Nat "Y"[0-9\']* -> Nat "Z"[0-9\']* -> Nat "Xs"[0-9\']* -> SNat "Ys"[0-9\']* -> SNat "Zs"[0-9\']* -> SNat "I"[0-9\']* -> Nat "J"[0-9\']* -> Nat "K"[0-9\']* -> Nat "L"[0-9\']* -> Nat
hiddens
sorts NatPair
context-free syntax
"dec" "(" SNat ")" -> SNat
"expand" "(" SNat ")" -> SNat
"exone" -> SNat
"nat2sym" "(" Nat ")" -> SNat
variables "P"[0-9\']* -> NatPair "P*"[0-9\']* -> NatPair* "Left" -> Tree "Right" -> Tree "Max"[\']* -> Nat "Val"[\']* -> Nat
- ASF source
%% Boolean equations [B1] or(true, Bool) = true [B2] or(false, Bool) = Bool
[B3] and(true, Bool) = Bool [B4] and(false, Bool) = false
[B5] not ( false ) = true [B6] not ( true ) = false
%% Normal operations on naturals [nat-1] plus(X,z) = X [nat-2] plus(X,s(Y)) = s(plus(X,Y))
[nat-3] mult(X,z) = z [nat-4] mult(X,s(Y)) = plus(mult(X,Y),X)
[nat-5] exp(X,z) = s(z) [nat-6] exp(X,s(Y)) = mult(X,exp(X,Y))
[nat-7] equal(X, X) = true [default-8] equal(X, Y) = false
[nat-9] less(z, X) = true [nat-10] less(s(X),s(Y)) = less(X,Y) [default-9] less(X,Y) = false
%% We are working modulo 17
[mod-1] succ17(s(s(s(s(s(s(s(s(s(s(s(s(
s(s(s(s(z))))))))))))))))) = z
[default-mod-2] succ17(X) = s(X)
[pred-1] pred17(s(X)) = X
[pred-2] pred17(z) = s(s(s(s(s(s(s(s(s(s(s(s(
s(s(s(s(z))))))))))))))))
%% Operations on naturals modulo 17 [mod-3] plus17(X,z) = X [mod-4] plus17(X,s(Y)) = succ17(plus17(X,Y))
[mod-5] mult17(X,z) = z [mod-6] mult17(X,s(Y)) = plus17(X,mult17(X,Y))
[mod-7] exp17(X,z) = succ17(z) [mod-8] exp17(X,s(Y)) = mult17(X,exp17(X,Y))
%% Complete evaluation of expressions [eval-1] eval(exz) = z [eval-2] eval(exs(Xs)) = s(eval(Xs)) [eval-3] eval(explus(Xs,Ys)) = plus(eval(Xs), eval(Ys)) [eval-4] eval(exmult(Xs,Ys)) = mult(eval(Xs), eval(Ys)) [eval-5] eval(exexp(Xs,Ys)) = exp(eval(Xs), eval(Ys))
%% Fast evaluation modulo 17 [mod17-1] eval17(exz) = z [mod17-2] eval17(exs(Xs)) = succ17(eval17(Xs)) [mod17-3] eval17(explus(Xs,Ys)) = plus17(eval17(Xs),eval17(Ys)) [mod17-4] eval17(exmult(Xs,Ys)) = mult17(eval17(Xs),eval17(Ys)) [mod17-5] eval17(exexp(Xs,Ys)) = exp17(eval17(Xs),eval(Ys))
%% Some symbolic natural constants [const-1] one = exs(exz) [const-2] two = exs(one) [const-3] three = exs(two) [const-4] four = exs(three) [const-5] five = exs(four) [const-6] six = exs(five) [const-7] seven = exs(six) [const-8] eight = exs(seven) [const-9] nine = exs(eight) [const-10] ten = exs(nine) [const-11] eleven = exs(ten) [const-12] twelve = exs(eleven) [const-13] thirteen = exs(twelve) [const-14] fourteen = exs(thirteen) [const-15] fifteen = exs(fourteen) [const-16] sixteen = exs(fifteen) [const-17] seventeen = exs(sixteen) [const-18] eighteen = exs(seventeen) [const-19] nineteen = exs(eighteen) [const-20] twenty = exs(nineteen) [const-21] twentyone = exs(twenty) [const-22] twentytwo = exs(twentyone) [const-23] twentythree = exs(twentytwo) [const-24] twentyfour = exs(twentythree) [const-25] twentyfive = exs(twentyfour) [const-26] twentysix = exs(twentyfive) [const-27] twentyseven = exs(twentysix) [const-28] twentyeight = exs(twentyseven) [const-29] twentynine = exs(twentyeight) [const-30] thirty = exs(twentynine) [const-31] thirtyone = exs(thirty) [const-32] thirtytwo = exs(thirtyone) [const-33] thirtythree = exs(thirtytwo) [const-34] thirtyfour = exs(thirtythree) [const-35] thirtyfive = exs(thirtyfour)
%% Translation from naturals to symbolic naturals [n2s-0] nat2sym(z) = exz [n2s-1] nat2sym(s(X)) = exs(nat2sym(X))
%% Some natural constants [n-0] 0 = z [n-1] 1 = s(0) [n-2] 2 = s(1) [n-3] 3 = s(2) [n-4] 4 = s(3) [n-5] 5 = s(4) [n-6] 6 = s(5) [n-7] 7 = s(6) [n-8] 8 = s(7) [n-9] 9 = s(8) [n-10] 10 = s(9) [n-11] 11 = s(10) [n-12] 12 = s(11) [n-13] 13 = s(12) [n-14] 14 = s(13) [n-15] 15 = s(14) [n-16] 16 = s(15) [n-17] 17 = s(16)
%% Symbolic evaluation of expressions modulo 17 [evalsym-1] evalsym17(exz) = z [evalsym-2] evalsym17(exs(Xs)) = succ17(evalsym17(Xs))
[evalsym-3] evalsym17(explus(Xs,Ys)) = plus17(evalsym17(Xs),evalsym17(Ys))
[evalsym-4] evalsym17(exmult(Xs,exz)) = z
[evalsym-5] evalsym17(exmult(Xs,exs(Ys))) =
evalsym17(explus(exmult(Xs,Ys),Xs))
[evalsym-6] evalsym17(exmult(Xs,explus(Ys,Zs))) =
evalsym17(explus(exmult(Xs,Ys),exmult(Xs,Zs)))
[evalsym-7] evalsym17(exmult(Xs,exmult(Ys,Zs))) =
evalsym17(exmult(exmult(Xs,Ys),Zs))
[evalsym-8] evalsym17(exmult(Xs,exexp(Ys,Zs))) =
evalsym17(exmult(Xs,dec(exexp(Ys,Zs))))
[evalsym-9] dec(exexp(Xs,exz)) = exs(exz)
[evalsym-10] dec(exexp(Xs,exs(Ys))) = exmult(exexp(Xs,Ys),Xs)
[evalsym-11] dec(exexp(Xs,explus(Ys,Zs))) =
exmult(exexp(Xs,Ys),exexp(Xs,Zs))
[evalsym-11] dec(exexp(Xs,exmult(Ys,Zs))) =
dec(exexp(exexp(Xs,Ys),Zs))
[evalsym-12] dec(exexp(Xs,exexp(Ys,Zs))) =
dec(exexp(Xs, dec(exexp(Ys,Zs))))
[evalsym-13] evalsym17(exexp(Xs,exz)) = succ17(z)
[evalsym-14] evalsym17(exexp(Xs,exs(Ys))) =
evalsym17(exmult(exexp(Xs,Ys),Xs))
[evalsym-15] evalsym17(exexp(Xs,explus(Ys,Zs))) =
evalsym17(exmult(exexp(Xs,Ys),exexp(Xs,Zs)))
[evalsym-16] evalsym17(exexp(Xs,exmult(Ys,Zs))) =
evalsym17(exexp(exexp(Xs,Ys),Zs))
[evalsym-17] evalsym17(exexp(Xs,exexp(Ys,Zs))) =
evalsym17(exexp(Xs,dec(exexp(Ys,Zs))))
%% Symbolic evaluation after expansion [evalexp-1] evalexp17(Xs) = eval17(expand(Xs))
[expand-1] expand(exz) = exz [expand-3] expand(exs(Xs)) = explus(exs(exz),expand(Xs))
[expand-6] expand(explus(Xs2,Ys2)) = explus(expand(Xs2),expand(Ys2))
[expand-7] expand(exmult(Xs,exz)) = exz
[expand-8] expand(exmult(Xs,exs(exz))) = expand(Xs)
[expand-9] expand(exmult(Xs,explus(Ys,Zs))) =
expand(explus(exmult(Xs,Ys),exmult(Xs,Zs)))
[default-expand-9]
expand(exmult(Xs1,Ys1)) = expand(exmult(Xs1,expand(Ys1)))
[expand-10] expand(exexp(Xs,exz)) = exs(exz)
[expand-11] expand(exexp(Xs,exs(exz))) = expand(Xs)
[expand-12] expand(exexp(Xs,explus(Ys,Zs))) =
expand(exmult(exexp(Xs,Ys),exexp(Xs,Zs)))
[default-expand-13]
expand(exexp(Xs,Ys)) = expand(exexp(Xs, expand(Ys)))
%% Tree benchmark [getval-1] getval(leaf(Val)) = Val [getval-2] getval(node(Val,Max,Left,Right)) = Val
[getmax-1] getmax(leaf(Val)) = Val [getmax-2] getmax(node(Val,Max,Left,Right)) = Max
[buildtree-1] buildtree(z, Val) = leaf(Val)
[buildtree-2] Left = buildtree(X, Y),
Max' = getmax(Left),
Right = buildtree(X, succ17(Max')),
Val' = getval(Left),
Val = getval(Right),
Val = plus17(Val', Val),
Max = getmax(Right)
================================================
buildtree(s(X), Y) = node(Val, Max, Left, Right)
[calctree-1] I = exp17(s(s(z)), pred17(X)), J = pred17(exp17(s(s(z)),X)) ============================ calctree17(X) = mult17(I,J)
%% Benchmark equations
[bench-1] Zs = exexp(two,Xs)
=====================================================
bench-evalsym17(Xs) = equal(eval17(Zs),evalsym17(Zs))
[bench-2] Zs = exexp(two,Xs)
=====================================================
bench-evalexp17(Xs) = equal(eval17(Zs),evalexp17(Zs))
[bench-3] X = eval(Xs)
=====================================================
bench-evaltree17(Xs) = equal(calctree17(X),
getval(buildtree(X, z)))
- The Layout
%%%% %%%% $Id: Layout.sdf2,v 1.1 2000/04/26 14:51:29 jurgenv Exp $ %%%% %%%% This file is part of the specification %%%% "Box: Language, Laws and Formatters" %%%% %%%% Copyright (c) Mark van den Brand & Eelco Visser, 1995 %%%% %%%% Programming Research Group, University of Amsterdam %%%% Kruislaan 403, 1098 SJ Amsterdam, The Netherlands. %%%% mail:markvdb@fwi.uva.nl http://adam.fwi.uva.nl/~markvdb/ %%%% mail:visser@fwi.uva.nl http://adam.fwi.uva.nl/~visser/ %%%%
%% \module{Layout}
module Layout
exports
lexical syntax
[\ \t\n] -> LAYOUT
"%%" ~[\n]* "\n" -> LAYOUT
"%" ~[\%\n]+ "%" -> LAYOUT
context-free restrictions
LAYOUT? -/- [\ \t\n\%]
[edit] Elan sources
- ELN file
module benchmark
import global eq[Nat]; end
sort Bool Nat SNat Tree NatPair; end
operators global
'true' : Bool;
'false' : Bool;
'or' '(' @ ',' @ ')' : (Bool Bool) Bool;
'and' '(' @ ',' @ ')' : (Bool Bool) Bool;
'not' '(' @ ')' : (Bool) Bool;
'zero' : Nat;
's' '(' @ ')' : (Nat) Nat;
'equal' '(' @ ',' @ ')' : (Nat Nat) Bool;
'less' '(' @ ',' @ ')' : (Nat Nat) Bool;
'plus' '(' @ ',' @ ')' : (Nat Nat) Nat;
'mult' '(' @ ',' @ ')' : (Nat Nat) Nat;
'exp' '(' @ ',' @ ')' : (Nat Nat) Nat;
'succ17' '(' @ ')' : (Nat) Nat;
'pred17' '(' @ ')' : (Nat) Nat;
'plus17' '(' @ ',' @ ')' : (Nat Nat) Nat;
'mult17' '(' @ ',' @ ')' : (Nat Nat) Nat;
'exp17' '(' @ ',' @ ')' : (Nat Nat) Nat;
'exz' : SNat;
'exs' '(' @ ')' : (SNat) SNat;
'explus' '(' @ ',' @ ')' : (SNat SNat) SNat;
'exmult' '(' @ ',' @ ')' : (SNat SNat) SNat;
'exexp' '(' @ ',' @ ')' : (SNat SNat) SNat;
'leaf' '(' @ ')' : (Nat) Tree;
'node' '(' @ ',' @ ',' @ ',' @ ')' : (Nat Nat Tree Tree) Tree;
'buildtree' '(' @ ',' @ ')' : (Nat Nat) Tree;
'calctree17' '(' @ ')' : (Nat) Nat;
'getmax' '(' @ ')' : (Tree) Nat;
'getval' '(' @ ')' : (Tree) Nat;
'eval' '(' @ ')' : (SNat) Nat;
'eval17' '(' @ ')' : (SNat) Nat;
'evalsym17' '(' @ ')' : (SNat) Nat;
'evalexp17' '(' @ ')' : (SNat) Nat;
'benchevalsym17' '(' @ ')' : (SNat) Bool;
'benchevalexp17' '(' @ ')' : (SNat) Bool;
'benchevaltree17' '(' @ ')' : (SNat) Bool;
'one' : SNat; 'two' : SNat; 'three' : SNat; 'four' : SNat; 'five' : SNat; 'six' : SNat; 'seven' : SNat; 'eight' : SNat; 'nine' : SNat; 'ten' : SNat; 'eleven' : SNat; 'twelve' : SNat; 'thirteen' : SNat; 'fourteen' : SNat; 'fifteen' : SNat; 'sixteen' : SNat; 'seventeen' : SNat; 'eighteen' : SNat; 'nineteen' : SNat; 'twenty' : SNat; 'twentyone' : SNat; 'twentytwo' : SNat; 'twentythree' : SNat; 'twentyfour' : SNat; 'twentyfive' : SNat; 'twentysix' : SNat; 'twentyseven' : SNat; 'twentyeight' : SNat; 'twentynine' : SNat; 'thirty' : SNat; 'thirtyone' : SNat; 'thirtytwo' : SNat; 'thirtythree' : SNat; 'thirtyfour' : SNat; 'thirtyfive' : SNat;
'0' : Nat; '1' : Nat; '2' : Nat; '3' : Nat; '4' : Nat; '5' : Nat; '6' : Nat; '7' : Nat; '8' : Nat; '9' : Nat; '10' : Nat; '11' : Nat; '12' : Nat; '13' : Nat; '14' : Nat; '15' : Nat; '16' : Nat; '17' : Nat;
'dec' '(' @ ')' : (SNat) SNat;
'expand' '(' @ ')' : (SNat) SNat;
'exone' : SNat;
'<' @ ',' @ '>' : (Nat Nat) NatPair;
'mod' '(' @ ',' @ ')' : (Nat Nat) Nat;
'mod' '(' @ ',' @ ',' @ ',' @ ')' : (Nat Nat Nat Nat) Nat;
'nat2spoon' '(' @ ',' @ ',' @ ')' : (Nat Nat Nat) Nat;
'nat2sym' '(' @ ')' : (Nat) SNat;
end
rules for Bool bool : Bool; X, x, y, x1, y1 : Nat; Xs, Ys, Zs : SNat; global [] or(true, bool) => true end [] or(false, bool) => bool end
[] and(true, bool) => bool end [] and(false, bool) => false end
[] not(false) => true end [] not(true) => false end
[] equal(x,x) => true end [] equal(x,y) => false end
[] less(zero, y) => true end [] less(s(x), s(y)) => less(x,y) end [] less(x, y) => false end
[] benchevalsym17(Xs) => equal(eval17(Zs),evalsym17(Zs))
where Zs := ()exexp(two,Xs)
end
[] benchevalexp17(Xs) => equal(eval17(Zs),evalexp17(Zs))
where Zs := ()exexp(two,Xs)
end
[] benchevaltree17(Xs) => equal(calctree17(X),getval(buildtree(X,zero)))
where X := ()eval(Xs)
end
end
rules for Nat i, j, x, y, val, max : Nat; xs, ys : SNat; Xs, Ys, Zs : SNat; left, right : Tree;
global [] plus(x,zero) => x end [] plus(x,s(y)) => s(plus(x,y)) end
[] mult(x,zero) => zero end [] mult(x,s(y)) => plus(mult(x,y),x) end
[] exp(x,zero) => s(zero) end [] exp(x,s(y)) => mult(x,exp(x,y)) end
[] succ17(s(s(s(s(s(s(s(s(s(s(s(s(
s(s(s(s(zero))))))))))))))))) => zero end
[] succ17(x) => s(x) end
[] pred17(s(x)) => x end
[] pred17(zero) => s(s(s(s(s(s(s(s(s(s(s(s(
s(s(s(s(zero)))))))))))))))) end
[] plus17(x,zero) => x end [] plus17(x,s(y)) => succ17(plus17(x,y)) end
[] mult17(x,zero) => zero end [] mult17(x,s(y)) => plus17(x,mult17(x,y)) end
[] exp17(x,zero) => succ17(zero) end [] exp17(x,s(y)) => mult17(x,exp17(x,y)) end
[] eval(exz) => zero end [] eval(exs(xs)) => s(eval(xs)) end [] eval(explus(xs,ys)) => plus(eval(xs), eval(ys)) end [] eval(exmult(xs,ys)) => mult(eval(xs), eval(ys)) end [] eval(exexp(xs,ys)) => exp(eval(xs), eval(ys)) end
[] eval17(exz) => zero end [] eval17(exs(xs)) => succ17(eval17(xs)) end [] eval17(explus(xs,ys)) => plus17(eval17(xs), eval17(ys)) end [] eval17(exmult(xs,ys)) => mult17(eval17(xs), eval17(ys)) end [] eval17(exexp(xs,ys)) => exp17(eval17(xs), eval(ys)) end
[] 0 => zero end [] 1 => s(0) end [] 2 => s(1) end [] 3 => s(2) end [] 4 => s(3) end [] 5 => s(4) end [] 6 => s(5) end [] 7 => s(6) end [] 8 => s(7) end [] 9 => s(8) end [] 10 => s(9) end [] 11 => s(10) end [] 12 => s(11) end [] 13 => s(12) end [] 14 => s(13) end [] 15 => s(14) end [] 16 => s(15) end [] 17 => s(16) end
[] evalsym17(exz) => zero end
[] evalsym17(exs(Xs)) => succ17(evalsym17(Xs)) end
[] evalsym17(explus(Xs,Ys)) => plus17(evalsym17(Xs),evalsym17(Ys)) end
[] evalsym17(exmult(Xs,exz)) => zero end
[] evalsym17(exmult(Xs,exs(Ys))) =>
evalsym17(explus(exmult(Xs,Ys),Xs)) end
[] evalsym17(exmult(Xs,explus(Ys,Zs))) =>
evalsym17(explus(exmult(Xs,Ys),exmult(Xs,Zs))) end
[] evalsym17(exmult(Xs,exmult(Ys,Zs))) =>
evalsym17(exmult(exmult(Xs,Ys),Zs)) end
[] evalsym17(exmult(Xs,exexp(Ys,Zs))) =>
evalsym17(exmult(Xs,dec(exexp(Ys,Zs)))) end
[] evalsym17(exexp(Xs,exz)) => succ17(zero) end
[] evalsym17(exexp(Xs,exs(Ys))) =>
evalsym17(exmult(exexp(Xs,Ys),Xs)) end
[] evalsym17(exexp(Xs,explus(Ys,Zs))) =>
evalsym17(exmult(exexp(Xs,Ys),exexp(Xs,Zs))) end
[] evalsym17(exexp(Xs,exmult(Ys,Zs))) =>
evalsym17(exexp(exexp(Xs,Ys),Zs)) end
[] evalsym17(exexp(Xs,exexp(Ys,Zs))) =>
evalsym17(exexp(Xs,dec(exexp(Ys,Zs)))) end
[] evalexp17(Xs) => eval17(expand(Xs)) end [] eval17(exone) => s(zero) end
[] getval(leaf(val)) => val end [] getval(node(val,max,left,right)) => val end
[] getmax(leaf(val)) => val end [] getmax(node(val,max,left,right)) => max end
[] calctree17(x) => mult17(i,j)
where i := ()exp17(s(s(zero)),pred17(x))
where j := ()pred17(exp17(s(s(zero)),x))
end
end
rules for SNat x : Nat; Xs, Ys, Zs : SNat;
global [] one => exs(exz) end [] two => exs(one) end [] three => exs(two) end [] four => exs(three) end [] five => exs(four) end [] six => exs(five) end [] seven => exs(six) end [] eight => exs(seven) end [] nine => exs(eight) end [] ten => exs(nine) end [] eleven => exs(ten) end [] twelve => exs(eleven) end [] thirteen => exs(twelve) end [] fourteen => exs(thirteen) end [] fifteen => exs(fourteen) end [] sixteen => exs(fifteen) end [] seventeen => exs(sixteen) end [] eighteen => exs(seventeen) end [] nineteen => exs(eighteen) end [] twenty => exs(nineteen) end [] twentyone => exs(twenty) end [] twentytwo => exs(twentyone) end [] twentythree => exs(twentytwo) end [] twentyfour => exs(twentythree) end [] twentyfive => exs(twentyfour) end [] twentysix => exs(twentyfive) end [] twentyseven => exs(twentysix) end [] twentyeight => exs(twentyseven) end [] twentynine => exs(twentyeight) end [] thirty => exs(twentynine) end [] thirtyone => exs(thirty) end [] thirtytwo => exs(thirtyone) end [] thirtythree => exs(thirtytwo) end [] thirtyfour => exs(thirtythree) end [] thirtyfive => exs(thirtyfour) end
[] nat2sym(zero) => exz end [] nat2sym(s(x)) => exs(nat2sym(x)) end
[] expand(exz) => exz end
[] expand(exone) => exone end
[] expand(exs(Xs)) => explus(exone,expand(Xs)) end
[] expand(explus(Xs,Ys)) => explus(expand(Xs),expand(Ys)) end
[] expand(exmult(Xs,exz)) => exz end
[] expand(exmult(Xs,exone)) => expand(Xs) end
[] expand(exmult(Xs,explus(Ys,Zs))) =>
expand(explus(exmult(Xs,Ys),exmult(Xs,Zs))) end
[] expand(exmult(Xs,Ys)) => expand(exmult(Xs,expand(Ys))) end
[] expand(exexp(Xs,exz)) => exone end
[] expand(exexp(Xs,exone)) => expand(Xs) end
[] expand(exexp(Xs,explus(Ys,Zs))) =>
expand(exmult(exexp(Xs,Ys),exexp(Xs,Zs))) end
[] expand(exexp(Xs,Ys)) => expand(exexp(Xs, expand(Ys))) end
end
rules for Tree x, y, val, val1, val2, max, max1 : Nat; left, right : Tree;
global
[] buildtree(zero, val) => leaf(val) end
[] buildtree(s(x), y) => node(val, max, left, right)
where left := ()buildtree(x, y)
where max1 := ()getmax(left)
where right := ()buildtree(x, succ17(max1))
where val1 := ()getval(left)
where val2 := ()getval(right)
where val := ()plus17(val1,val2)
where max := ()getmax(right)
end
end
end
- LGI file
LPL benchmark description query of sort Bool result of sort Bool import benchmark start with ()benchevaltree17(twentyseven) end
[edit] Maude sources
fmod BENCHMARK is sorts Boel Nat SNat Tree NatPair Boolean .
op true : -> Boolean . op false : -> Boolean . op or : Boolean Boolean -> Boolean . op and : Boolean Boolean -> Boolean . op neg : Boolean -> Boolean .
op zero : -> Nat . op s : Nat -> Nat . op equal : Nat Nat -> Boolean . op less : Nat Nat -> Boolean . op plus : Nat Nat -> Nat . op mult : Nat Nat -> Nat . op exp : Nat Nat -> Nat .
op succ17 : Nat -> Nat . op pred17 : Nat -> Nat . op plus17 : Nat Nat -> Nat . op mult17 : Nat Nat -> Nat . op exp17 : Nat Nat -> Nat .
op exz : -> SNat . op exs : SNat -> SNat . op explus : SNat SNat -> SNat . op exmult : SNat SNat -> SNat . op exexp : SNat SNat -> SNat .
op leaf : Nat -> Tree . op node : Nat Nat Tree Tree -> Tree . op buildtree : Nat Nat -> Tree . op calctree17 : Nat -> Nat . op getmax : Tree -> Nat . op getval : Tree -> Nat .
op eval : SNat -> Nat . op eval17 : SNat -> Nat . op evalsym17 : SNat -> Nat . op evalexp17 : SNat -> Nat .
op benchevalsym17 : SNat -> Boolean . op benchevalexp17 : SNat -> Boolean . op benchevaltree17 : SNat -> Boolean .
op one : -> SNat . op two : -> SNat . op three : -> SNat . op four : -> SNat . op five : -> SNat . op six : -> SNat . op seven : -> SNat . op eight : -> SNat . op nine : -> SNat . op ten : -> SNat . op eleven : -> SNat . op twelve : -> SNat . op thirteen : -> SNat . op fourteen : -> SNat . op fifteen : -> SNat . op sixteen : -> SNat . op seventeen : -> SNat . op eighteen : -> SNat . op nineteen : -> SNat . op twenty : -> SNat . op twentyone : -> SNat . op twentytwo : -> SNat . op twentythree : -> SNat . op twentyfour : -> SNat . op twentyfive : -> SNat . op twentysix : -> SNat . op twentyseven : -> SNat . op twentyeight : -> SNat . op twentynine : -> SNat . op thirty : -> SNat . op thirtyone : -> SNat . op thirtytwo : -> SNat . op thirtythree : -> SNat . op thirtyfour : -> SNat . op thirtyfive : -> SNat .
op 0 : -> Nat . op 1 : -> Nat . op 2 : -> Nat . op 3 : -> Nat . op 4 : -> Nat . op 5 : -> Nat . op 6 : -> Nat . op 7 : -> Nat . op 8 : -> Nat . op 9 : -> Nat . op 10 : -> Nat . op 11 : -> Nat . op 12 : -> Nat . op 13 : -> Nat . op 14 : -> Nat . op 15 : -> Nat . op 16 : -> Nat . op 17 : -> Nat .
op dec : SNat -> SNat . op expand : SNat -> SNat . op exone : -> SNat .
op < _ , _ > : Nat Nat -> NatPair . op mod : Nat Nat -> Nat . op mod : Nat Nat Nat Nat -> Nat . op nat2spoon : Nat Nat Nat -> Nat .
op nat2sym : Nat -> SNat .
*** some variables
var Boolean : Boolean . vars X Y Val Max : Nat . vars Xs Ys Zs : SNat . vars Left Right : Tree .
*** equations for boolean expressions eq or(true,Boolean) = true . eq or(false,Boolean) = Boolean .
eq and(true, Boolean) = Boolean . eq and(false, Boolean) = false .
eq neg(false) = true . eq neg(true) = false .
*** toplevel benchmarks
eq benchevalsym17(Xs) = equal(eval17(exexp(two,Xs)),evalsym17(exexp(two,Xs))) .
eq benchevalexp17(Xs) = equal(eval17(exexp(two,Xs)),evalexp17(exexp(two,Xs))) .
eq benchevaltree17(Xs) = equal(calctree17(eval(Xs)),getval(buildtree(eval(Xs),zero))) .
*** equations for naturals modulo 17 eq equal(X,X) = true . eq equal(X,Y) = false .
eq less(zero, Y) = true . eq less(s(X), s(Y)) = less(X,Y) . eq less(X, Y) = false .
eq plus(X,zero) = X . eq plus(X,s(Y)) = s(plus(X,Y)) .
eq mult(X,zero) = zero . eq mult(X,s(Y)) = plus(mult(X,Y),X) .
eq exp(X,zero) = s(zero) . eq exp(X,s(Y)) = mult(X,exp(X,Y)) .
eq succ17(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(zero))))))))))))))))) = zero . eq succ17(X) = s(X) .
eq pred17(s(X)) = X . eq pred17(zero) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(zero)))))))))))))))) .
eq plus17(X,zero) = X . eq plus17(X,s(Y)) = succ17(plus17(X,Y)) .
eq mult17(X,zero) = zero . eq mult17(X,s(Y)) = plus17(X,mult17(X,Y)) .
eq exp17(X,zero) = succ17(zero) . eq exp17(X,s(Y)) = mult17(X,exp17(X,Y)) .
eq eval(exz) = zero . eq eval(exs(Xs)) = s(eval(Xs)) . eq eval(explus(Xs,Ys)) = plus(eval(Xs), eval(Ys)) . eq eval(exmult(Xs,Ys)) = mult(eval(Xs), eval(Ys)) . eq eval(exexp(Xs,Ys)) = exp(eval(Xs), eval(Ys)) .
eq eval17(exz) = zero . eq eval17(exs(Xs)) = succ17(eval17(Xs)) . eq eval17(explus(Xs,Ys)) = plus17(eval17(Xs), eval17(Ys)) . eq eval17(exmult(Xs,Ys)) = mult17(eval17(Xs), eval17(Ys)) . eq eval17(exexp(Xs,Ys)) = exp17(eval17(Xs), eval(Ys)) .
eq 0 = zero . eq 1 = s(0) . eq 2 = s(1) . eq 3 = s(2) . eq 4 = s(3) . eq 5 = s(4) . eq 6 = s(5) . eq 7 = s(6) . eq 8 = s(7) . eq 9 = s(8) . eq 10 = s(9) . eq 11 = s(10) . eq 12 = s(11) . eq 13 = s(12) . eq 14 = s(13) . eq 15 = s(14) . eq 16 = s(15) . eq 17 = s(16) .
eq evalsym17(exz) = zero . eq evalsym17(exs(Xs)) = succ17(evalsym17(Xs)) . eq evalsym17(explus(Xs,Ys)) = plus17(evalsym17(Xs),evalsym17(Ys)) . eq evalsym17(exmult(Xs,exz)) = zero . eq evalsym17(exmult(Xs,exs(Ys))) = evalsym17(explus(exmult(Xs,Ys),Xs)) . eq evalsym17(exmult(Xs,explus(Ys,Zs))) = evalsym17(explus(exmult(Xs,Ys),exmult(Xs,Zs))) . eq evalsym17(exmult(Xs,exmult(Ys,Zs))) = evalsym17(exmult(exmult(Xs,Ys),Zs)) . eq evalsym17(exmult(Xs,exexp(Ys,Zs))) = evalsym17(exmult(Xs,dec(exexp(Ys,Zs)))) . eq evalsym17(exexp(Xs,exz)) = succ17(zero) . eq evalsym17(exexp(Xs,exs(Ys))) = evalsym17(exmult(exexp(Xs,Ys),Xs)) . eq evalsym17(exexp(Xs,explus(Ys,Zs))) = evalsym17(exmult(exexp(Xs,Ys),exexp(Xs,Zs))) . eq evalsym17(exexp(Xs,exmult(Ys,Zs))) = evalsym17(exexp(exexp(Xs,Ys),Zs)) . eq evalsym17(exexp(Xs,exexp(Ys,Zs))) = evalsym17(exexp(Xs,dec(exexp(Ys,Zs)))) .
eq evalexp17(Xs) = eval17(expand(Xs)) . eq eval17(exone) = s(zero) .
eq getval(leaf(Val)) = Val . eq getval(node(Val,Max,Left,Right)) = Val .
eq getmax(leaf(Val)) = Val . eq getmax(node(Val,Max,Left,Right)) = Max .
eq calctree17(X) = mult17(exp17(s(s(zero)),pred17(X)), pred17(exp17(s(s(zero)),X))).
*** equations for SNat
eq one = exs(exz) . eq two = exs(one) . eq three = exs(two) . eq four = exs(three) . eq five = exs(four) . eq six = exs(five) . eq seven = exs(six) . eq eight = exs(seven) . eq nine = exs(eight) . eq ten = exs(nine) . eq eleven = exs(ten) . eq twelve = exs(eleven) . eq thirteen = exs(twelve) . eq fourteen = exs(thirteen) . eq fifteen = exs(fourteen) . eq sixteen = exs(fifteen) . eq seventeen = exs(sixteen) . eq eighteen = exs(seventeen) . eq nineteen = exs(eighteen) . eq twenty = exs(nineteen) . eq twentyone = exs(twenty) . eq twentytwo = exs(twentyone) . eq twentythree = exs(twentytwo) . eq twentyfour = exs(twentythree) . eq twentyfive = exs(twentyfour) . eq twentysix = exs(twentyfive) . eq twentyseven = exs(twentysix) . eq twentyeight = exs(twentyseven) . eq twentynine = exs(twentyeight) . eq thirty = exs(twentynine) . eq thirtyone = exs(thirty) . eq thirtytwo = exs(thirtyone) . eq thirtythree = exs(thirtytwo) . eq thirtyfour = exs(thirtythree) . eq thirtyfive = exs(thirtyfour) .
eq nat2sym(zero) = exz . eq nat2sym(s(X)) = exs(nat2sym(X)) .
eq expand(exz) = exz .
eq expand(exone) = exone .
eq expand(exs(Xs)) = explus(exone,expand(Xs)) .
eq expand(explus(Xs,Ys)) = explus(expand(Xs),expand(Ys)) .
eq expand(exmult(Xs,exz)) = exz .
eq expand(exmult(Xs,exone)) = expand(Xs) .
eq expand(exmult(Xs,explus(Ys,Zs))) =
expand(explus(exmult(Xs,Ys),exmult(Xs,Zs))) .
eq expand(exmult(Xs,Ys)) = expand(exmult(Xs,expand(Ys))) .
eq expand(exexp(Xs,exz)) = exone .
eq expand(exexp(Xs,exone)) = expand(Xs) .
eq expand(exexp(Xs,explus(Ys,Zs))) =
expand(exmult(exexp(Xs,Ys),exexp(Xs,Zs))) .
eq expand(exexp(Xs,Ys)) = expand(exexp(Xs, expand(Ys))) .
*** equations for trees
eq buildtree(zero, Val) = leaf(Val) .
eq buildtree(s(X),Y) = node(plus17(getval(buildtree(X,Y)),
getval(buildtree(X,succ17(getmax(buildtree(X,Y)))))),
getmax(buildtree(X,succ17(getmax(buildtree(X,Y))))),
buildtree(X,Y),
buildtree(X,succ17(getmax(buildtree(X,Y))))) .
endfm
