holds(F, [F|_]).
holds(F, Z) :- Z=[F1|Z1], F\==F1, holds(F, Z1).

holds(F, [F|Z], Z).
holds(F, Z, [F1|Zp]) :- Z=[F1|Z1], F\==F1, holds(F, Z1, Zp).

minus_(Z, [], Z).
minus_(Z, [F|Fs], Zp) :-
   (\+ holds(F, Z) -> Z1=Z ; holds(F, Z, Z1)),
   minus_(Z1, Fs, Zp).

plus_(Z, [], Z).
plus_(Z, [F|Fs], Zp) :-
   (\+ holds(F, Z) -> Z1=[F|Z] ; holds(F, Z), Z1=Z),
   plus_(Z1, Fs, Zp).

update(Z1, ThetaP, ThetaN, Z2) :-
   minus_(Z1, ThetaN, Z), plus_(Z, ThetaP, Z2).

execute([],Z,Z) :- !.
execute([A|Acts],Z,Zr) :- !,execute(Acts,Z,Z1), execute(A,Z1,Zr).
execute(A, Z1, Z2) :- perform(A),
                      state_update(Z1, A, Z2).