% Autor: MB
% Datum: 11.05.2016

% Counting the distinct variables in a list of terms
anzahlVariablen([],[],0).
anzahlVariablen([H|T],Variablen,N):- var(H),
                                     anzahlVariablen(T,TailVariablen,NT),
                                     memberVariable(H,TailVariablen),
                                     Variablen = TailVariablen,
                                     N is NT, !.
anzahlVariablen([H|T],Variablen,N):- var(H),
                                     anzahlVariablen(T,TailVariablen,NT),
                                     Variablen = [H|TailVariablen],
                                     N is NT + 1, !.
anzahlVariablen([_|T],Variablen,N):- anzahlVariablen(T,Variablen,N).
% test: anzahlVariablen([1,2,C,4,5,6,Z,U],Variablen,Anzahl).

% "member(X,[Y])" is true, since they become unified!
% So we need a special predicate.
memberVariable(X,[H|_]):- X == H, !.
memberVariable(X,[_|T]):- memberVariable(X,T).
% test: memberVariable(X,[3,5,6,F,H,i,O]).

flacheTermliste(C,[C]):- (atom(C); var(C)), !.
flacheTermliste(Term,Liste):- compound(Term), not(is_list(Term)),
                              Term =.. [Funktor|Anfangsliste],
                              flacheTermliste(Anfangsliste,Endliste),
                              append([Funktor],Endliste,Liste), !.
flacheTermliste([],[]).
flacheTermliste([H|T],Liste):- compound(H),
                               flacheTermliste(T,Tailliste),
                               flacheTermliste(H,Headliste),
                               append(Headliste,Tailliste,Liste), !.
flacheTermliste([H|T],Liste):- flacheTermliste(T,Tailliste),
                               append([H],Tailliste,Liste), !.
% test: flacheTermliste(wenn_dann(P,wenn_dann(E,D)),Liste).

verschiedeneVariablen(X,Y):- not(memberVariable(X,[Y])),
                             not(memberVariable(Y,[X])).