% This is a problem that was raised within the Schwerpunktprogramm
% Deduktion

sel_var(mk_pair(X1,V1))=X1.
sel_val(mk_pair(X2,V2))=V2.
car(cons(X3,V3))=X3.
cdr(cons(X4,V4))=V4.
sel_var(car(X5))=V5 -> look_up(X5,V5)=sel_val(car(X5)).
sel_var(car(X6))=V6, look_up(X6,V6)=look_up(cdr(X6),V6).
update(X7,Y7,Z7)=cons(mk_pair(Y7,Z7),X7).



% Beweisprobleme


a=b -> [].

% Problem 1
% look_up(update(e,a,1),b) = look_up(e,b) -> [].

% Problem 2
look_up(update(update(e,a,1),b,2),c) = 
   look_up(update(update(e,b,2),a,1),c) -> [].

precedence( [look_up,update,sel_var,sel_val,car,cdr,cons,mk_pair,nil,
	     foo,a,b,c,1,2,e] ).