% problem-set/pelletier/p43.clauses
% created : 07/25/86
% revised : 08/17/89

% description:
%
% Full Predicate Logic (without Identity and Functions)..
%             - De Champeaux, 1979..
% Define set equality ('Q') as having exactly the same members. Prove.
% set equality is symmetric..
% (Ax)(Ay)(Qxy <-> (Az)(Fzx <-> Fzy)).
% ----------------------------------.
%    (Ax)(Ay)(Qxy <-> Qyx).

% representation:
%
% declare_predicates(2,[Q,F]).
% declare_variables([x,y,z]).


% premise
(all x all y (Q(x,y) <-> (all z (F(z,x) <-> F(z,y))))).

% denial of the conclusion
-(all x all y (Q(x,y) <-> Q(y,x))).