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).

not_holds(F, Z) :- \+ holds(F, Z).

minus(Z, [], Z).
minus(Z, [F|Fs], Zp) :-
   (holds(F, Z, Z1) ; not_holds(F, Z), Z1=Z),
   minus(Z1, Fs, Zp).

plus(Z, [], Z).
plus(Z, [F|Fs], Zp) :-
   (not_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) :- execute_action(A),
                      state_update(Z1, A, Z2).

execute_action(A) :- write(A), nl.