/************************************************************
  Computing social welfare functions and distributing rights
  program: cswf06.pl
  language: prolog
  date: 2006.12.14-21,24
  revised: 2007.7.5
  creator: Kenryo INDO
************************************************************/
% load preference generator if r/1 does not exist.
:- (\+ clause(r(_),_)->[gprf06];true).

:- dynamic r/1.   % possible profiles (rr/1)

% members of society
:- dynamic agents/1.
agents([1,2]).
model(states:A, agents:N):-alternatives(A),agents(N).
make_n_agents(N):-
   abolish(agents/1),length(L,N),
   findall(K,nth1(K,L,_),L),assert(agents(L)).
j(X):- agents(N),member(X,N).

% profile : the domain of swf
rr([R|Q],[_|N]):- rr(Q,N),r(R).
rr([],[]).
rr(QQ):- model(_,_:N),rr(QQ,N).
r_j(J,PP,R):- rr(PP),j(J),nth1(J,PP,R).
r_j(-J,PP,R,QL):- r_j(J,PP,R), findall(Q,(r_j(K,PP,Q),K\=J),QL).
rr_b(_,[],[]).
rr_b(XY,[A|B],[Q|R]):- rr_b(XY,B,R),rb(A,XY,Q). 
all_rr(L):- findall(QQ,rr(QQ),L).

% possible types of swf values: 
%  t(Q), l(Q), q(Q), a(Q), o(Q) in gprf06.pl.

swf([],[],_).
swf([RR->Q|F],[RR|L],X):- swf(F,L,X),axiom_swf(X,RR->Q,F).
swf(F,X):-all_rr(L),swf(F,L,X).

% axioms for swf
axiom_swf(iia,RR->Q,F):- r(Q),iia(RR->Q,F).
axiom_swf(pareto,RR->Q,_):- r(Q), pareto(RR->Q).
axiom_swf(arrow,RR->Q,F):- r(Q),t(Q),pareto(RR->Q),iia(RR->Q,F).
axiom_swf(wilson,RR->Q,F):- r(Q),t(Q),iia(RR->Q,F).
axiom_swf(sen,RR->Q,F):- q(Q),pareto(RR->Q),iia(RR->Q,F).
axiom_swf(iia(T),RR->Q,F):- r(Q,_,_,T), iia(RR->Q,F).
axiom_swf(pareto(T),RR->Q,_):- r(Q,_,_,T), pareto(RR->Q).
axiom_swf(arrow(T),RR->Q,F):- r(Q,_,_,T), pareto(RR->Q),iia(RR->Q,F).
axiom_swf(wilson(T),RR->Q,F):- r(Q,_,_,T), iia(RR->Q,F).
axiom_swf(bnom,RR->Q,_):- bnom(RR->Q). % a binominating rule.
axiom_swf(olig(C),RR->Q,_):- q(Q), oligarchy(C,[RR->Q]).
axiom_swf(decisive(B),RR->Q,_):- r(Q),decisive(B,RR->Q).
axiom_swf(rights(B),RR->Q,_):- r(Q),rights(B,RR->Q).
axiom_swf(rights_p(B),RR->Q,_):- r(Q),rights(B,RR->Q),pareto(RR->Q).
axiom_swf(rights_i(B),RR->Q,F):- r(Q),rights(B,RR->Q),iia(RR->Q,F).
axiom_swf(na_decisive(L),RR->Q,F):- r(Q),na_decisive(L,RR->Q,F).
axiom_swf(majority_2,RR->Q,_):- agents([_,_]),majority_2(RR->Q).
axiom_swf(majority,RR->Q,_):- majority(RR->Q).

dictator(J,F):- j(J),\+ (member(PP->R,F),r_j(J,PP,P),opposite(+,_,[P,R])).
%pareto([P,Q]->R):- \+ (p(XY,P),p(XY,Q),\+ p(XY,R)).
pareto(RR->R):- \+ (agree(+,XY,RR),\+ p(XY,R)).
iia(RR->R,F):- \+ niia(RR->R,F).
niia([P,Q]->R,F):- F\=[], rr_b(XY,A,[P,Q]), member([U,T]->S,F),
   rr_b(XY,A,[U,T]), \+ agree(_,XY,[R,S]).
