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(A, Z1, Z2) :-
   perform(A, E), state_updates(Z1, [A|E], Z2).

state_updates(Z, [], Z).
state_updates(Z1, [A|S], Z2) :-
   state_update(Z1, A, Z), state_updates(Z, S, Z2).