subst([], [ bind(Val, Id) ], bind(Val, Id) ).
   
subst([ bind(_OldVal, Id) | More ], 
      [ bind(Val, Id) | More ], 
      bind(Val, Id) ).
      
subst([ bind(Val, Id) | More ],
      [ bind(Val, Id) | More1 ],
      bind(NewVal, NewId) ) :-
   not( Id=NewId ), 
   subst(More, More1, bind(NewVal, NewId)).

 and(true, true, true).
 and(true, false, false).
 and(false, true, false).
 and(false, false, false).

 or(false, false, false).
 or(true, _, true).
 or(_, true, true).

 binding( Id, [ bind(Val, Id) | _More], Val ).
 binding( Id, [ bind(_Val, OtherId) | More], Val) :-
   not( Id=OtherId ), binding( Id, More, Val ).
 eval(state(N, _Sigma), N) :- number(N).
 
 eval(state(X, Sigma), V) :-
    atom(X), binding(X, Sigma, V).
 
eval(state(app('+', A0, A1), Sigma), N) :-
   eval(state(A0, Sigma), N0),
   eval(state(A1, Sigma), N1), 
   N is N0+N1.

 eval(state(app('-', A0, A1), Sigma), N) :-
    eval(state(A0, Sigma), N0),
    eval(state(A1, Sigma), N1),
    N is N0-N1.
 eval(state(app('*', A0, A1), Sigma), N) :-
    eval(state(A0, Sigma), N0),
    eval(state(A1, Sigma), N1),
    N is N0*N1.

 eval(state(true, _Sigma), true).
 eval(state(false, _Sigma), false).

 
 eval(state(app('=', A0, A1), Sigma), true) :- 
     eval(state(A0, Sigma), N0),
     eval(state(A1, Sigma), N1),
     N0 = N1 .
 eval(state(app('=', A0, A1), Sigma), false) :- 
     eval(state(A0, Sigma), N0),
     eval(state(A1, Sigma), N1),
     not(N0 = N1) .	    

 eval(state(app('=<', A0, A1), Sigma), true) :- 
     eval(state(A0, Sigma), N0),
     eval(state(A1, Sigma), N1),
     N0 =< N1 .
 eval(state(app('=<', A0, A1), Sigma), false) :- 
     eval(state(A0, Sigma), N0),
     eval(state(A1, Sigma), N1),
     not(N0 =< N1) .	    

   
   eval(state(app(not, B), Sigma), false) :- 
       eval(state(B, Sigma), true) .
   eval(state(app(not, B), Sigma), true) :- 
       eval(state(B, Sigma), false) .

   eval(state(app(and, A0, A1), Sigma), T) :- 
       eval(state(A0, Sigma), T0),
       eval(state(A1, Sigma), T1),
       and(T0, T1, T).
       

   eval(state(app(or, A0, A1), Sigma), T) :- 
       eval(state(A0, Sigma), T0),
       eval(state(A1, Sigma), T1),
       and(T0, T1, T).
       
     eval(state(assgn(Id, A), Sigma), Sigma1) :-
	 eval(state(A, Sigma), N),
	 subst(Sigma, Sigma1, bind(N, Id)).

     eval(state(skip, Sigma), Sigma).

     eval(state(seq(C0, C1), Sigma), Sigma1) :-
	 eval(state(C0, Sigma), Sigma2),
	 eval(state(C1, Sigma2), Sigma1) .


eval(state(if(B, C0, _C1), Sigma), Sigma1) :-
    eval(state(B, Sigma), true),
    eval(state(C0, Sigma), Sigma1).
eval(state(if(B, _C0, C1), Sigma), Sigma1) :-
    eval(state(B, Sigma), false),
    eval(state(C1, Sigma), Sigma1).

eval(state(while(B, _C), Sigma), Sigma) :- 
   eval(state(B, Sigma), false).

eval(state(while(B, C), Sigma), Sigma1) :-
   eval(state(B, Sigma), true),
   eval(state(C, Sigma), Sigma2),
   eval(state(while(B, C), Sigma2), Sigma1).