%niia(RR->R,F):- F\=[], rr_b(XY,A,RR), member(QQ->S,F),
%   rr_b(XY,A,QQ), \+ agree(_,XY,[R,S]).
debug_iia(RR->R,QQ->S,XY,A):- nl,write(RR->R;QQ->S;[XY];A).

agree(_,_,[]).
%agree(+,XY,[Q]):- p(XY,Q).
%agree(-,XY,[Q]):- XY=(X,Y),p((Y,X),Q).
agree(+,XY,[Q|R]):- agree(+,XY,R),p(XY,Q).
agree(-,XY,[Q|R]):- agree(-,XY,R),XY=(X,Y),p((Y,X),Q).
agree(0,XY,[Q|R]):- agree(0,XY,R),i(XY,Q).
opposite(+,(X,Y),[Q,R]):- p((X,Y),Q),r((Y,X),R).
opposite(-,(X,Y),[Q,R]):- p((Y,X),Q),r((X,Y),R).
opposite(S,XY,QR):- length(QR,K),K>2,opposite(S,_,XY,QR).
opposite(+,J,XY,QQ):- r_j(-J,QQ,R,QL),p(XY,R),agree(-,XY,QL). 
opposite(-,J,XY,QQ):- r_j(-J,QQ,R,QL),X=(X,Y),p((Y,X),R),agree(+,XY,QL).

% citizen's sovereignty
cs(F):- forall(dop(XY),(member(_->S,F),r(XY,S))).

% anti-dictatorship
ad(J,F):- j(J),\+ (member(PP->R,F),r_j(J,PP,P),agree(+,_,[P,R])).

% bi-nominating rule
bnom([[],[]]->[]).
bnom([[B|P],[C|R]]->[A|Q]):-
   bnom([P,R]->Q),
   member((B,C,A),[(+,-,0),(-,+,0),(+,+,+),(-,-,-)]).

% oligarchy, vetoers, decisive group
oligarchy(_,[]).
oligarchy(C,[RR->Q|F]):- oligarchy(C,F),vetoers(C,RR->Q),
   \+ (dop(XY),\+ decisive_group(C,XY,RR->Q)).

vetoers([],_). 
vetoers([J|C],RR->Q):- vetoers(C,RR->Q),a_veoter(J,RR->Q).
a_veoter(J,RR->Q):- r_j(J,RR,R),\+ (p((X,Y),R),p((Y,X),Q)). 

decisive_group(C,XY,RR->Q):- 
   forall(
     forall((member(J,C),r_j(J,RR,R)),p(XY,R)),
     p(XY,Q)
   ).

% decisiveness (at a profile) for pairs to an individual
decisive([]->_,_).
decisive([XY|E]->J,[P,Q]->S):-
   decisive(E->J,[P,Q]->S),
   member(J:R,[1:P,2:Q]),
   \+ opposite(_,XY,[R,S]).

% almost decisiveness (with a detector)
a_decisive(XY:[P,Q]->J,0,[P,Q]->S):-
   member(J:R:U,[1:P:Q,2:Q:P]),
   opposite(_,XY,[R,U]),
   \+ opposite(_,XY,[R,S]).
a_decisive(X,X,_).

% distribution of rights among individuals
rights(XY->1;WZ->2,[P,Q]->R):-
   \+ opposite(_,XY,[P,R]),agree(_,WZ,[Q,R]).

rights([],_).
rights([XY->J|E],[P,Q]->S):-
   rights(E,[P,Q]->S),
   member(J:R,[1:P,2:Q]),
   \+ opposite(_,XY,[R,S]).

% deter all almost decisiveness
na_decisive(L,RR->Q,F):-
   subset(L,[p,i]),
   \+ a_decisive(_->_,0,RR->Q),
   (member(p,L)->pareto(RR->Q);true),
   (member(i,L)->iia(RR->Q,F);true).

