:- use_module(library(lists)).

:- op(400,fy,-),
   op(100,fy,transfer),
   op(650,xfy,->),
   op(600,xfy,and),
   op(610,xfy,or),
   op(700,xfy,<).

/* formula
   true if Fml is the formula equivalent to the rule R_{n,m} of the
   sequent calculus for Lewis' conditional logic V
   Implemented for N,M > 0
*/
formula(N,M,Fml) :-
    conclusion(N,M,Fml1),
    substitute(Fml1,N,M,Fml).


/* substitute
   true if the first argument substituted by the substitution given by
   rule R_{N,M} yields the last argument
*/
substitute((Fml1 and Fml2), N,M, (Fml3 and Fml4)) :-
    substitute(Fml1,N,M,Fml3),
    substitute(Fml2,N,M,Fml4).
substitute((Fml1 or Fml2), N,M, (Fml3 or Fml4)) :-
    substitute(Fml1,N,M,Fml3),
    substitute(Fml2,N,M,Fml4).
substitute((Fml1 -> Fml2), N,M, (Fml3 -> Fml4)) :-
    substitute(Fml1,N,M,Fml3),
    substitute(Fml2,N,M,Fml4).
substitute((Fml1 < Fml2), N,M, (Fml3 < Fml4)) :-
    substitute(Fml1,N,M,Fml3),
    substitute(Fml2,N,M,Fml4).
substitute(a(I),N,M,(Prem -> a(I))) :-
    premiss(N,M,Prem).
substitute(b(I),N,M,(Prem and b(I))) :-
    premiss(N,M,Prem).
substitute(c(J),N,M,(Prem and c(J))) :-
    premiss(N,M,Prem).
substitute(d(J),N,M,(Prem -> d(J))) :-
    premiss(N,M,Prem).

/* premiss /3
   true if the premiss formula for the rule R_{n,m} is Prem
*/
premiss(N,M,Prem1 and Prem2) :-
    premiss_positive(N,M,Prem1),
    premiss_negative(N,M,Prem2).

/* premiss_positive
   true if Prem is the "positive bit" of the premiss formula for the
   rule R_{N,M}, i.e., the formula
   And_{i <= n} (b(i) -> Or_{j <= n} a(j) or Or_{k <= m} d(k))
*/
premiss_positive(N,M,Prem) :-
    premiss_positive_aux(1,N,M,Prem).

premiss_positive_aux(N,N,M,b(N) -> Disj_A or Disj_D) :-
    disjunction(a,1,N,Disj_A),
    disjunction(d,1,M,Disj_D).
premiss_positive_aux(K,N,M,(b(K) -> Disj_A or Disj_D) and Rest) :-
    K < N,
    disjunction(a,1,N,Disj_A),
    disjunction(d,1,M,Disj_D),
    L is K + 1,
    premiss_positive_aux(L,N,M,Rest).

/* premiss_negative
   true if Prem is the "negative bit" of the premiss formula for the
   rule R_{N,M}, i.e., the formula
   And_{i <= k <= m}(c(k) -> Or_{k < l <= m}d(l) or Or_{j <= n} a(j))
*/
premiss_negative(N,M,Prem) :-
    premiss_negative_aux(1,N,M,Prem).

premiss_negative_aux(K,N,M, (c(K) -> Disj_D or Disj_A) and Rest) :-
    K < M,
    L is K + 1,
    disjunction(d,L,M,Disj_D),
    disjunction(a,1,N,Disj_A),
    premiss_negative_aux(L,N,M, Rest).
premiss_negative_aux(M,N,M, (c(M) -> Disj_A)) :-
    disjunction(a,1,N,Disj_A).

/* disjunction /4
   true if K < L and Disj is var(K) or ... or var(L)
*/
disjunction(Var,K,L,Term or Disj) :-
    K < L,
    Term =.. [Var,K],
    M is K + 1,
    disjunction(Var,M,L,Disj).
disjunction(Var,K,K,Term) :-
    Term =.. [Var,K].



/* conclusion
   true if Conc is the conclusion of the rule R_{n,m}, i.e., the
   formula
   c(1) < d(1) and ... and c(m) < d(m) -> a(1) < b(1) or ... or a(n) < b(n)
*/
conclusion(N,M,Conj -> Disj) :-
    concl_conj(1,M,Conj),
    concl_disj(1,N,Disj).
concl_conj(M,M,c(M)<d(M)).
concl_conj(K,M,(c(K)<d(K)) and Rest) :-
    K < M,
    L is K + 1,
    concl_conj(L,M,Rest).
concl_disj(M,M,a(M)<b(M)).
concl_disj(K,M,(a(K)<b(K)) or Rest) :-
    K < M,
    L is K + 1,
    concl_disj(L,M,Rest).



