pa([]).
pa([L|Ls]):-pa(Ls), write(L).

buildtree(P, _Ls):-atom(P), write(P), write('<font color=black>\n').
buildtree(not(P), Ls):- write('NOT-'), buildtree(P, ['    '|Ls]).
buildtree('K'(P), Ls):- write('K-'), buildtree(P, ['  '|Ls]).
buildtree('M'(P), Ls):- write('M-'), buildtree(P, ['  '|Ls]).
buildtree(and(P,Q), Ls):- write('AND-'), buildtree(P, ['  | '|Ls]),
           pa(Ls), write('  +-'), buildtree(Q, ['    '|Ls]).
buildtree(or(P,Q), Ls):- write('OR-'), buildtree(P, [' | '|Ls]),
           pa(Ls), write(' +-'), buildtree(Q, ['   '|Ls]).

buildtree(mark(P, R), Ls):- write('<font color='),write(R),write('>'),
                     buildtree(P, ['>',R,'<font color='|Ls]) .

buildtree(Tree):- buildtree(Tree, []).

s5(mark(P,R)):-atom(R), \+var(P), s5(P).
simplify(mark(P, R), mark(Q, R), MSG):-simplify(P, Q, MSG).


clean(P,P):-atom(P).
clean(not(P),not(P2)):-clean(P,P2).
clean('K'(P),'K'(P2)):-clean(P,P2).
clean('M'(P),'M'(P2)):-clean(P,P2).
clean(and(P,Q),and(P2,Q2)):-clean(P,P2), clean(Q,Q2).
clean(or(P,Q),or(P2,Q2)):-clean(P,P2), clean(Q,Q2).
clean(mark(P, _Q), P2):-clean(P,P2).


printexp(P):-atom(P), write(P).
printexp(not(P)):- write('not('), printexp(P), write(')').
printexp('K'(P)):- write('K('), printexp(P), write(')').
printexp('M'(P)):- write('M('), printexp(P), write(')').
printexp(and(P,Q)):- write('and('), printexp(P),write(','), printexp(Q), write(')').
printexp(or(P,Q)):- write('or('), printexp(P),write(','), printexp(Q), write(')').
printexp(mark(P, R)):- write('<font color='),write(R),write('>'), printexp(P), write('</font>').