% simple majority principle
majority_2([[],[]]->[]).
majority_2([[T|P],[T|Q]]->[T|R]):-majority_2([P,Q]->R).
majority_2([[T|P],[F|Q]]->[0|R]):-majority_2([P,Q]->R),T\=F.

majority(QQ->R):- findall(XY,d_pair(XY),L), majority(L,QQ->R).
majority([],_->[]).
majority([XY|L],QQ->[S|R]):- majority(L,QQ->R),majority(S,XY,QQ).

% correct: 05 Jul 2007
majority(S,XY,QQ):- d_pair(XY),length(QQ,N),
   count_ballot(XY,QQ->S,M1),
   cop(XY,YX),
   count_ballot(YX,QQ->S,M2),
   sign_majority(S,N,M1,M2).
sign_majority(+,N,M1,M2):- N < 2 * M1,N >= 2 * M2, !.
sign_majority(-,N,M1,M2):- N >= 2 * M1,N < 2 * M2, !.
sign_majority(0,_,_,_). 

count_ballot(_,[]->_,0).
count_ballot(XY,[R|Q]->S,K):-
   count_ballot(XY,Q->S,M),
   (r(XY,R)->B=1;B=0),
   K is M + B.

cop((X,Y),(Y,X)).


/*

?- r(M,_,B),cycle(B),name_domain(A,[M]).

M = [+, -, +]
B = [a>b, c>a, b>c]
A = 'G' ;

M = [-, +, -]
B = [b>a, a>c, c>b]
A = 'V' ;

No
?- make_n_agents(4).

Yes
?- rr(A),majority(A->M),r(M,_,B),cycle(B).

No
?- rr(A),majority(A->M),\+ a(M).

No
?- rr(A),majority(A->M),nt(M).

A = [[-, -, +], [-, -, +], [+, +, +], [+, +, +]]
M = [0, 0, +] ;

A = [[+, -, -], [-, -, +], [+, +, +], [+, +, +]]
M = [+, 0, +] 

Yes
?- make_n_agents(5).

Yes
?- rr(A),majority(A->M),r(M,_,B),cycle(B).

A = [[+, -, -], [-, -, +], [-, -, +], [+, +, +], [+, +, +]]
M = [+, -, +]
B = [a>b, c>a, b>c] 

Yes
?-

*/

%  five types of display
%-------------------
% (1) simple table in symbols
 
display_swf(F):-show_swf(F).
display_swf_t1(F):-show_swf(F).

show_swf(F):-
   \+ var(F),agents([1,2]),
   display_swf_header,
   hr(20),
   forall( id_r(_:I,P),
    (
     an_swf_line(L,P,F),
     nl,write(P=I),tab(2),write('|'),
     write_sequence(L)
    )
   ).

display_swf_header:-
   bagof(N,K^R^id_r(K:N,R),L),
   nl,write('swf:row  col |'),
   write_sequence(L).

write_sequence(L):-
  forall(member(B,L),write(B)).

hr(N):-
   length(L,N),
   nl,
   forall(member(_,L),write('-')).

an_swf_line(L,P,F):-
   bagof(N, K^Q^R^B^(
     id_r(K:N,R,B),
     member([P,Q]->R,F)
   ),L).

%-------------------
% (2) a compound table in symbols + binaries

display_swf_t2(F):- show_swf_ct(F).

show_swf_ct(F):-
   \+ var(F),agents([1,2]),
   length(F,_),
%   bin_swf(Fxy,F),
   display_swf_header,
   forall(d_pair(XY),display_swf_header(XY)),
   hr(50),
   forall(
    (
     id_r(_:I,P),
     an_swf_line(L,P,F),
     nl,write(P=I),write('  |'),
     write_sequence(L),
     d_pair(XY)
    ),
     display_swf_bb(XY,P,F)
   ).

display_swf_header(XY):-
   b(XY),
   findall(T,(id_r(_,R),rb(T,XY,R)),L),
   tab(1),XY=(X,Y),
   write(X),write(Y),write(|),
   write_sequence(L).

