:- 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,<).

generate_lewis(1,(a+1 < a+1)).
generate_lewis(N, (Disjunction or (Last < a+1 )) ) :-
  listAtoms(1,N,Atoms),
  find_last(Last,Atoms),
  orFormula(Atoms,Disjunction).

listAtoms(N,N,[a+N]).
listAtoms(M,N,[a+M|L]) :-
  M1 is M+1,
  listAtoms(M1,N,L).

orFormula([A1|[A2|[]]],(A1 < A2)).
orFormula([A1|[A2|T]],((A1 < A2) or F)) :-
  orFormula([A2|T],F).

find_last(X,[X]).
find_last(X,[_|Z]) :- find_last(X,Z).

generate_tr(1, (a+1 < a+1)).
generate_tr(N, ((Conjunction) -> (a+1 < Last) )) :-
  listAtoms(1,N,Atoms),
  find_last(Last,Atoms),
  andFormula(Atoms,Conjunction).

andFormula([A1|[A2|[]]],(A1 < A2)).
andFormula([A1|[A2|T]],((A1 < A2) and F)) :-
  andFormula([A2|T],F).

generate_or(1,(a+1 < a+1)).
generate_or(N, Formula) :-
  listAtoms(1,N,Atoms),
  orAtoms(Atoms,Disjunction),
  orCycle(Atoms,Disjunction,Formula).

orAtoms([A|[]],A).
orAtoms([A|T],(A or F)) :-
    orAtoms(T,F).

orCycle([A|[]],D,(A < D) ).
orCycle([A|T],D,((A < D) or Formula ) ) :-
  orCycle(T,D,Formula).


