% samples test cases from specification

% the result of this test case is the binding of the closure to variable CLOSURE
fdinf([], [a,b,c,d], [[[a,b],[c]], [[c], [d]], [[d], [a]]], CLOSURE).

% the result of this test case is the binding of the closure to variable CLOSURE
fdinf([s], [a,b,c,d], [[[a,b],[c]], [[c], [d]], [[d], [a]]], CLOSURE).

% the result of this test case is yes
fdinf([], [a,b,c,d], [[[a,b],[c]], [[c], [d]], [[d], [a]]], [[[a,b],[c,d]], [[a,b,c],[d]], [[a,b,d],[c]], [[a,c],[d]], [[b,c],[a,d]], [[b,c,d],[a]], [[b,d],[a,c]], [[c],[a,d]], [[c,d],[a]], [[d],[a]]]).

% the result of this test case is yes
fdinf([s], [a,b,c,d], [[[a,b],[c]], [[c], [d]], [[d],[a]]], [[[a,b],[c]], [[a,b],[d]], [[a,b,c],[d]], [[a,b,d],[c]], [[a,c], [d]], [[b,c],[a]], [[b,c],[d]], [[b,c,d],[a]], [[b,d],[a]], [[b,d],[c]], [[c],[a]], [[c],[d]], [[c,d],[a]], [[d],[a]]]).


% the result of this test case is F1 |= F2
fdinf2([a,b,c], [[[a],[b]],[[b],[c]]], [[[a],[b]],[[a],[c]]]).

% the result of this test case is F1 |= F2
fdinf2([a,b,c], [[[a],[b]],[[b],[c]]], [[[a],[b]],[[a,b],[c]]]).

% the result of this test case is F1 and F2 are equivalent
fdinf2([a,b,c], [[[a],[b]],[[a],[c]]], [[[a],[b]],[[a,b],[c]]]).

% the result of this test case is the empty string
fdinf2([a,b,c], [[[a],[b]]], [[[b],[c]]]).

% the result of this test case is the binding of the minimal base to
% to variable MINIMAL_BASIS
fdinf([m], [a,b,c], [[[b],[a,c]], [[a],[b]], [[c],[b]], [[a],[c]], [[c],[a]], [[a,b],[c]], [[a,c],[b]], [[b,c],[a]]], MINIMAL_BASIS).

% the result of this test case is yes
fdinf([m], [a,b,c], [[[b],[a,c]], [[a],[b]], [[c],[b]], [[a],[c]], [[c],[a]],
[[a,b],[c]], [[a,c],[b]], [[b,c],[a]]], [[[[a],[b,c]], [[b],[a]], [[c],[a]]], [[[a],[b]], [[b],[a,c]], [[c],[b]]], [[[a],[c]], [[b],[c]], [[c],[a,b]]], [[[a],[b]], [[b],[c]], [[c],[a]]], [[[a],[c]], [[b],[a]], [[c],[b]]]]).

% the result of this test case is the binding of the minimal base to
% to variable MINIMAL_BASIS
fdinf([m,s], [a,b,c], [[[b],[a,c]], [[a],[b]], [[c],[b]], [[a],[c]], [[c],[a]]], MINIMAL_BASIS).

% the result of this test case is yes
fdinf([m,s], [a,b,c], [[[b],[a,c]], [[a],[b]], [[c],[b]], [[a],[c]], [[c],[a]]], [[[[a],[b]], [[a],[c]], [[b],[a]], [[c],[a]]], [[[a],[b]], [[b],[a]], [[b],[c]], [[c],[b]]], [[[a],[c]], [[b],[c]], [[c],[a]], [[c],[b]]], [[[a],[b]], [[b],[c]], [[c],[a]]], [[[a],[c]], [[b],[a]], [[c],[b]]]]).

% the result of this test case is the binding of the MVDs to variable MVDs
mineMVDs([a,b,c], [[x,y,z], [x,y,q], [p,y,z], [p,y,r]], MVDs).

% the result of this test case is yes 
mineMVDs([a,b,c], [[x,y,z], [x,y,q], [p,y,z], [p,y,r]], [[[a], [b]], [[a], [c]], [[c], [a]], [[c], [b]]]).