display_swf_bb(XY,P,F):-
   rb(T_row,XY,P),
   tab(2),write(T_row),write('|'),
   findall(T,(
     id_r(_,Q),
     member([P,Q]->R,F),
     rb(T,XY,R)
   ),L),
   write_sequence(L).

%-------------------
% (3) lined profiles in binaries

display_swf_t3(F):-show_swf_l(F).
display_swf_t3(XY,F):-show_swf_l(XY,F).

show_swf_l(F):-
   \+ var(F),
   forall(j(J),write_component_wise_swf(_,[J],F)),
   write_component_wise_swf(_,soc,F).

show_swf_l(XY,F):-
   \+ var(F),
   d_pair(XY),
   forall(j(J),write_component_wise_swf(XY,[J],F)),
   write_component_wise_swf(XY,soc,F).

select_swf_component(_,[J],P,QQ->_):- r_j(J,QQ,P).
select_swf_component(_,soc,P,_->P).

write_component_wise_swf(XY,C,F):-
   forall(d_pair(XY),(
     nl,write(XY:C),write(:),
     forall(member(Element,F),(
       select_swf_component(XY,C,P,Element),
       rb(T,XY,P),write(T)
     ))
   )).

%-------------------
% (4) table for a pair in signs

display_swf_t4(XY,F):-show_swf_b(XY,F).

show_swf_b(XY,F):-
   \+ var(F),agents([1,2]),
   decompose_swf_into_tables(F,W),
   write_header_swf(XY,W,_),
   write_swf_contents(XY,W).

decompose_swf_into_tables(F,W):-
   findall(J:L, bagof(C,K^member([J,K]->C,F),L),W).

write_header_swf(XY,W,N):-
   length(W,N),length(H,N),d_pair(XY),nl,write(swf:wrt(XY)),
   tab(1),forall(nth1(K,H,_),(tab(2),write(r(K)))).

write_swf_contents(XY,W):-
   d_pair(XY),
   forall(nth1(K,W,J:L),(
     nl,write(r(K)=J),write_each_swf_row_as_binary(XY,L)
   )).

write_each_swf_row_as_binary(XY,L):-
   d_pair(XY),
   forall(member(R,L),(tab(5),rb(T,XY,R),write(T))).

%-------------------
% (5) lined profiles in alphabets

display_swf_t5(F):-show_swf_la(F).

show_swf_la(F):-
   \+ var(F),
   forall(j(J),write_agent_wise_swf(_,[J],F)),
   write_agent_wise_swf(_,soc,F).

write_agent_wise_swf(XY,C,F):-
   nl,write(C),write(:),
   forall(member(Element,F),(
     select_swf_component(XY,C,P,Element),
     id_r(_:N,P),write(N)
   )).


%-----
% demo

% impossibility theorems (Arrow-Wilson) and
% a possibility theorem (Sen)

