% Explanation:
%-------------
% The following series of experiments aims at showing
% that the ordered pair notion, as defined by J.T. Schwartz,
% indeed meets the formal properties which truly count
% due (which of course other pair notions, such as the
% classical one to K. Kuratowski, would satisfy too). The 
% interest of this notion lies in the fact that it relies on 
% axioms which are different from those ensuring "correctness"
% of Kuratowski's pairing notion. In particular, the regularity
% axiom enters into play --- extensionality, on the other
% hand, is not needed)

% Italian translation:
%---------------------
% Questa serie di esperimenti e` tesa a dimostrare che
% la coppia ordinata, come definita da J.T. Schwartz,
% soddisfa le proprieta` formali che davvero contano,
% che anche altre nozioni di coppia (ad es. quella,
% classica, di  K. Kuratowski) soddisfebbero ugualmente.
% Il pregio di questa nozione e` di impegnare assiomi
% diversi (regolarita`, in particolare --- non serve,
% invece, l'estensionalita`) da quelli necessari per
% dimostrare la "correttezza" della nozione di coppia di
%  Kuratowski, verificata in altra sede.

set(auto).

% e/2 designated membership
% 0/0 designates the null set
% a/1 designates arbitrary selection
% w/2 designates single element adjunction
% l/2 designates single element removal
% the ordered pair construction is:
%	w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
% its associated projections are:
%	a(a(p))
% and
%	a(a(
%		 l(
%		 a(l( p
%		   ,a(p)
%		 )),
%		 a(p)
%		 )))

assign(max_seconds,32700).

include(boolean). % "breadth" of membership
include(nesting). % "depth" of membership 
%include(exten).   % extensionality, part 1
%include(xtens).   % extensionality, part 2
include(regul).   % regularity
%include(pow).     % powerset
%include(trans).   % transitive closure
%include(union).   % unionset
%include(choice).  % the most controversial of all axioms of set theory
%include(infty).   % antithetic to the finiteness group "fty" of axioms
%include(fty).   % antithetic to the infinity group "infty" of axioms

formula_list(usable).

( all y x ( -( y = x ) -> 		% a
		e(y,l(  w(w(0,y),x)
			  ,	     x
		   ))
) ). % 14.5s

( all z y ( a(w(w(0,z),y)) = y | a(w(w(0,z),y)) = z ) ). % b, ca. 30.0s

( all z y x ( e(z,y) -> -( a(w(w(x,z),y)) = y ) ) ). % c, ca. 1.1s

%%( all y z x ( e(y,z) -> -( a(w(w(x,z),y)) = z ) ) ). % b', inessential hint, less than 2.0s

( all y z ( e(y,z) -> a(w(w(0,z),y)) = y ) ). % d, ca. 0.2s with b', 95.0s without it

( all z y x ( e(z,l(  w(w(0,y),x)
			  ,		 x
		   )) ->
			   	 z = y
) ). % e, less than 0.3s

( all z y x ( e(z,l(  w(w(0,w(y,x)),x)
			 ,a(w(w(0,w(y,x)),x))
		   )) ->
			      z = w(y,x)
) ). % f, less than 12.0s

( all y x ( -( w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x)) = w(w(0,x),x) ) ) ). % g, 0.1s

( all y x (   a(w(w(0,w(w(0,y),x)),x)) = x ) ). % h, less than 0.1s

( all x y (
   exists z ( e(z,  w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
	   & -( z = a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))) )
) ) ). % i, 0.5s

%( all x y z ( exists t ( e(z,x) & -( z = a(x) ) -> e(t,l(x,a(x))) ) ) ). % j, 0.2s

%( all x y (
%   exists z ( e(z,l(   w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
%			  ,a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
%		   ))
%) ) ). % k, 0.55s

( all x y ( e(a(l(   w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
			,a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		   )),l( w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
			,a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		   ))
) ). % l, 0.77s

( all y x (
	-( w(w(0,w(0,y)),y) = w(w(0,x),x) )
) ). % m, less than 2.0s

%% TO QUICKLY OBTAIN THE FOLLOWING, ONE SHOULD INHIBIT EARLIER STEPS j AND k
%% THEY WILL REMAIN INACTIVATED FROM NOW ON

( all y x ( a(l( w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
		  ,a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		   ))    = w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))
) ). % n, less than 0.5s

( all z y x ( e(z,l(
		 a(l( w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
		   ,a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 )),
		 a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 )) -> z = w(w(0,w(0,y)),y)
) ). % o, less than 2.0s

%% TO OBTAIN THE FOLLOWING, WE MOMENTARILY INHIBIT include(nesting)

( all y x ( e(    w(w(0,w(0,y)),y),l(
		 w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x)),
		 w(w(0,x),x)
		 ))
) ). % p, less than 0.5s

%% HENCEFORTH include(nesting) IS ACTIVATED AGAIN

( all y x ( e(w(w(0,w(0,y)),y),l(
		 a(l( w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
		   ,a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 )),
		 a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 ))
) ). % q, less than 1.0s

( all y x ( e(a(
		 l(
		 a(l( w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
		   ,a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 )),
		 a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 ))
		,l(
		 a(l( w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
		   ,a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 )),
		 a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 ))
) ). % r, less than 2.0s

( all y x ( a(
		 l(
		 a(l( w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
		   ,a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 )),
		 a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 )) =		   w(w(0,w(0,y)),y)
) ). % s, less than 2.0s

% the following two propositions state that cdr(cons(X,Y))=Y, car(cons(X,Y))=Y

( all y x ( a(a(
		 l(
		 a(l( w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
		   ,a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 )),
		 a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x)))
		 ))) =	y
) ). % t, less than 2.0s

( all y x ( a(a(w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))))
	= x ) ). % u, less than 0.1s

% the following two propositions state that cons(X,Y)=cons(Z,V)->X=Z&Y=V; they
% should readily follow from the last preceding two, but they confused Otter

%( all y x v z ( w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
%		  = w(w(0,w(w(0,w(w(0,w(0,v)),v)),w(w(0,z),z))),w(w(0,z),z))
%->
%	x = z
%) ). % v, less than 1.0s

%( all y x v z ( w(w(0,w(w(0,w(w(0,w(0,y)),y)),w(w(0,x),x))),w(w(0,x),x))
%		  = w(w(0,w(w(0,w(w(0,w(0,v)),v)),w(w(0,z),z))),w(w(0,z),z))
%->
%	y = v
%) ). % w, less than 1.0s

end_of_list.