symbol(X) :- delta(_,X,_), X \== nil.
alphabet(A) :- setof(X,symbol(X),A).
all_final_states(F) :- setof(X,final_state(X),F).
intersect([],_,[]).
intersect([X|L],S1,[X|S]) :- member(X,S1),!,intersect(L,S1,S).
intersect([_|L],S1,S) :- intersect(L,S1,S). 
state(Q) :- delta(Q,_,_).
state(Q) :- delta(_,_,Q).
states(S) :- setof(Q,state(Q),S).
e_path(Q,Q,_,_).
e_path(Q,R,_,_) :- delta(Q,nil,R).
e_path(Q,R,N,NStates) :- delta(Q,nil,P), M is N+1, M < NStates, e_path(P,R,M,NStates).
e_closure(Q,C) :- states(S), length(S,NStates), setof(R,e_path(Q,R,0,NStates),C).
set_e_closure([],[]).
set_e_closure([Q|L],D) :- e_closure(Q,C), set_e_closure(L,M),
                          union(C,M,D).
set_d([],_,[]).
set_d([Q|L],X,D) :- d(Q,X,P1), set_d(L,X,P2), union(P1,P2,D).
d(Q,A,S) :- setof(P,delta(Q,A,P),S),!.
d(_,_,[]).
rm_etrans :- tell('out.dat'),alphabet(A),print_start,states(S),
             process(A,S),decide_final(S), told.
print_start :- start_state(S), write(start_state), write('('), write(S),
               write(')'), write('.'),nl. 
process(_,[]).
process(A,[Q|L]) :- process_state(A,Q), process(A,L).
process_state([],_).
process_state([X|L],Q) :- e_closure(Q,C), set_d(C,X,D),
              set_e_closure(D,P), output(Q,X,P), process_state(L,Q).
output(_,_,[]).
output(Q,X,[P|L]) :- write(delta),write('('),write(Q),write(','),
                     write(X), write(','), write(P), write(')'),
                     write('.'), nl, output(Q,X,L).
decide_final([]).
decide_final([Q|L]) :- e_closure(Q,C), all_final_states(F),
                       intersect(C,F,S), S \== [], !, write(final_state),
                       write('('), write(Q), write(')'), write('.'), nl,
                       decide_final(L).
decide_final([_|L]) :- decide_final(L).