/*

?- [menu].
% menu compiled 0.00 sec, 0 bytes

Yes
?- stopwatch((swf(F,arrow),nl,display_swf_t2(F),fail;true),T).


swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |ACITZN  +|+--++-  +|++-+--  +|+++---
[-, +, +]=C  |ACITZN  -|+--++-  +|++-+--  +|+++---
[-, -, +]=I  |ACITZN  -|+--++-  -|++-+--  +|+++---
[+, +, -]=T  |ACITZN  +|+--++-  +|++-+--  -|+++---
[+, -, -]=Z  |ACITZN  +|+--++-  -|++-+--  -|+++---
[-, -, -]=N  |ACITZN  -|+--++-  -|++-+--  -|+++---

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |AAAAAA  +|++++++  +|++++++  +|++++++
[-, +, +]=C  |CCCCCC  -|------  +|++++++  +|++++++
[-, -, +]=I  |IIIIII  -|------  -|------  +|++++++
[+, +, -]=T  |TTTTTT  +|++++++  +|++++++  -|------
[+, -, -]=Z  |ZZZZZZ  +|++++++  -|------  -|------
[-, -, -]=N  |NNNNNN  -|------  -|------  -|------
% time elapsed (sec): 2

F = _G157
T = 2 

Yes
?- stopwatch((swf(F,wilsom),cs(F),nl,display_swf_t2(F),fail;true),T).


swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |ACITZN  +|+--++-  +|++-+--  +|+++---
[-, +, +]=C  |ACITZN  -|+--++-  +|++-+--  +|+++---
[-, -, +]=I  |ACITZN  -|+--++-  -|++-+--  +|+++---
[+, +, -]=T  |ACITZN  +|+--++-  +|++-+--  -|+++---
[+, -, -]=Z  |ACITZN  +|+--++-  -|++-+--  -|+++---
[-, -, -]=N  |ACITZN  -|+--++-  -|++-+--  -|+++---

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |AAAAAA  +|++++++  +|++++++  +|++++++
[-, +, +]=C  |CCCCCC  -|------  +|++++++  +|++++++
[-, -, +]=I  |IIIIII  -|------  -|------  +|++++++
[+, +, -]=T  |TTTTTT  +|++++++  +|++++++  -|------
[+, -, -]=Z  |ZZZZZZ  +|++++++  -|------  -|------
[-, -, -]=N  |NNNNNN  -|------  -|------  -|------

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |ACITZN  +|-++--+  +|--+-++  +|---+++
[-, +, +]=C  |ACITZN  -|-++--+  +|--+-++  +|---+++
[-, -, +]=I  |ACITZN  -|-++--+  -|--+-++  +|---+++
[+, +, -]=T  |ACITZN  +|-++--+  +|--+-++  -|---+++
[+, -, -]=Z  |ACITZN  +|-++--+  -|--+-++  -|---+++
[-, -, -]=N  |ACITZN  -|-++--+  -|--+-++  -|---+++

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |ACITZN  +|+--++-  +|++-+--  +|+++---
[-, +, +]=C  |ACITZN  -|+--++-  +|++-+--  +|+++---
[-, -, +]=I  |ACITZN  -|+--++-  -|++-+--  +|+++---
[+, +, -]=T  |ACITZN  +|+--++-  +|++-+--  -|+++---
[+, -, -]=Z  |ACITZN  +|+--++-  -|++-+--  -|+++---
[-, -, -]=N  |ACITZN  -|+--++-  -|++-+--  -|+++---

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |AAAAAA  +|++++++  +|++++++  +|++++++
[-, +, +]=C  |CCCCCC  -|------  +|++++++  +|++++++
[-, -, +]=I  |IIIIII  -|------  -|------  +|++++++
[+, +, -]=T  |TTTTTT  +|++++++  +|++++++  -|------
[+, -, -]=Z  |ZZZZZZ  +|++++++  -|------  -|------
[-, -, -]=N  |NNNNNN  -|------  -|------  -|------
% time elapsed (sec): 48.234

F = _G157
T = 48.234 

Yes
?- stopwatch((swf(F,sen),nl,display_swf_t2(F),fail;true),T).


swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |ACITZN  +|+--++-  +|++-+--  +|+++---
[-, +, +]=C  |ACITZN  -|+--++-  +|++-+--  +|+++---
[-, -, +]=I  |ACITZN  -|+--++-  -|++-+--  +|+++---
[+, +, -]=T  |ACITZN  +|+--++-  +|++-+--  -|+++---
[+, -, -]=Z  |ACITZN  +|+--++-  -|++-+--  -|+++---
[-, -, -]=N  |ACITZN  -|+--++-  -|++-+--  -|+++---

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |ABEJMO  +|+00++0  +|++0+00  +|+++000
[-, +, +]=C  |BCFKOP  -|0--00-  +|++0+00  +|+++000
[-, -, +]=I  |EFIORS  -|0--00-  -|00-0--  +|+++000
[+, +, -]=T  |JKOTWX  +|+00++0  +|++0+00  -|000---
[+, -, -]=Z  |MORWZn  +|+00++0  -|00-0--  -|000---
[-, -, -]=N  |OPSXnN  -|0--00-  -|00-0--  -|000---

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |AAAAAA  +|++++++  +|++++++  +|++++++
[-, +, +]=C  |CCCCCC  -|------  +|++++++  +|++++++
[-, -, +]=I  |IIIIII  -|------  -|------  +|++++++
[+, +, -]=T  |TTTTTT  +|++++++  +|++++++  -|------
[+, -, -]=Z  |ZZZZZZ  +|++++++  -|------  -|------
[-, -, -]=N  |NNNNNN  -|------  -|------  -|------
% time elapsed (sec): 10.75

F = _G157
T = 10.75 

Yes
?- swf(F,bnom),display_swf_t2(F),fail.

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |ABEJMO  +|+00++0  +|++0+00  +|+++000
[-, +, +]=C  |BCFKOP  -|0--00-  +|++0+00  +|+++000
[-, -, +]=I  |EFIORS  -|0--00-  -|00-0--  +|+++000
[+, +, -]=T  |JKOTWX  +|+00++0  +|++0+00  -|000---
[+, -, -]=Z  |MORWZn  +|+00++0  -|00-0--  -|000---
[-, -, -]=N  |OPSXnN  -|0--00-  -|00-0--  -|000---

No
?- 
*/

