% subset relation
A=<B, B=<C -> A=<C.
A=<A.
A=<B,B=<A -> A=B.

% greatest lower bounds
in(A,S) -> glb(S)=<A.
all(A,in(A,S)=>B=<A) -> B=<glb(S).

% least upper bounds
%in(A,S) -> A=<lub(S).
%all(A,in(A,S)=>A=<B) -> lub(S)=<B.

% f is monotone
A=<B -> f(B)=<f(A).

% properties are sets
prop(P,A) -> in(A,P).
in(A,P) -> prop(P,A).

% Tarksi's Fixpoint Theorem
tarski == (exists(X,f(X)=X) and all(Y,f(Y)=Y => X=<Y)).

goal
	~tarski.

% property 'O' is the set of pre-fixpoints of f
%prop('P',A) -> (A=<f(A)).
%A=<f(A) -> prop('P',A).
%prop('O',A) -> (f(A)=<A).
%f(A)=<A -> prop('O',A).
prop('F',A) -> (f(A)=A).
f(A)=A -> prop('F',A).




% this precedence yields a faster proof
precedence([prop,in,f]).

%:-option(iterative_saturation(on)).