inv(false, true).
inv(true, false).

inv(P, not(P)):-atom(P).
inv(not(P), P):- atom(P).

inv(or(P,Q), and(P2,Q2)):- inv(P,P2),inv(Q,Q2).
inv(and(P,Q), or(P2,Q2)):- inv(P,P2),inv(Q,Q2).

inv(or(P,Q), and(Q2,P2)):- inv(P,P2),inv(Q,Q2).
inv(and(P,Q), or(Q2,P2)):- inv(P,P2),inv(Q,Q2).


%%%%%%%%%%%% proposition-logic  %%%%%%%%%%%%
%%%%%%%%%%%% not %%%%%%%%%%%%

simplify(not(false), mark(true, red), '<=> <i>{ ~F == T }</i>\n').
simplify(not(or(P,Q)), mark(and(not(P),not(Q)), green), '<=> <i>{ ~(p | q) == ~p & ~q  (De Morgan) }</i>\n').

simplify(not(true), mark(false, red), '<=> <i>{ ~T == F }</i>\n').
simplify(not(and(P,Q)), mark(or(not(P),not(Q)), green), '<=> <i>{ ~(p & q) == ~p | ~q  (De Morgan) }</i>\n').

simplify(not(not(P)), mark(P, red), '<=> <i>{ ~~p == q }</i>\n').

simplify(not(P), not(Q), MSG):-simplify(P,Q, MSG).

%%%%%%%%%%%% and-distribution %%%%%%%%%%%%

simplify(and(or(P,Q),R), mark(or(and(P,R),and(Q,R)),green), '<=> <i>{ (p | q) & r == (p & r) | (q & r)  (distribution)}</i>\n').
simplify(and(R,or(P,Q)), mark(or(and(R,P),and(R,Q)),green), '<=> <i>{ p & (q | r) == (p & q) | (p & r)  (distribution)}</i>\n').

%%%%%%%%%%%% and  %%%%%%%%%%%%
simplify(and(P,P2),and(Q,P2), MSG):-simplify(P,Q, MSG).    
simplify(and(P,P2),and(P,Q2), MSG):-simplify(P2,Q2, MSG).

simplify(and(P,and(Q,R)), mark(and(and(P,Q),R), green), '<=> <i>{ p & (q & r) == (p & q) & r  (association)}</i>\n').

simplify(and(true,P2), mark(P2,red), '<=> <i>{ T & p == p  }</i>\n').       %% T & p == p
simplify(and(P,true), mark(P,red), '<=> <i>{ p & T == p  }</i>\n').

simplify(and(P,Q), mark(P, red), '<=> <i>{ (.((.) & p) & .) & p ==  (.((.) & p) & .)  }</i>\n'):-inand(P,Q).  %% p & ... & p == p & ...
simplify(and(_,false), mark(false,red), '<=> <i>{ (.) & F == F }</i>\n').   %% F & p = F 
simplify(and(P,_), mark(false,red), '<=> <i>{ ( F & (.) == F  }</i>\n' ):-inand(P,false).
%%simplify(and(P,Q), mark(false,red), '<=> <i>{ (.(.) & ~p ).) & p == F }</i>\n'):- inv(P, P2), inor(P2,Q). %redundant%
simplify(and(P,Q), mark(false,red), '<=> <i>{ (.(.) & p ).) & ~p == F }</i>\n'):- inv(Q, Q2), inand(P,Q2).

%inand(+AndTree, +AndElement)
inand(P,P).
inand(and(P,_), R):- inand(P,R).
inand(and(_,Q), R):- inand(Q,R).

%%%%%%%%%%%% or  %%%%%%%%%%%%

simplify(or(P,P2),or(Q,P2), MSG):-simplify(P,Q, MSG).  
simplify(or(P,P2),or(P,Q2), MSG):-simplify(P2,Q2, MSG).

simplify(or(P,or(Q,R)), mark(or(or(P,Q),R),green), '<=> <i>{ p | (q | r) == (p | q) | r  (association)}</i>\n').

simplify(or(false,P2), mark(P2,red), '<=> <i>{ F | p == p }</i>\n').        %% F | p = p
simplify(or(P,false), mark(P,red), '<=> <i>{ p | F == p }</i>\n').  

simplify(or(P,Q), mark(P,red), '<=> <i>{  (.((.) | p) | .) | p ==  (.((.) | p) | .) }</i>\n'):-inor(P,Q).
simplify(or(_,true), mark(true, red), '<=> <i>{ (.) | T == T }</i>\n').     %% T | p = T 
simplify(or(P,_), mark(true, red), '<=> <i>{ T | (.) == T }</i>\n'):-inor(P,true).
%%simplify(or(P,Q), mark(true, red), '<=> <i>{ (.(.) | ~p ).) | p == T }</i>\n'):- inv(P, P2), inand(P2,Q). %redundant%
simplify(or(P,Q), mark(true, red), '<=> <i>{ (.(.) | p ).) | ~p == T }</i>\n'):- inv(Q, Q2), inor(P,Q2). 

simplify(or(P,Q), mark(Q,red), '<=> <i>{ (p & q) | q == q }</i>\n' ):- inand(P,Q).
simplify(or(P,Q), mark(P,red), '<=> <i>{ q | (p & q) == q }</i>\n'):- inand(Q,P).

%inor(+OrTree, +ORElement)
inor(P,P).
inor(or(P,_), R):- inor(P,R).
inor(or(_,Q), R):- inor(Q,R).