% verify above result is the oligarchy.

/*

?- member(G,[[1,2],[1],[2]]),swf(F,olig(G)),display_swf_t2(F),nl,fail.

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |ABEJMO  +|+00++0  +|++0+00  +|+++000
[-, +, +]=C  |BCFKOP  -|0--00-  +|++0+00  +|+++000
[-, -, +]=I  |EFIORS  -|0--00-  -|00-0--  +|+++000
[+, +, -]=T  |JKOTWX  +|+00++0  +|++0+00  -|000---
[+, -, -]=Z  |MORWZn  +|+00++0  -|00-0--  -|000---
[-, -, -]=N  |OPSXnN  -|0--00-  -|00-0--  -|000---

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |AAAAAA  +|++++++  +|++++++  +|++++++
[-, +, +]=C  |CCCCCC  -|------  +|++++++  +|++++++
[-, -, +]=I  |IIIIII  -|------  -|------  +|++++++
[+, +, -]=T  |TTTTTT  +|++++++  +|++++++  -|------
[+, -, -]=Z  |ZZZZZZ  +|++++++  -|------  -|------
[-, -, -]=N  |NNNNNN  -|------  -|------  -|------

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |ACITZN  +|+--++-  +|++-+--  +|+++---
[-, +, +]=C  |ACITZN  -|+--++-  +|++-+--  +|+++---
[-, -, +]=I  |ACITZN  -|+--++-  -|++-+--  +|+++---
[+, +, -]=T  |ACITZN  +|+--++-  +|++-+--  -|+++---
[+, -, -]=Z  |ACITZN  +|+--++-  -|++-+--  -|+++---
[-, -, -]=N  |ACITZN  -|+--++-  -|++-+--  -|+++---

No
?-

*/

% verify that above nondictatorship (origarchy) is the pairwise majority vote.

/*

?- stopwatch((swf(F,majority),display_swf_t2(F),fail;true),T).

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |ABEJMO  +|+00++0  +|++0+00  +|+++000
[-, +, +]=C  |BCFKOP  -|0--00-  +|++0+00  +|+++000
[-, -, +]=I  |EFIORS  -|0--00-  -|00-0--  +|+++000
[+, +, -]=T  |JKOTWX  +|+00++0  +|++0+00  -|000---
[+, -, -]=Z  |MORWZn  +|+00++0  -|00-0--  -|000---
[-, -, -]=N  |OPSXnN  -|0--00-  -|00-0--  -|000---
% time elapsed (sec): 0.062

F = _G160
T = 0.062 

Yes
?-

*/



% verifying the decomposability of decisiveness 
% (or the possibility of distributing individual rights)

