nWeight(X,W) :-leafWeightCardinality(X,W,C).

nCard(X,C)  :-leafWeightCardinality(X,W,C).

leaf(X):-leafWeightCardinality(X,W,C).


% --------------------------------------------------------------
% --------------------------------------------------------------
% --------------------------------------------------------------
% BEGIN  Tree Definition 

%%
%% Tree T' Generation and Test
%%
%% GENERATE  tree
%%
childRight(R,P) v nonChildRight(R,P)  :-  innerNode(P), leaf(R).
:- childRight(R,P), childRight(R1,P), R1 != R.
hasChildRight(P) :- childRight(R,P).
:- innerNode(P), not hasChildRight(P).

innerLeftRight(P,P1,R) :- innerNode(P), P1 = P - 1, P>1, childRight(R,P).

%
% Inner node 1 has two leafs
%
innerLeftRight(1,L,R) v notInnerLeftRight(1,L,R)  :- leaf(L), childRight(R,1).

%%
%% TEST  tree
%%
%same leaf cannot be a leaf of a different parent 
:-childRight(R,P1), childRight(R,P2), P1!=P2.

%someones right child
child(N):-childRight(N,P).
%left child of the first inner node may not be right child of someone else.
:-innerLeftRight(1,L,R), child(L).


% END  Tree Definition 
% --------------------------------------------------------------
% --------------------------------------------------------------
% --------------------------------------------------------------
% BEGIN Weight T  definition

%  if color of X is green
%    weight(X) = weight(right child of X) + cardinality(right child of X) 
%

weight(green,P,W):- innerNodeColor(P,green), W= W1+C, 
			nWeight(R,W1), nCard(R,C),
            childRight(R,P), leaf(R).




%  if color of X is red
%     weight(X) = weight(right child of X) + weight(left child of X) 
%
weight(red,P,W):- innerNodeColor(P,red), W= W1+W2,
			nWeight(R,W1),nWeight(L,W2),
			innerLeftRight(P,L,R), leaf(R).



%  if color(X) is blue
%     weight(X) = cardinality(right child of X) + weight(left child of X) 
%
weight(blue, P,W):- innerNodeColor(P,blue), W= W1+C, 
			nCard(R,C), nWeight(L,W1),
			innerLeftRight(P,L,R), leaf(R).


%%
%% each inner node in primer tree T' has a unique color
%%
innerNodeColor(P,red) v innerNodeColor(P,green) v innerNodeColor(P,blue) :- innerNode(P).


nWeight(P,W):- weight(C,P,W).
%%
%% Weights related Tests
%%

%% 
%% definition of a total weight of a prime tree T'
tWeight(1,W):-nWeight(1,W).
tWeight(N,W):-W=W1+W2, N1 = N-1, tWeight(N1,W1), nWeight(N,W2),innerNode(N),N>1.


% END Weight T definition
% --------------------------------------------------------------
% --------------------------------------------------------------
% --------------------------------------------------------------
% exists Definition


exists:- tWeight(N1,W), N1 = N-1, W<=M, max_total_weight(M),num(N).
:-not exists.