/************************************************************
  Computing social welfare functions and distributing rights
  program: cswf07.pl
  language: prolog
  date: 2006.12.14.-21,24.( cswf06.pl)
  revised: 2007.10.29-31.
  creator: Kenryo INDO
************************************************************/
% load preference generator if r/1 does not exist.
:- (\+ clause(r(_),_)->[gprf06];true).
%:- dynamic r/1, domain_type/1.
:- (\+ clause(all_r(_),_)->assert((all_r(L):- findall(Q,r(Q),L)));true).
% set the initial domain.
:- chdom(_->l:linear),display_domain.

% 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
%  SWF is a function which decides a social ordering for each profile.
% In Arrow's theorem, which derives only dictatorial rules, 
% the following conditions are assumed:
% the iia condition and the Pareto condition, as well as  
% the tansitivity and unrestrictedness for orderings 
% both in the domain and region of SWF. And the theorems 
% which generalize Arrow's theorem modifies some of these conditions.

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).

axiom_swf(dict(J),RR->Q,_):- r(Q),dictator(J,[RR->Q]).
axiom_swf(sdict(J),RR->Q,_):- r(Q),dictator_s(J,[RR->Q]).
axiom_swf(adict(J),RR->Q,_):- r(Q),ad(J,[RR->Q]).

% revised: 29-31 Oct 2007
% earlier code is not correct except for linear ordering.
% Specifically, the code of iia was too loose.

% dictatorship
dictator(J,F):- j(J),\+ (member(PP->R,F),r_j(J,PP,P),opposite(s,_,[R,P])).
dictator_s(J,F):-j(J),\+ (member(PP->R,F),r_j(J,PP,P),opposite(_,_,[R,P])).

% Pareto condition
pareto(RR->R):- \+ (dop(XY),opposite(s,XY,[R|RR])).
pareto_w(RR->R):- \+ (dop(XY),opposite(-,XY,[R|RR])).
pareto_s(RR->R):- \+ (dop(XY),opposite(+,XY,[R|RR])).

% Independence of irrelevant alternatives (IIA)
iia(RR->R,F):-
   \+ (member(QQ->Q,F),dop(XY),is_same_profile_for_dop(XY,RR,QQ),opposite(_,XY,[R,Q])).

is_same_profile_for_dop(_,[],[]).
is_same_profile_for_dop(XY,[R|P],[S|Q]):-
   is_same_profile_for_dop(XY,P,Q),\+ opposite(_,XY,[R,S]).

debug_iia(RR->R,QQ->S,XY,A):- nl,write(RR->R;QQ->S;[XY];A).

agree(_,_,[]).
agree(s,XY,[Q|R]):- agree(s,XY,R),p(XY,Q).
agree(+,XY,[Q|R]):- agree(+,XY,R),r(XY,Q).
agree(-,XY,[Q|R]):- agree(-,XY,R),\+ r(XY,Q).
%agree(0,XY,[Q|R]):- agree(0,XY,R),i(XY,Q).

opposite(_,_,[]).
opposite(A,XY,[Q|R]):- A==s,agree(s,XY,R),\+ p(XY,Q).
opposite(+,XY,[Q|R]):- agree(+,XY,R),\+ r(XY,Q).
opposite(-,XY,[Q|R]):- agree(-,XY,R),r(XY,Q).
% deviator in a profile 
opposite(+,J,XY,QQ):- agree(-,XY,QL),r_j(-J,QQ,R,QL),r(XY,R). 
opposite(-,J,XY,QQ):- agree(+,XY,QL),r_j(-J,QQ,R,QL),\+ r(XY,R).

% Other important conditions for social orderings

% 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(s,_,[R,P])).

% 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]).

% distribution of rights among individuals

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

% almost decisiveness (with a detector)

a_decisive(XY,J,[P,Q]->S):-
   member(J:R:U,[1:P:Q,2:Q:P]),
   (opposite(_,XY,[R,U])-> \+ opposite(_,XY,[R,S]);true).

% deter the almost decisiveness 

na_decisive(L,RR->Q,F):-
   subset(L,[p,i]),
   \+ a_decisive(_,_,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)).


%  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)

/*

?- swf(F,dict(J)),nl,display_swf(F),fail.


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

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

No
?- swf(F,arrow),nl,display_swf(F),fail.


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

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

No
?- chdom(A).

A = l:linear->t:transitive 

Yes
?- swf(F,dict(J)),nl,display_swf(F),fail.


swf:row  col |ABCFIJOSTWZnN
--------------------
[+, +, +]=A  |AAAAAAAAAAAAA
[0, +, +]=B  |BBBBBBBBBBBBB
[-, +, +]=C  |CCCCCCCCCCCCC
[-, 0, +]=F  |FFFFFFFFFFFFF
[-, -, +]=I  |IIIIIIIIIIIII
[+, +, 0]=J  |JJJJJJJJJJJJJ
[0, 0, 0]=O  |OOOOOOOOOOOOO
[-, -, 0]=S  |SSSSSSSSSSSSS
[+, +, -]=T  |TTTTTTTTTTTTT
[+, 0, -]=W  |WWWWWWWWWWWWW
[+, -, -]=Z  |ZZZZZZZZZZZZZ
[0, -, -]=n  |nnnnnnnnnnnnn
[-, -, -]=N  |NNNNNNNNNNNNN

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

No
?- swf(F,arrow),nl,display_swf(F),fail.


swf:row  col |ABCFIJOSTWZnN
--------------------
[+, +, +]=A  |AAAAAAAAAAAAA
[0, +, +]=B  |BBBBBBBBBBBBB
[-, +, +]=C  |CCCCCCCCCCCCC
[-, 0, +]=F  |FFFFFFFFFFFFF
[-, -, +]=I  |IIIIIIIIIIIII
[+, +, 0]=J  |JJJJJJJJJJJJJ
[0, 0, 0]=O  |OOOOOOOOOOOOO
[-, -, 0]=S  |SSSSSSSSSSSSS
[+, +, -]=T  |TTTTTTTTTTTTT
[+, 0, -]=W  |WWWWWWWWWWWWW
[+, -, -]=Z  |ZZZZZZZZZZZZZ
[0, -, -]=n  |nnnnnnnnnnnnn
[-, -, -]=N  |NNNNNNNNNNNNN

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

No
?- chdom(A).

A = t:transitive->l:linear 

Yes
?- 

?- [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): 0.797

F = _G157
T = 0.797

Yes
?- stopwatch((swf(F,wilson),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  |NNNNNN  +|------  +|------  +|------
[-, +, +]=C  |ZZZZZZ  -|++++++  +|------  +|------
[-, -, +]=I  |TTTTTT  -|++++++  -|++++++  +|------
[+, +, -]=T  |IIIIII  +|------  +|------  -|++++++
[+, -, -]=Z  |CCCCCC  +|------  -|++++++  -|++++++
[-, -, -]=N  |AAAAAA  -|++++++  -|++++++  -|++++++

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  -|+--++-  -|++-+--  -|+++---
% time elapsed (sec): 17.078

F = _G160
T = 17.078 

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): 3.75

F = _G157
T = 3.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.0320001

F = _G160
T = 0.0320001

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
?- chdom(A).

A = l:linear->t:transitive 

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

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

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_i([(a,b)->1,(a,c)->2])).

No
%
% The following query consumes time. 
%
?- swf(F,rights_p([(a,b)->1,(a,c)->2])).

No
?- 

*/

% an experimentation to deter the almost decisiveness
% (earlier code has a bug)

/*

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

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

No
?- 

*/

%---- end