i(+,up,up).
i(+,down,down).
i(-,down,up).
i(-,up,down).

:- op(701,xfx,(at)).


v(A=X at T, W,W) :-
       member(A=X at T, W).

v(A=X at T0,W0,W) :-
       e(A,I,B),
       i(I,X,Y),
       t(B=Y,W0,T0,T),
       not(nogood(B=Y at T,W0)),
       v(B=Y at T,[B=Y at T|W0],W).

e(A,I,B) :- e0(A,I,B).
e(A,I,B) :- e0(B,I,A).

:- dynamic e0/3.

term_expansion(- [X=X|T],       Rest    ) :- term_expansion(- T,Rest).
term_expansion(- [A + B|T],     [e0(A,+,B)|Rest]) :- term_expansion(- T,Rest).
term_expansion(- [A - B|T],     [e0(A,-,B)|Rest]) :- term_expansion(- T,Rest).
term_expansion(- [],            []).

t0(A=X,W,T,next(T)) :- member(A=Y at T,W), not(X=Y),!.
t0(_,_,T ,T).
t0(_,_,T, next(T)).

t(Z,W,T0,T) :- t0(Z,W,T0,T), not(tooLong(T)).

tooLong(next(next(_))).

nogood(X,L) :- not(member(X,L)).
nogood(This = That at Time,L) :- member(This=That1 at Time, L), not(That=That1).