/*
?- swf(F,rights([(a,b)->1,(a,c)->2])),display_swf_t2(F),!,fail.

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |AAAZZZ  +|++++++  +|++-+--  +|++-+--
[-, +, +]=C  |CCCIII  -|------  +|++-+--  +|++++++
[-, -, +]=I  |CCCIII  -|------  -|++-+--  +|++++++
[+, +, -]=T  |AAAZZZ  +|++++++  +|++-+--  -|++-+--
[+, -, -]=Z  |AAAZZZ  +|++++++  -|++-+--  -|++-+--
[-, -, -]=N  |CCCIII  -|------  -|++-+--  -|++++++

No
?- swf(F,rights([(a,b)->1,(a,c)->J,(b,c)->K])),display_swf_t2(F),nl,write([J:K]),fail.

swf: row  col|ACITZN ab|+--++- ac|++-+-- bc|+++---
--------------------------------------------------
[+, +, +]=A  |AAAAAA  +|++++++  +|++++++  +|++++++
[-, +, +]=C  |CCCCCC  -|------  +|++++++  +|++++++
[-, -, +]=I  |IIIIII  -|------  -|------  +|++++++
[+, +, -]=T  |TTTTTT  +|++++++  +|++++++  -|------
[+, -, -]=Z  |ZZZZZZ  +|++++++  -|------  -|------
[-, -, -]=N  |NNNNNN  -|------  -|------  -|------
[1:1]

No
?- 
*/

% a proof of the Paretian-Liberal and the IIA-liberal for weak ordering

/*
?- swf(F,rights([(a,b)->1,(a,c)->2,(b,c)->K])),display_swf_t2(F),nl,write([J:K]).

No
?- chdom(K).

K = l:linear->t:transitive 

Yes
?- swf(F,rights_p([(a,b)->1,(a,c)->2])),display_swf_t2(F).

No
?- swf(F,rights_i([(a,b)->1,(a,c)->2])),display_swf_t2(F).

No
?- 

*/

% an experimentation to deter the almost decisiveness

/*

?- swf(F,na_decisive([i])),display_swf_t2(F),fail.

swf: row  col|ABCFIJOSTWZnN ab|+0---+0-+++0- ac|+++0-+0-+0--- bc|+++++000-----
--------------------------------------------------
[+, +, +]=A  |OOOOOOOOOOOOO  +|0000000000000  +|0000000000000  +|0000000000000
[0, +, +]=B  |OOOOOOOOOOOOO  0|0000000000000  +|0000000000000  +|0000000000000
[-, +, +]=C  |OOOOOOOOOOOOO  -|0000000000000  +|0000000000000  +|0000000000000
[-, 0, +]=F  |OOOOOOOOOOOOO  -|0000000000000  0|0000000000000  +|0000000000000
[-, -, +]=I  |OOOOOOOOOOOOO  -|0000000000000  -|0000000000000  +|0000000000000
[+, +, 0]=J  |OOOOOOOOOOOOO  +|0000000000000  +|0000000000000  0|0000000000000
[0, 0, 0]=O  |OOOOOOOOOOOOO  0|0000000000000  0|0000000000000  0|0000000000000
[-, -, 0]=S  |OOOOOOOOOOOOO  -|0000000000000  -|0000000000000  0|0000000000000
[+, +, -]=T  |OOOOOOOOOOOOO  +|0000000000000  +|0000000000000  -|0000000000000
[+, 0, -]=W  |OOOOOOOOOOOOO  +|0000000000000  0|0000000000000  -|0000000000000
[+, -, -]=Z  |OOOOOOOOOOOOO  +|0000000000000  -|0000000000000  -|0000000000000
[0, -, -]=n  |OOOOOOOOOOOOO  0|0000000000000  -|0000000000000  -|0000000000000
[-, -, -]=N  |OOOOOOOOOOOOO  -|0000000000000  -|0000000000000  -|0000000000000

No
?- swf(F,na_decisive([p])),display_swf_t2(F),fail.

No
?- 

*/

%---- end