Print[":Package Title: goedel73.27c             2005 September 27 at 4:55 p.m. "];

(*
   :Context: Goedel` 
   :Author: Johan G. F. Belinfante
   :Collaborators: Tiffany D. Goble, Claudia D. Huang

   :Summary:
   The GOEDEL program implements Goedel's algorithm for class formation, 
   with some modifications made to avoid assuming the axiom of regularity, 
   and Kuratowski's construction of ordered pairs.  

   :Copyright:   2001 by Johan G. F. Belinfante
   :Mathematica Version: 3.0                    
*)

(* :History: 
   Version goedel73.27b plus rules derived in EXAMPLES.NB and LUB-FU.NB
  
   Earlier versions go back to 1996.
*)

(* :Keywords: class, member *)

(* :Sources:
   Kurt Goedel, 1939 monograph on the consistency of the
   axiom of choice and of the generalized continuum hypothesis.  
*)

(* :Warnings:
   <description of global effects, incompatibilities>

    count is an unprotected global counter used in the test suites
 
    0 is used to represent the empty set.

    E is used to represent the membership relation.
*)

(* For debugging sometimes the following may be useful:    *)
(* $IterationLimit = $RecursionLimit = 20;                 *)

(* :Limitations:
   <special cases not handled, known problems>

   The simplification rules are not confluent.  It is unknown whether 
   a Knuth Bendix completion of the present rules would terminate.  
   Probably not.  The order in which simplification rules are applied
   is therefore important, but no mechanism has been included
   for user control over this order.

   Mathematica's builtin Tracing commands are the only mechanism
   for discovering what rules were actually applied.  In one of
   the earlier versions we had built in a mechanism for documenting
   which rules had been accessed, but this proved to be of limited
   value.    
*)

(* :Discussion:
   <description of algorithm, information for experts>

   See Goedel's monograph, pages 10-14.
*)

(* :Requirements:

*)

(* :Examples:
   <sample input that demonstrates the features of this package>

   Sample files are available in various test suites.
*)

(* set up the package context, including public imports *)

BeginPackage["Goedel`"]

(* added 2003 June 25 *)
Unprotect[E]; Clear[E];

(* usage messages for the exported functions and the context itself *)

Goedel::usage = "Goedel.m is a package that implements a modification
                 of Goedel's algorithm for class formation."

A::usage = "A[x] is the class obtained by intersecting all the
 sets that belong to x"

Aclosure::usage = "Aclosure[x] is the class of all sets A[y] where y is a
 nonempty subset of x"

ACLOSURE::usage = "ACLOSURE is the function that takes x to image[BIGCAP,P[x]]"

ACYCLIC::usage = "ACYCLIC is the class of all relations that contain no cycles"

ADJOIN::usage = "ADJOIN[x] is the function that takes y to union[x,y]."

and::usage = "and[x,y,...]  is a flat, orderless function of any number of variables"

ANTISYM::usage = "ANTISYM is the class of all antisymmetric relations"

ANTISYMMETRIC::usage = "ANTISYMMETRIC[x] is the statement that x is an
 antisymmetric relation"

apply::usage = "apply[x,y] was used by Quaife to apply a function to its argument"

APPLY::usage = "APPLY[x,y] is useful for applying a function to its argument"

assert::usage = "assert[p] is a statement equivalent to p obtained by applying Goedel's algorithm to class[w,p].
 Applying assert repeatedly sometimes simplifies a statement."

ASSOC::usage = "ASSOC is the function that reassociates ordered triples"

associative::usage = "associative[x] is the statement that x is an associative relation"

ASSOCIATIVE::usage = "ASSOCIATIVE is the class of all associative relations"

axch::usage = "axch is a flag for a set form of the axiom of choice"

AxCh::usage = "AxCh is a flag that can be set equal to True if one is assumes the class form of the axiom of choice.  Not protected."

AxReg::usage = "AxReg is a flag that can be set equal to True if one assumes the axiom of regularity.  Not protected."

BIGCAP::usage = "BIGCAP is the function that takes x to A[x]"

BIGCUP::usage = "BIGCUP is the function that takes x to U[x]"

BIJ::usage = "BIJ is the class of one-to-one correspondences"

binclosed::usage = "binclosed[x] is the class of sets y that are closed under a binary operation x"

cantor::usage = "Quaife introduced cantor[x] to prove Cantor's theorem"

CAP::usage = "CAP is the function that takes pair[x,y] to
 intersection[x,y]"

CAPclosed::usage = "CAPclosed is the class of sets which are closed under binary intersection"

card::usage = "card[x] is the intersection of all ordinals equipollent to x"

CARD::usage = "the function CARD takes x to card[x] when both are sets"

cart::usage = "cart[x,y] is the cartesian product of x and y.
 Note that cart is not associative."

CART::usage = "CART is the function that takes pair[x,y] to cart[x,y]"
 
CATOFUNS::usage = "CATOFUNS is the binary composition for the category of sets (mappings)"
 
CATORELN::usage = "CATORELNS is the binary composition for the category of relations"

CHOICE::usage = "the choice function takes each nonempty set x to
 some member of x.  To use it, one needs to assign True to AxCh"

choicefunction::usage = "choicefunction[f,x] is the statement that f is a choice function with domain x"

class::usage = "class[x,p] applies Goedel's algorthm to the class of all sets x 
 satisfying the condition p.  The variable x may be an atomic variable, or 
 of the form pair[u,v], where u and v in turn can be pairs, etc. "

cliques::usage = "cliques[x] is the class of all w such that
 cart[w,w] is contained in x"

CLIQUES::usage = "CLIQUES is the function that takes x to cliques[x]"

COARSER::usage = "pair[x,y] belongs to COARSER if x is a subset of y and U[x] = U[y]"

commutant::usage = "commutant[x] is the class of all sets which commute with x"

commute::usage = "commute[x,y] is true if and only if the composite of
 x and y is the same as the composite of y and x"

COMMUTE::usage = "COMMUTE is the class of pair[x,y] such that x and y commute"

COMPACT::usage = "COMPACT is the class of all t such that for every set coarser than t
 there is a finite set that is even coarser"

complement::usage = "complement[x] is the class of all sets that
 to not belong to x"

COMPOSE::usage = "COMPOSE is the function that takes pair[x,y]
 to composite[x,y]"

composite::usage = "composite[x,y,...]  is a flat function of any number
 of variables"
 
cond::usage = "cond is a flag for the thin conditional rules"

core::usage = "core[x,y] is the union of all subsets of y that belong to x"

CORE::usage = "CORE[x] is the function that takes u to the union of all
 subsets of v that belong to x"

count::usage = "count is a global variable used in the test suites"

COUNTABLE::usage = "COUNTABLE is the class of sets that are finite or denumerable"

cross::usage = "cross[x,y] is the cross product of x and y"

CROSS::usage = "CROSS is the function that takes pair[x,y]
 to cross[x,y]"

CUP::usage = "CUP is the function that takes pair[x,y] to union[x,y]"

CUPclosed::usage = "CUPclosed is the class of sets which are closed
 under binary union"

DEDEKIND::usage = "DEDEKIND is the class of Dedekind-finite sets"

DENUMERABLE::usage = "DENUMERABLE is the class of sets whose cardinality is omega"

DESCENDING::usage = "DESCENDING is the class subvar[E] of all sets x
 with the property that for each member v of x, there is a member 
 u of x that belongs to v"

Di::usage = "The diversity relation Di is the class of ordered pairs
 pair[x,y] such that x is not equal to y. "

diag::usage = "Quaife uses diag[x] for our complement[fix[x]]"

dif::usage = "dif[x,y] is the relative complement of y in x"

DIF::usage = "DIF is the function that takes pair[x,y] to 
 intersection[x,complement[y]]"

DIFclosed::usage = "DIFclosed is the class of all sets which are
 closed under set differences"

direct::usage = "direct[x,y] is an abbreviation for the direct product of x and y"

disjoint::usage = "disjoint[x,y] is the statement that x and y are
 disjoint, that is, their intersection is empty."

DISJOINT::usage = "DISJOINT is the class of all pair[x,y] such that
 x and y are disjoint"

DIV::usage = "DIV is the divisibility relation for natural numbers"

domain::usage = "domain[x] is the domain of x"

DORA::usage = "DORA is the function that takes x to pair[domain[x],range[x]"

DUP::usage = "DUP is the function that takes x to pair[x,x]"

E::usage = "E is the membership relation"

empty::usage = "empty[x] is the statement that x is the empty set"

equal::usage = "equal[x,y] is the statement that the classes x and y
 are equal"

equality::usage = "equality is a flag governing equality substitution"

EQUIDIFF::usage = "EQUIDIFF is an equivalence relation on cart[omega,omega]
 used to define the integers"

equiv::usage = "equiv[p,q] is the statement that p and q imply each
 other"

EQUIV::usage = "EQUIV is the function lambda[x, eqv[x]]"

EQUIVALENCE::usage = "EQUIVALENCE[x] is the statement that x is an
 equivalence relation"

EQV::usage = "EQV is the class of (small) equivalence relations"

eqv::usage = "eqv[x] is the symmetric part of trv[x]"

example::usage = "example[n_,string_,comment_] is used in the test
 suites"

exists::usage = "exists[x,y,...,p] is the statement that there
 exist x,y,... such that p"
 
FACTORIAL::usage = "FACTORIAL is the factorial function for natural numbers"

FINITE::usage = "the class of finite sets"

first::usage = "first[x] is the first argument of an ordered pair"

FIRST::usage = "FIRST is the function which takes pair[x,y] to y"

fix::usage = "the fixed point class fix[x] is the class of 
 all y such that pair[y,y] belongs to x"

FIX::usage = "FIX is the function that takes x to fix[x]"

flags::usage = "flags shows values of all flags"

flip::usage = "flip[x] is the class of all pair[pair[u,v],w]
 such that pair[pair[v,u],w] belongs to x"

forall::usage = "forall[x,y,...,p] is the statement that p holds
 for all sets x,y,..."

full::usage = "full[x] is the statement that every member of x is
 a subset of x"

FULL::usage = "FULL is the class of all full sets."

FUNCTION::usage = "FUNCTION[x] is the statement that x is a function"

funpart::usage = "funpart[x] is the functional part of x"

FUNPART::usage = "FUNPART is the function that takes x to funpart[x]"

FUNS::usage = "FUNS is the class of all functions whose domains are sets"
 
GLB::usage = "member[pair[x,y],GLB[z]] means y is a greatest lower bound for x
 with respect to the relation z"

greatest::usage = "greatest[x,y] is the set of x-greatest elements of y"
 
GREATEST::usage = "member[pair[x,y],GREATEST[z]] means y is a greatest element of x
 with respect to the relation z"

H::usage = "H[x] is Jech's hereditarily functor"

HC::usage = "HC in the function that takes x to H[x]"

history::usage = "history[x,y] is the history of x with respect to y"

HISTORY::usage = "HISTORY[x,y] is a shorthand for an expression equal to history[x,y]"

hull::usage = "hull[x,y] is the intersection of all sets belonging to x that contain y"
 
HULL::usage = "HULL[x] is the function that takes u to the intersection of all
 sets that contain u and belong to x"

Id::usage = "Id is the identity relation"

id::usage = "id[x] is the restriction of the identity relation to x"

IDEM::usage = "IDEM is the class of idempotent relations"

idempotent::usage = "idempotent[x] is the statement that x = composite[x,x]"

IDP::usage = "IDP is a shorthand for IMAGE[DUP]"

image::usage = "image[x,y] is the image of the class y under x"

IMAGE::usage = "IMAGE[x] is the function that takes y to image[x,y].
 When x is a set, the function IMAGE[x] is a proper class."

IMG::usage = "IMG is the function that takes pair[x,y] to image[x,y]"

implies::usage = "implies[x,y] is the statement that x implies y"

INDUCTIVE::usage = "INDUCTIVE[x] is the statement that x is an
 inductive class"

intadd::usage = "intadd[x,y] is the sum of of integers x and y"

INTADD::usage = "member[pair[pair[x,y],z],INTADD] holds if x and y are integers
 and  x + y = z"

intersection::usage = "intersection[x,y,...]  is a flat, orderless 
 function of any number of variables"
 
invar::usage = "invar[x] is the class of all sets which are
 invariant under x"

INVAR::usage = "INVAR is the relation consisting all pair[x,y] such
 that y is invariant under x"

invariant::usage = "invariant[x,y] means y is invariant under x"

inverse::usage = "the relation inverse[x] is the inverse of x"

INVERSE::usage = "INVERSE is the function that takes x to inverse[x]"

INVFUN::usage = "INVFUN[x] is the statement that inverse[x] is a function"

iterate::usage = "iterate[x,y] is the relation whose vertical sections are
 the generations produced using x starting with the initial generation y"

K::usage = "K is the cover relation defined as the intersection of PS
 and the complement of composite[PS,PS]"

KURA::usage = "KURA is the function that takes pair[x,y] to Kuratowski's
 construction of an ordered pair"

lambda::usage = "lambda[x,f[x]] is the function which takes x to f[x], and
 lambda[pair[x,y],f[x,y] is the function that takes pair[x,y] to f[x,y], etc."

LAMBHULL::usage = "LAMBHULL is the function that takes x to HULL[x]"
 
lb::usage = "lb[x,y] is the class of all lower bounds for y with respect to
 the relation x"

LB::usage = "member[pair[x,y],LB[z]] means y is an lower bound for x
 with respect to the relation z"
 
least::usage = "least[x,y] is the set of x-least elements of y"

LEAST::usage = "member[pair[x,y],LEAST[z]] means y is a least element of x
 with respect to the relation z"

LEFT::usage = "LEFT[x] is the function which takes y to pair[x,y]"

LeftPairV::usage = "LeftPairV is the function that takes x to pair[V,x]"
 
LISTS::usage = "LISTS is the class of all lists"

LUB::usage = "member[pair[x,y],LUB[z]] means y is a least upper bound for x
 with respect to the relation z"
 
map::usage = "map[x,y] is the class of all functions with domain x and range contained in y"

MAP::usage = "MAP is the function which takes pair[x,y] to map[x,y]"

MAXIMAL::usage = "member[pair[x,y],MAXIMAL[z]] means y is a maximal element 
 of x with respect to the relation z"

member::usage = "member[x,y] is the statement that x belongs to y"
 
MINIMAL::usage = "member[pair[x,y],MINIMAL[z]] means y is a minimal element of x with respect to the relation z"

modulo::usage = "modulo[x] is the function that reduces natural numbers modulo x"

monus::usage = "monus[x,y] is the floored difference of natural numbers nat[natsub[x,y]]"

nat::usage = "nat[x] is x when x is a natural number, and 0 otherwise"

natadd::usage = "natadd[x,y] is the sum of  x  and y  if they are natural numbers"

NATADD::usage = "member[pair[pair[x,y],z],NATADD] holds if x and y are natural numbers and  x + y = z"

natmod::usage = "natmod[x,y] is the remainder when the natural number x is divided by the natural number y"

NATMOD::usage = "NATMOD is the function for the remainder obtained when one natural number is divided by another"

natmul::usage = "natmul[x,y] is the product of  x  and y  if they are natural numbers"

NATMUL::usage = "member[pair[pair[x,y],z],NATMUL] holds if x and y are natural numbers and  x y = z"

natsub::usage = "natsub[x,y] is the difference of  x  and y  if they are natural numbers and  x  is not less than y"

not::usage = "not[p] represents the negation of p"

omega::usage = "omega is the set of all natural numbers"

OMEGA::usage = "OMEGA is the class of all ordinal numbers"

ONEONE::usage = "ONEONE[x] is the statement that x is a one-to-one correspondence"

oopart::usage = "oopart[x] is the one-to-one part of x"

OOPART::usage = "OOPART = lambda[x,oopart[x]]"

or::usage = "or[x,y,...] is a flat, orderless function of any number of variables"

P::usage = "P[x] is the power class of x, that is the class of all subsets of x"

pair::argx = "Warning: pair[-,-] must have exactly 2 arguments"

pair::usage = "pair[x,y] is the ordered pair of x and y."

PAIR::usage = "PAIR[x,y] is the ordered pair of x and y if x and y are sets and otherwise is V"

pairset::usage = "pairset[x,y] = set[x,y] is a shorthand for the union of set[x] and set[y] "

PAIRSET::usage = "PAIRSET is the function that takes pair[x,y] to union[set[x],set[y]]"

PARTIALORDER::usage = "PARTIALORDER[x] is the statement that x is a partial order relation"

partrec::usage = "partrec[x,y] is the class of partial solutions of a recursive definition
 with generator x and relation y"

plus::usage = "plus[x] is the non-negative integer corresponding to the natural number x"

PLUS::usage = "PLUS is the function that takes each natural number to the
 corresponding non-negative integer"

PO::usage = "PO is the class of all partial order relations"

PointClosed::usage = "PointClosed is the class of collections of sets that satsify the
 condition that points are closed"

POWER::usage = "POWER is the function that takes x to P[x]"

power::usage = "power[x] is the relation whose n-th vertical slice is the composite
 of  n  copies of x"

PRIMES::usage = "the set of primes"

PRIMESEQ::usage = "list of all primes in increasing order"

PROJ::usage = "PROJ is the class of all projections, that is, idempotent functions"

propersubclass::usage = "propersubclass[x,y] is the statement
 that x is a subclass of y but not equal to y."

PS::usage = "the proper subclass relation "

PSM::usage = "PSM was used in some old Otter work to define certain functions"

Q::usage = "the equinumerosity relation"

range::usage = "range[x] is the range of x"

rank::usage = "rank[x] is the rank of x in the Zermelo-von Neumann 
 cumulative hierarchy"

RANK::usage = "RANK is the function which assigns rank[x] to x"

RC::usage = "RC[x] is the function which takes any set y to its
 relative complement with respect to x"

RCF::usage = "RCF is the function which takes any set x to RC[x]"

rec::usage = "rec[x,y] is the union of the class of partial solutions of a recursive definition
 with generator x and relation y"

RECTANGLE::usage = "RECTANGLE[x] is the predicate that x is a 
 cartesian product"

REFLEXIVE::usage = "REFLEXIVE[x] is the predicate that x is a reflexive 
 relation"

REGULAR::usage = "REGULAR is the class of all regular sets"

restrict::usage = "restrict[z,x,y] is the intersection of z and cart[x,y]"

RESTRICT::usage = "RESTRICT is the restriction relation"

RFX::usage = "RFX is the class of all (small) reflexive relations"

rfx::uage = "rfx[x] = core[RFX,x] is the reflexive core of  x"

RIF::usage = "RIF is a rotation-invariant function"

RIGHT::usage = "RIGHT[x] is the function which takes y to pair[y,x]"

RightPairV::usage = "RightPairV is the function that takes x
 to pair[x,V]"

ROT::usage = "ROT is the function which rotates ordered triples"

rotate::usage = "rotate[x] is the class obtained from x by
 rotating all ordered triples"

RS::usage = "RS[x] is the class of all small restrictions of x"

RUSSELL::usage = "RUSSELL is the class of all x that do not
 belong to themselves"

S::usage = "S is the subset relation"

second::usage = "second[x] is the second argument of an ordered pair"

SECOND::usage = "SECOND is the function that maps pair[x,y] to y"

SELECT::usage = "SELECT is the class of sets that admit cross-sections"

set::usage = "set[x,y,z, ... ] is the set whose only members are x, y, z, ... ,
 if these are indeed sets."
 
setpart::usage = "setpart[x] is x when x is a set, and 0 when x is not a set"

simplify::usage = "simplify is a flag that can be used to turn off certain rules"

singleton::usage = "singleton[x] = set[x] is the set whose only member is x.  
 It is the empty set if x is a proper class"

SINGLETON::usage = "SINGLETON is the the function that takes
 x to set[x]"

singlevalued::usage = "singlevalued[x] is one version of the statement that x is singlevalued"

SINGVAL::usage = "SINGVAL[x] is another version of the statement that x is singlevalued"

SMALLER::usage = "SMALLER is the strict numerical dominance relation"

subclass::usage = "subclass[x,y] is the statement that x is contained in y"

subcommutant::usage = "subcommutant[x] is the class of all y such that
 subclass[composite[x,y],composite[y,x]]" 

subcommute::usage = "subcommute[x,y] is an abbreviation for the condition
 subclass[composite[x,y],composite[y,x]]" 

SUBCOMMUTE::usage = "SUBCOMMUTE is the class of pair[x,y] such that subcommute[x,y]"

subvar::usage = "subvar[x] is the class of all sets y which satisfy the condition subclass[y,image[x,y]] "

SUBVAR::usage = "SUBVAR is the function which takes x to subvar[x]"

subvariant::usage = "subvariant[x,y] means y is subvariant under x"

succ::usage = "succ[x] is the union of x and set[x]"

SUCC::usage = "SUCC is the function that takes x to succ[x]"

SWAP::usage = "SWAP is the function that takes pair[x,y]
 to pair[y,x]"

SYM::usage = "SYM is the class of all (small) symmetric relations"

SYMDIF::usage = "SYMDIF is the symmetric difference function"

symdif::usage = "symmdiff[x,y] is the symmetric difference of x and y"

SYMMETRIC::usage = "SYMMETRIC[x] is the statement that x is a symmetric 
 relation"

T1::usage = "T1 holds all collections of sets satisfying the T1 separation condition in topology"

T2::usage = "T2 holds all collections of sets satisfying the T2 separation condition in topology"

tc::usage = "tc[x] is the transitive closure of x"

TC::usage = "TC is the transitive closure operator"

thin::usage = "thin[x] is the statement that all vertical cross sections of  x  are sets"

thinpart::usage = "thinpart[x] is the largest thin relation obtainable as a restriction of x"

times::usage = "times[x] is the function that multiplies natural numbers by x"

TO::usage ' "TO is the class of all small total order relations"

TOPS::usage = "TOPS is the class of all topologies"

TOTALORDER::usage = "TOTALORDER[x] is the statement that x is a total ordering"

TRANSITIVE::usage = "TRANSITIVE[x] is the statement that x is a transitive relation"

transvar::usage = "transvar[x,y] is the class of all sets z for which image[x,z] is contained in image[y,z]"

transvariant::usage = "transvariant[x,y,z] is the statement that image[x,z] is contained in image[y,z]"

trv::usage = "trv[x] is the least transitive relation which contains composite[Id,x]"

TRV::usage = "TRV is the class of (small) transitive relations"

twist::usage = "twist[x] is the class obtained from x by replacing
 all pair[pair[t,u],pair[v,w]] in x by switching u and v "

TWIST::usage = "TWIST is a function that converts cart to cross"

U::usage = "U[x] is the sum class of x, that is the union of
 all the sets that belong to the class x"
 
ub::usage = "ub[x,y] is the class of all upper bounds for y with respect to
 the relation x"
 
UB::usage = "member[pair[x,y],UB[z]] means y is an upper bound for x
 with respect to the relation z"

Uclosure::usage = "Uclosure[x] is the class of all sets U[y] where y is 
 a subset of x"

UCLOSURE::usage = "UCLOSURE is the function that takes x to Uclosure[x]"

union::usage = "union[x,y,...]  is a flat, orderless function of any 
 number of class variables"

unsafe::usage = "unsafe is a flag used to turn on rewrite rules that are valid, but considered
 unsafe in because they yield unsatisfactory results for some test suite examples"

V::usage = "the universal class"

VERTSECT::usage = "VERTSECT[z] is the function that maps x to the
 vectical section image[z,set[x]]"

VS::usage = "VS is the function that takes x to composite[VERTSECT[x],id[domain[x]]]"

WELLFOUNDED::usage = "WELLFOUNDED[x] is the statement that x is a (strict) wellfounded relation"

WELLORDER::usage = "WELLORDER[x] is the statement that x is a wellordering"

WF::usage = "WF is the class of all small strict wellfounded relations"

wf::usage = "wf[x] is a generic well-founded relation"

WFPART::usage = "WFPART = lambda[x, wf[x]]"

WO::usage = "WO is the class of all small wellordering relations"

X::usage = "X[x] is the set of cross-sections of x"

XS::usage = "XS is the function lambda[x, X[x]]"

Z::usage = "Z is the set of integers"

ZN::usage = "ZN = composite[Id,U[subcommutant[inverse[E]]]]"

Begin["`Private`"]    (* begin the private context (implementation part) *)

(* definition of auxiliary functions and local (static) variables *)

Month[n_] := Part[{" Jan ", " Feb ", " Mar ", 
                   " Apr ", " May ", " Jun ", 
                   " Jul ", " Aug ", " Sep ", 
                   " Oct ", " Nov ", " Dec "}, n]

PrintDate[] := Module[{date=Date[]},
               Print["It is now:  ",
               Part[date,1],Month[Part[date,2]],Part[date,3]," at ",
	           Part[date,4],":", Part[date,5]]]

PrintDate[]

(* replaced 2002 November 23 based on VARLIST.NB *)
varlist[x_] := {x}

(* replaced 2002 November 23 based on VARLIST.NB *)
varlist[pair[x_,y_]] := Union[Flatten[{x,y} /. pair -> List]]

(* Is the expression x free of all variables which occur in y? *)
allfreeQ[x_,y_] := Apply[And,Map[FreeQ[x,#]&,varlist[y]]]

(* added 2004 June 8 to fix a nuisance with two general equality substitution rules *)
noblanks[x_] := Equal[{},Position[x,Verbatim[Blank[]]]]

(* definition of the exported functions *)

count = 0          (* initialize counter *)
example[n_,string_,comment_] := 
    Module[{t},count++;
               Print["In[",n,"]:= ",string]; 
               If[comment!="",Print[comment]]; Print[""];
               t = Timing[ToExpression[string]];
               Print["Out[",n,"]= ",Part[t,2]];
               Print[""]; Print["Execution time = ",
               Round[Part[t,1]/Second]," Seconds"]; 
               Print["\n"]]

(*    
   Goedel's algorithm for class formation.   
*)

(* Rules that must be assigned before attributes are set. *)

and[p_] := p

(* added 2000 September 13 *)
composite[] := Id               

composite[x_] := composite[Id,x]

intadd[x_] := x

intersection[x_] := x

natadd[x_] := x

(* added 2002 August 29 based on MUL-ZERO.NB *)
natmul[x_] := x

or[p_] := p

union[x_] := x


Attributes[and] = {Flat,Orderless,OneIdentity}

Attributes[composite] = {Flat,OneIdentity}

Attributes[disjoint] = {Orderless}

Attributes[equal] = {Orderless}

Attributes[intadd] = {Flat,OneIdentity,Orderless}

Attributes[intersection] = {Flat,Orderless,OneIdentity}

(* added 2002 July 28 based on ADD-NAT.NB *)
Attributes[natadd] = {Flat,OneIdentity,Orderless}

(* added 2002 August 28-19 based on MUL-SWAP.NB and MULASSOC.NB *)
Attributes[natmul] = {Flat,OneIdentity,Orderless}

Attributes[or] = {Flat,Orderless,OneIdentity}

(* introduced 2005 January 10 in SET.NB *)
Attributes[set] = {Orderless}

Attributes[union] = {Flat,Orderless,OneIdentity}


not[True] := False                         (* Truth Table *)
not[False] := True
not[not[p_]] := p                          (* Double Negation *)
not[or[p_,q_]] := and[not[p],not[q]]       (* DeMorgan Laws *)
not[and[p_,q_]] := or[not[p],not[q]]

and[True,p_] := p                          (* Truth Table *)
and[False,p_] := False
and[p_,p_] := p                            (* Idempotent Law  *)
and[not[p_],p_] := False                   (* Excluded Middle *)
and[p_,or[q_,r_]] := or[and[p,q],and[p,r]] (* Distributive Law *)

or[True,p_] := True                        (* Truth Table *)
or[False,p_] := p
or[p_,p_] := p                             (* Idempotent Law *)
or[not[p_],p_] := True                     (* Dichotomy Law *)
or[p_,and[p_,q_]] := p                     (* Absorptive Law *)

(* An empirical set of simplification rules *)

or[and[p_,q_],and[not[p_],q_]] := q
or[p_,and[not[p_],q_]] := or[p,q]
or[not[p_],and[p_,q_]] := or[not[p],q]
or[and[p_,q_],and[p_,not[q_],r_]] := or[and[p,q],and[p,r]]
or[and[p_,not[q_]],and[p_,q_,r_]] := or[and[p,not[q]],and[p,r]]
or[and[not[p_],q_],and[p_,r_],and[q_,r_]] := or[and[not[p],q],and[p,r]]

(* Rules modified 1998 September 12 *)
or[and[not[p_],r_],and[not[q_],r_],and[p_,q_]] := or[and[p,q],r]
or[and[p_,r_],and[not[q_],r_],and[not[p_],q_]] := or[and[not[p],q],r]
or[and[p_,r_],and[q_,r_],and[not[p_],not[q_]]] := or[and[not[p],not[q]],r]

(* definition of logical equivalence *)
equiv[p_,q_] := and[implies[p,q],implies[q,p]]

(* some predicates *)
propersubclass[x_,y_] := and[subclass[x,y],not[subclass[y,x]]]
singlevalued[z_] := equal[0,fix[composite[inverse[z],complement[Id],z]]]

(* introduced 2004 October 26 in AXCH-AC1.NB *)
class[w_,axch] := Module[{x = Unique[],y = Unique[]},class[w,forall[x,
      implies[not[member[0,x]],exists[y,and[FUNCTION[y],subclass[y,inverse[E]],equal[domain[y],x]]]]]]]

(* introduced 2004 October 26 in AXCH.NB *)
class[w_,AxCh] := class[w,and[FUNCTION[CHOICE],subclass[CHOICE,inverse[E]],
                              equal[domain[CHOICE],complement[set[0]]]]]

(* introduced 2004 December 30 in AXREG.NB *)
class[w_,AxReg] := complement[image[V,complement[REGULAR]]]

(* introduced 2004 March 20 in EQV-WRAP.NB *)
class[z_,EQUIVALENCE[x_]] := Module[{u = Unique[],v = Unique[]},class[z,
      and[TRANSITIVE[x],forall[u,v,implies[member[pair[u,v],x],member[pair[v,u],x]]]]]]


(* basic rules for membership *)

(* 
   Special rule used to avoid assuming axiom of regularity 
   Goedel had used the rule member[x,x] = False.
*)
class[w_,member[x_,x_]] := Module[{y=Unique[]},class[w,
                        exists[y,and[member[x,y],equal[x,y]]]]]


(* Theorems A-1,A-2A and A-2B in A1 *)
class[w_,member[u_,A[x_]]] := Module[{v=Unique[]},class[w,and[member[u,V],
                           forall[v,implies[member[v,x],member[u,v]]]]]]

(* corrected 2001 October 14 *)
class[u_,member[v_,Aclosure[x_]]] := Module[{w=Unique[]},
         class[u,and[member[v,V],exists[w,and[subclass[w,x],
                     equal[v,A[w]]]]]]]

(* added 2003 October 28 based on APPLY.NB; wrapped 2005 August 15 *)
class[u_,member[w_,APPLY[x_,y_]]] := class[u,and[member[w,V],
      not[member[y,image[inverse[x],P[complement[set[w]]]]]]]]

(* membership rule for ASSOC revised 2001 November 15 *)
class[x_,member[y_,ASSOC]] := 
       Module[{u=Unique[],v=Unique[],w=Unique[]},class[x,exists[u,v,w,
              equal[pair[pair[pair[u,v],w],pair[u,pair[v,w]]],y]]]]

(* added 2003 July 1 based on ASSOC.NB *)
class[w_,associative[x_]] := class[w,and[subclass[x,cart[cart[V,V],V]],
      equal[composite[x,cross[x,Id]],composite[x,cross[Id,x],ASSOC]]]]

(* added 2001 December 1 *)
class[u_,member[v_,card[x_]]] := Module[{w=Unique[]},class[u,and[member[v,V],
         forall[w,implies[and[member[w,OMEGA],member[pair[x,w],Q]],member[v,w]]]]]]

class[w_,member[z_,COARSER]] := Module[{x = Unique[],y = Unique[]},
      class[w,exists[x,y,and[equal[z,pair[x,y]],subclass[x,y],
              equal[U[x],U[y]]]]]]                        

class[w_,member[t_,COMPACT]] := Module[{x = Unique[],y = Unique[]},
         class[w,and[member[t,V],forall[x,implies[and[subclass[x,t],subclass[U[t],U[x]]],
         exists[y,and[member[y,FINITE],subclass[y,x],subclass[U[x],U[y]]]]]]]]]

class[w_,member[z_,composite[x_,y_]]] := 
         Module[{u = Unique[],v = Unique[]},class[w,exists[u,v,
         and[equal[z,pair[u,v]],member[pair[u,v],composite[x,y]]]]]]

(* 
   Theorem CO-DF2 in CO2 and Theorems CO-COM-V,CO-1A' 
   and CO-1B' in CO4
*)
class[z_,member[pair[u_,w_],composite[x_,y_]]] := 
         Module[{v = Unique[]},class[z,exists[v,
         and[member[u,V],member[w,V],
         member[pair[u,v],y],member[pair[v,w],x]]]]]

(* added 2004 April 17 *)
class[u_,member[v_,core[x_,y_]]] := Module[{w = Unique[]},
      class[u,exists[w,and[member[w,x],member[v,w],subclass[w,y]]]]]

(* Theorems X-OP-1,X-OP-2 and X-OP-3 in X2 *)
class[z_,member[w_,cross[x_,y_]]] := 
         Module[{u1 = Unique[],u2 = Unique[],v1 = Unique[],v2 = Unique[]},
         class[z,exists[u1,u2,v1,v2,and[
         equal[pair[pair[u1,u2],pair[v1,v2]],w],
         member[pair[u1,v1],x],member[pair[u2,v2],y]]]]]

(* introduced 2005 January 27 *)
class[w_,member[x_,DEDEKIND]] := Module[{y = Unique[]},class[w,and[member[x,V],
      forall[y,implies[and[subclass[y,x],member[pair[x,y],Q]],equal[x,y]]]]]]

class[w_,member[x_,DIV]] := Module[{y = Unique[]},class[w,and[member[first[x],V],exists[y,
         and[member[y,omega],equal[second[x],natmul[first[x],y]]]]]]]

(*  
    Theorems DO-1A',DO-1B and DO-1C in DO1.
    Goedel's definition 1.5      modified  9/15/96  
*)
class[w_,member[u_,domain[x_]]] := 
         Module[{v = Unique[]},class[w,exists[v,
         and[member[u,V],member[pair[u,v],x]]]]]

(* added 2001 December 18 *)
class[z_,member[w_,DORA]] := 
         Module[{u = Unique[]},class[z,exists[u,
         equal[pair[u,pair[domain[u],range[u]]],w]]]]

(* Theorems DUP-1 and DUP-2 in DUP *)
class[z_,member[w_,DUP]] := 
         Module[{u = Unique[]},class[z,exists[u,
         equal[pair[u,pair[u,u]],w]]]]

(* introduced 2004 May 12 *)
class[w_,member[x_,eqv[y_]]]:= class[w,and[member[x,trv[y]],member[x,inverse[trv[y]]]]]

class[w_,member[x_,FINITE]] :=
         Module[{y = Unique[]},class[w,and[member[x,V],
         not[exists[y,and[member[x,y],subclass[y,image[PS,y]]]]]]]]

(* added 2001 November 13 *)
class[w_,member[x_,first[y_]]] :=
         Module[{u = Unique[],v = Unique[]},class[w,and[member[x,V],
         forall[u,v,implies[equal[y,pair[u,v]],member[x,u]]]]]]

(* modified 2003 June 17 *)
class[w_,member[x_,fix[y_]]] := class[w,and[member[x,V],member[pair[x,x],y]]]

class[x_,member[y_,funpart[z_]]] := 
     Module[{u = Unique[],v = Unique[]},class[x,exists[u,v,
     and[equal[pair[u,v],y],equal[image[z,set[u]],set[v]]]]]]

(* introduced 2005 September 18 *)
class[w_,member[x_,GLB[y_]]] := Module[{u = Unique[],v = Unique[]},
      class[w,exists[u,v,and[equal[x,pair[u,v]],member[u,V],member[v,domain[y]],
      subclass[u,image[y,set[v]]],subclass[intersection[domain[y],lb[y,u]],image[inverse[y],set[v]]]]]]]

class[x_,member[y_,GREATEST[z_]]] := 
       Module[{u = Unique[],v = Unique[]},class[x,exists[u,v,
       and[equal[y,pair[u,v]],member[v,u],subclass[cart[u,set[v]],z]]]]]

(* added 2004 September 5 based on HISTORY.NB *)
class[u_,member[v_,history[x_,y_]]] := class[u,and[
      equal[composite[x,id[image[y,set[first[second[v]]]]]],second[second[v]]],
      equal[first[v],first[second[v]]],member[first[v],V],
      member[image[y,set[first[second[v]]]],V]]]

(* added 2004 March 29 based on HULL.NB *)
class[u_,member[v_,hull[x_,y_]]] := Module[{w = Unique[]},
      class[u,forall[w,implies[and[member[w,x],subclass[y,w]],member[v,w]]]]]

(* revised 2001 November 15 *)
class[u_,member[w_,IMAGE[z_]]] := 
        Module[{x = Unique[],y = Unique[]},class[u,exists[x,y,
        and[equal[pair[x,y],w],equal[image[z,x],y]]]]]

class[w_,member[v_,image[z_,x_]]] := 
        Module[{u = Unique[]},class[w,exists[u,
        and[member[v,V],member[u,x],member[pair[u,v],z]]]]]

(* added 2003 August 9 *)
class[u_,member[v_,intadd[x_,y_]]] := Module[{w=Unique[]},class[u,and[member[v,V],
         forall[w,implies[member[pair[pair[x,y],w],INTADD],member[v,w]]]]]]

(* membership rule for INTADD added 2003 July 25 *)
class[x_,member[y_,INTADD]] := 
       Module[{u = Unique[],v = Unique[],w = Unique[]},
       class[x,exists[u,v,w,and[equal[y,pair[pair[u,v],w]],
       member[u,Z],member[v,Z],member[w,Z],subclass[composite[u,v],w]]]]]

(* restored 29 June 2003 from GOEDEL52.L72 *)
class[x_,member[w_,inverse[z_]]] := 
        Module[{u = Unique[],v = Unique[]},class[x,
        exists[u,v,and[equal[pair[u,v],w],member[pair[v,u],z]]]]]

(* definition of iterate added 2002 April 15 *)
class[w_,member[x_,iterate[y_,z_]]] := 
         Module[{p = Unique[]},class[w,exists[p,and[member[x,p],
         subclass[p,union[cart[set[0],z],
         composite[y,p,inverse[SUCC],id[omega]]]]]]]]

(* added 2000 May 24 based on VS-K.NB; wraper 2005 January 7 *)
class[w_,member[x_,K]] := class[w,and[member[x,PS],not[member[x,composite[PS,PS]]]]]

class[x_,member[y_,LB[z_]]] := 
       Module[{u = Unique[],v = Unique[]},class[x,exists[u,v,
       and[equal[y,pair[u,v]],subclass[cart[set[v],u],z]]]]]

class[x_,member[y_,LEAST[z_]]] := 
       Module[{u = Unique[],v = Unique[]},class[x,exists[u,v,
       and[equal[y,pair[u,v]],member[v,u],subclass[cart[set[v],u],z]]]]]

(* revised 2001 November 15 *)
class[x_,member[y_,LEFT[z_]]] := 
       Module[{u = Unique[],v = Unique[]},class[x,
       exists[u,v,and[equal[pair[u,pair[v,u]],y],equal[v,z]]]]]

(* rules added 98/01/22 *)
class[x_,member[w_,LeftPairV]] := 
        Module[{u = Unique[],v = Unique[]},class[x,
        exists[u,v,and[equal[pair[u,v],w],equal[v,pair[V,u]]]]]]

(* introduced 2005 September 18 *)
class[w_,member[x_,LUB[y_]]] := Module[{u = Unique[],v = Unique[]},
      class[w,exists[u,v,and[equal[x,pair[u,v]],member[u,V],member[v,range[y]],
      subclass[u,image[inverse[y],set[v]]],subclass[intersection[range[y],ub[y,u]],image[y,set[v]]]]]]]

(* added 2001 April 25 *)
class[z_,member[w_,map[x_,y_]]] := class[z,and[member[w,FUNS],equal[domain[w],x],subclass[w,cart[V,y]]]]

class[x_,member[y_,MAXIMAL[z_]]] := 
       Module[{u = Unique[],v = Unique[],w=Unique[]},class[x,exists[u,v,
       and[equal[y,pair[u,v]],member[v,u],forall[w,implies[
       and[member[w,u],member[pair[v,w],z]],equal[v,w]]]]]]]

class[x_,member[y_,MINIMAL[z_]]] := 
       Module[{u = Unique[],v = Unique[],w=Unique[]},class[x,exists[u,v,
       and[equal[y,pair[u,v]],member[v,u],forall[w,implies[
       and[member[w,u],member[pair[w,v],z]],equal[v,w]]]]]]]

(* wrapped rule introduced 2005 February 12 *)
class[w_,member[x_,nat[y_]]] := class[w,and[member[x,y],member[y,omega]]]

(* added 2002 July 27 *)
class[u_,member[v_,natadd[x_,y_]]] := Module[{w=Unique[]},class[u,and[member[v,V],
         forall[w,implies[member[pair[pair[x,y],w],NATADD],member[v,w]]]]]]

(* added 2005 May 6 *)
class[u_,member[v_,natmod[x_,y_]]] := Module[{w=Unique[]},class[u,and[member[v,V],
         forall[w,implies[member[w,image[image[inverse[NATADD],set[x]],image[DIV,set[y]]]],member[v,w]]]]]]

(* added 2002 July 27 *)
class[u_,member[v_,natmul[x_,y_]]] := Module[{w=Unique[]},class[u,and[member[v,V],
         forall[w,implies[member[pair[pair[x,y],w],NATMUL],member[v,w]]]]]]

(* added 2002 July 27 *)
class[u_,member[v_,natsub[x_,y_]]] := Module[{w=Unique[]},class[u,and[member[v,V],
         forall[w,implies[member[pair[pair[y,w],x],NATADD],member[v,w]]]]]]

class[z_,member[x_,omega]] := 
       Module[{w = Unique[]},class[z,forall[w,implies[and[member[0,w],
                             subclass[image[SUCC,w],w]],member[x,w]]]]]

class[w_,member[x_,OMEGA]] := class[w,and[member[x,V],
                        subclass[intersection[P[x],FULL],succ[x]]]]

(* added 2004 May 6 *)
class[x_,member[y_,oopart[z_]]] := Module[{u = Unique[],v = Unique[]},
      class[x,exists[u,v,and[equal[pair[u,v],y],
      equal[image[z,set[u]],set[v]],
      equal[image[inverse[z],set[v]],set[u]]]]]]

class[u_,member[v_,pair[x_,y_]]] := 
       Module[{z=Unique[]},class[u,exists[z,
       and[equal[pair[x,y],z],member[v,z]]]]]

(* added 2004 July 29 *)
class[u_,member[v_,partrec[x_,y_]]] := Module[{w = Unique[]},class[u,
      and[invariant[y,domain[v]],exists[w,and[equal[w,composite[id[v],inverse[FIRST]]],
      subclass[v,composite[x,id[composite[IMAGE[w],VERTSECT[y]]],inverse[FIRST]]]]]]]]

(* definition of PointClosed added 2003 July 3 based on PTCLOSED.NB *)
class[w_,member[t_,PointClosed]] := 
      class[w,and[member[t,V],subclass[image[SINGLETON,U[t]],image[RC[U[t]],t]]]]

(* definition of power added 2002 May 20 *)
class[w_,member[x_,power[y_]]] := 
         Module[{p = Unique[]},class[w,exists[p,and[member[x,p],
         subclass[p,union[cart[set[0],Id],
         composite[cross[Id,y],p,inverse[SUCC],id[omega]]]]]]]]

(* revised 2002 January 8 *)
class[w_,member[x_,Q]] := Module[{u = Unique[],v = Unique[],z = Unique[]},
                class[w,exists[u,v,z,and[ONEONE[z],equal[pair[u,v],x],
                               equal[u,domain[z]],equal[v,range[z]]]]]]

class[w_,member[v_,range[z_]]] := 
       Module[{u = Unique[]},class[w,exists[u,
       and[member[v,V],member[pair[u,v],z]]]]]

(* membership rule for rank *)
class[w_,member[y_,rank[x_]]] := Module[{z=Unique[]},
         class[w,and[member[y,V],forall[z,
         implies[and[member[x,V],member[pair[z,x],ZN],member[z,OMEGA]],
                 member[y,z]]]]]]

(* relative complementation function revised 2001 November 15 *)
class[z_,member[w_,RC[x_]]] := Module[{u = Unique[],v = Unique[]},
      class[z,exists[u,v,and[equal[pair[u,v],w],disjoint[u,v],
                             equal[union[u,v],x]]]]]

(* added 2004 July 29 *)
class[u_,member[v_,rec[x_,y_]]] := Module[{w = Unique[]},class[u,
      exists[w,and[member[v,w],member[w,partrec[x,y]]]]]]

class[w_,member[x_,REGULAR]] := Module[{y = Unique[]},class[w,
                                and[member[x,V],forall[y,
                  implies[subclass[y,image[E,y]],not[member[x,y]]]]]]]

(* revised 2001 November 15 *)
class[x_,member[y_,RIF]] := Module[{u=Unique[],v=Unique[],w=Unique[]},
                class[x,exists[u,v,w,
                equal[pair[pair[pair[u,w],pair[v,u]],pair[w,v]],y]]]]

(* revised 2001 November 15 *)
class[x_,member[y_,RIGHT[z_]]] := 
       Module[{u = Unique[],v = Unique[]},class[x,
       exists[u,v,and[equal[pair[u,pair[u,v]],y],equal[v,z]]]]]

(* rules added 98/01/22 *)
class[x_,member[w_,RightPairV]] := 
        Module[{u = Unique[],v = Unique[]},class[x,
        exists[u,v,and[equal[pair[u,v],w],equal[v,pair[u,V]]]]]]

(* membership rule for ROT revised 2001 November 15 *)
class[x_,member[y_,ROT]] := 
       Module[{u = Unique[],v = Unique[],w = Unique[]},
       class[x,exists[u,v,w,equal[pair[pair[pair[u,v],w],
                                  pair[pair[w,u],v]],y]]]]

class[x_,member[y_,rotate[z_]]] := 
       Module[{u = Unique[],v = Unique[],w = Unique[]},class[x,
       exists[u,v,w,and[member[pair[pair[u,w],v],z],
                        equal[pair[pair[v,u],w],y]]]]]

(* modified 2003 June 17 *)
class[w_,member[x_,RUSSELL]] := class[w,and[member[x,V],not[member[x,x]]]]

(* added 2001 November 13 *)
class[w_,member[x_,second[y_]]] :=
         Module[{u = Unique[],v = Unique[]},class[w,and[member[x,V],
         forall[u,v,implies[equal[y,pair[u,v]],member[x,v]]]]]]

(* wrapped rule introduced 2004 May 16 *)
class[w_,member[x_,setpart[y_]]] := class[w,and[member[x,y],member[y,V]]]

(* added 2002 April 6 *)
class[w_,member[x_,SMALLER]] := Module[{u = Unique[],v = Unique[],y=Unique[],z = Unique[]},
                class[w,exists[u,v,and[equal[pair[u,v],x],
                exists[y,and[ONEONE[y],equal[u,domain[y]],subclass[range[y],v]]],
                not[exists[z,and[ONEONE[z],equal[v,domain[z]],subclass[range[z],u]]]]]]]]

class[w_,member[z_,SWAP]] := Module[{u = Unique[],v = Unique[]},class[w,
         exists[u,v,equal[pair[pair[u,v],pair[v,u]],z]]]]

(* added 2003 June 23 based on T1.NB *)
class[w_,member[t_,T1]] := class[w,and[member[t,V],
      subclass[composite[Di,id[U[t]]],composite[complement[inverse[E]],id[t],E]]]]

(* added 2003 June 23 based on T2.NB *)
class[w_,member[t_,T2]] := class[w,and[member[t,V],
      subclass[composite[id[U[t]],Di,id[U[t]]],composite[inverse[E],id[t],DISJOINT,id[t],E]]]]

(* added 2005 February 4 *)
class[w_,member[y_,tc[x_]]] := Module[{u = Unique[], v = Unique[]},
      class[w,exists[u,and[subclass[u,x],forall[v,implies[and[full[v],subclass[u,v]],member[y,v]]]]]]]

(* added 2004 May 13 *)
class[w_,member[x_,thinpart[y_]]] := class[w,and[member[x,y],member[first[x],V],member[image[y,set[first[x]]],V]]]

(* revised 2003 May 23 based on DEF-CLOS.NB *)
class[w_,member[x_,TOPS]] := class[w,and[equal[x,Uclosure[x]],member[x,V],
                       subclass[image[CAP,cart[x,x]],x]]]

(* revised 2004 March 29 based on HULL.NB *)
class[u_,member[x_,trv[y_]]] := Module[{z = Unique[]},
      class[u,exists[z,and[member[x,hull[TRV,z]],subclass[z,y],subclass[z,cart[V,V]]]]]]

(* added 1999 October 10 based on TWIST.1 *)
class[w_,member[z_,TWIST]] := 
              Module[{u=Unique[],v=Unique[],x=Unique[],y=Unique[]},
              class[w,exists[u,v,x,y,equal[
              pair[pair[pair[u,v],pair[x,y]],pair[pair[u,x],pair[v,y]]],z]]]]

class[t_,member[u_,twist[v_]]] := 
       Module[{w = Unique[],x = Unique[],y = Unique[],z = Unique[]},
       class[t,exists[w,x,y,z,and[equal[pair[pair[w,x],pair[y,z]],u],
       member[pair[pair[w,y],pair[x,z]],v]]]]]

class[w_,member[x_,U[z_]]] := 
       Module[{y = Unique[]},class[w,exists[y,
       and[member[x,y],member[y,z]]]]]

class[x_,member[y_,UB[z_]]] := 
       Module[{u = Unique[],v = Unique[]},class[x,exists[u,v,
       and[equal[y,pair[u,v]],subclass[cart[u,set[v]],z]]]]]

(* revised 2001 November 15 *)
class[x_,member[y_,VERTSECT[z_]]] := 
      Module[{u = Unique[],v = Unique[]},
        class[x,exists[u,v,and[equal[y,pair[u,v]],
              equal[image[z,set[u]],v]]]]]

(* added 2002 November 11 *)
class[w_,member[x_,Z]] := Module[{y = Unique[]},
         class[w,member[x,image[VERTSECT[y],cart[omega,omega]]]]/.y->EQUIDIFF]

(* added 2001 July 5 *)
class[x_,member[y_,ZN]] := Module[{u = Unique[],v= Unique[],w = Unique[]},
         class[x,exists[w,and[member[y,composite[Id,w]],
         subclass[composite[inverse[E],w],composite[inverse[E],IMAGE[w]]]]]]]

(* introduced 2004 March 21 in PO-WRAP.NB *)
class[w_,PARTIALORDER[x_]] := class[w,and[equal[domain[x],fix[x]],equal[fix[x],range[x]],
      subclass[intersection[x,inverse[x]],Id],TRANSITIVE[x]]]

(* introduced 2004 March 18 in RFX-WRAP.NB *)
class[w_,REFLEXIVE[x_]] := Module[{z = Unique[]},class[w,forall[z,
      implies[member[z,x],and[member[first[z],fix[x]],member[second[z],fix[x]]]]]]]

(* Definition DF-SU-1,DF-SU-2 and DF-SU-3 in AX-A *)
class[w_,subclass[x_,y_]] := 
       Module[{u = Unique[]},class[w,
       forall[u,implies[member[u,x],member[u,y]]]]]

(* introduced 2004 September 5 in WF-REC-4.NB *)
class[w_,subvariant[x_,y_]] := Module[{z = Unique[]},class[w,forall[z,implies[member[z,y],member[z,image[x,y]]]]]]

(* revised 2004 February 10 *)
class[w_,TOTALORDER[x_]] := class[w,and[ANTISYMMETRIC[x],TRANSITIVE[x],equal[union[x,inverse[x]],cart[fix[x],fix[x]]]]]

(* introduced 2004 March 20 in EQV-WRAP.NB *)
class[z_,TRANSITIVE[x_]] := Module[{u = Unique[],v = Unique[],w = Unique[]},
      class[z,and[subclass[x,cart[V,V]],forall[u,v,w,
      implies[and[member[pair[u,v],x],member[pair[v,w],x]],member[pair[u,w],x]]]]]]

(* added 2003 September 27 *)
class[w_,WELLFOUNDED[x_]] := Module[{y=Unique[]},class[w,and[subclass[x,cart[V,V]],forall[y,implies[subvariant[x,y],equal[0,y]]]]]]

(* wrapped 2004 January 24 *)
class[w_,WELLORDER[x_]] := class[w,and[REFLEXIVE[x],subclass[P[fix[x]],union[set[0],domain[funpart[LEAST[x]]]]]]]

class[x_,False]:=0
class[x_,True]:=V /; AtomQ[x]

class[pair[u_,v_],True] := cart[class[u,True],class[v,True]]

class[z_,member[z_,x_]] := x /; And[FreeQ[x,z],AtomQ[z]]

(* axiom B.1    membership relation *)

class[pair[u_,v_],member[u_,v_]] := E /; And[AtomQ[u],AtomQ[v]]

(* axiom B.2    intersection *)

class[x_,and[p_,q_]] := intersection[class[x,p],class[x,q]]

(* added 1996 July 28: *)

class[x_,or[p_,q_]] := union[class[x,p],class[x,q]]

(* axiom B.3    complement *)

class[x_,not[p_]] := intersection[complement[class[x,p]],class[x,True]]

(* axiom B.4 domain and Goedel's equation 2.8 on page 9 *)

class[x_,exists[y_,p_]] := domain[class[pair[x,y],p]]

(* axiom B.5    cartesian product
   an interpretation of Goedel's equations 2.41 and 2.7 on page 9
*)
class[pair[u_,v_],p_] := cart[class[u,p],class[v,True]] /; allfreeQ[p,v]

class[pair[u_,v_],p_] := cart[class[u,True],class[v,p]] /; allfreeQ[p,u]

(* axiom B.6    inverse *)

class[pair[u_,v_],member[v_,u_]] := inverse[E] /; And[AtomQ[u],AtomQ[v]]

(*
   The following rules replace Goedel's rotation rules on page 9:
*)

(* revised 2000 January 13 *)
class[pair[pair[u_,v_],w_],p_] := composite[class[pair[v,w],p],SECOND,
                             id[cart[class[u,True],V]]] /; allfreeQ[p,u]

(* revised 2000 January 13 *)
class[pair[pair[u_,v_],w_],p_] := composite[class[pair[u,w],p],FIRST,
                             id[cart[V,class[v,True]]]] /; allfreeQ[p,v]

(* revised 2000 January 13 *)
class[pair[w_,pair[u_,v_]],p_] := composite[id[cart[class[u,True],V]],
                    inverse[SECOND],class[pair[w,v],p]] /; allfreeQ[p,u]

(* revised 2000 January 13 *)
class[pair[w_,pair[u_,v_]],p_] := composite[id[cart[V,class[v,True]]],
                     inverse[FIRST],class[pair[w,u],p]] /; allfreeQ[p,v]

(* special page 10 maneuver   revised 9/15/96 *)

class[u_,member[x_,y_]] := Module[{v = Unique[]},
                           class[u,exists[v,and[equal[x,v],member[v,y]]]]] /; 
                           FreeQ[varlist[u],x]

(* new rules for equality *)

class[pair[u_,v_],equal[u_,v_]] := Id /; And[AtomQ[u],AtomQ[v]]

class[pair[u_,v_],equal[v_,u_]] := Id /; And[AtomQ[u],AtomQ[v]]

class[x_,equal[x_,y_]] := 
     intersection[set[y],class[x,True]] /; allfreeQ[y,x]

class[x_,equal[y_,x_]] := 
     intersection[set[y],class[x,True]] /; allfreeQ[y,x]

(* 
   AX-EQ in AX-A.  Goedel's Axiom A.3 of Coextension.    
   Revised 1996 August 23 
*)
class[w_,equal[x_,y_]] := intersection[class[w,subclass[x,y]],
                                       class[w,subclass[y,x]]] /;
                          And[Or[Not[MemberQ[varlist[w],x]],
                                 Not[MemberQ[varlist[w],y]]],
                              Not[SameQ[Head[x],pair]],
                              Not[SameQ[Head[y],pair]]]

(* corrections added 9/17/96 at 9:20 p.m. *)

class[w_,equal[set[u_],set[v_]]] := class[w,equal[u,v]] /;
                       MemberQ[varlist[w],u] || MemberQ[varlist[w],v] || 
                       member[u,V] || member[v,V]

(* rules for pairs *)

BadPair := Module[{},Print[pair::argx]; Abort[]]

pair[] := BadPair
 
pair[x_] := BadPair

pair[x_,y_,z__] := BadPair

(* rules that apply when x or y is known not to be a set *)
pair[x_,y_] := pair[V,y] /; Not[V === x] && not[member[x,V]]

pair[x_,y_] := pair[x,V] /; Not[V === y] && not[member[y,V]]

(* 
   rule that applies when z does not occur in varlist[u] 
   or when z does occur in x or y.
*)
class[u_,equal[pair[x_,y_],z_]] := Module[{v=Unique[]},
         class[u,exists[v,and[equal[pair[x,y],v],equal[v,z]]]]] /;
         Not[MemberQ[varlist[u],z]] || Not[FreeQ[{x,y},z]]

(* 
   First rule that applies when z does occur in varlist[w] and
   z does not occur in either x or y.  This rule only applies in 
   the special case when it is known somehow that x and y are sets.
*)
class[w_,equal[pair[x_,y_],z_]] := Module[{u=Unique[],v=Unique[]},
         class[(w/.z->pair[u,v]),and[equal[x,u],equal[y,v]]]] /;
         And[MemberQ[varlist[w],z],FreeQ[{x,y},z],
             Or[member[x,V],MemberQ[varlist[w],x]],
             Or[member[y,V],MemberQ[varlist[w],y]]]

(* next two rules were modified 1998 March 12 *)

(* rule that applies when one does not know whether or not x is a set *)
class[u_,equal[pair[x_,y_],z_]] := Module[{v=Unique[]},
         class[u,or[and[not[member[x,V]],equal[pair[V,y],z]],
         exists[v,and[equal[x,v],equal[pair[v,y],z]]]]]] /;
         Not[MemberQ[varlist[u],x]] && UnsameQ[V,x] && 
         Not[member[x,V] === True]

(* rule that applies when one does not know whether or not y is a set *)
class[u_,equal[pair[x_,y_],z_]] := Module[{v=Unique[]},
         class[u,or[and[not[member[y,V]],equal[pair[x,V],z]],
         exists[v,and[equal[y,v],equal[pair[x,v],z]]]]]] /;
         Not[MemberQ[varlist[u],y]] && UnsameQ[V,y] && 
         Not[member[y,V] === True]

(* added 9/15/96 *)

class[pair[u_,v_],equal[pair[V,u_],v_]] := LeftPairV
class[pair[u_,v_],equal[pair[u_,V],v_]] := RightPairV

(* added 1/18/98 *)

class[pair[u_,v_],equal[pair[V,v_],u_]] := inverse[LeftPairV]
class[pair[u_,v_],equal[pair[v_,V],u_]] := inverse[RightPairV]

(* added 9/17/96 *)
image[inverse[RightPairV],x_] := 0 /; composite[Id,x] == x
image[inverse[LeftPairV],x_] := 0 /; composite[Id,x] == x

(* rules added 1998 October 11 *)

class[w_,equal[pair[V,y_],z_]] := Module[{v = Unique[]},
         class[w,or[and[not[member[y,V]],equal[pair[V,V],z]],
         and[member[y,V],exists[v,and[equal[pair[V,v],z],equal[v,y]]]]]]] /;
         Not[allfreeQ[y,w]]

class[w_,equal[pair[x_,V],z_]] := Module[{v = Unique[]},
         class[w,or[and[not[member[x,V]],equal[pair[V,V],z]],
         and[member[x,V],exists[v,and[equal[pair[v,V],z],equal[v,x]]]]]]] /;
         Not[allfreeQ[x,w]]

class[w_,equal[pair[V,V],w_]] := set[pair[V,V]]

class[w_,equal[pair[V,V],x_]] := Module[{v = Unique[]},
         class[w,exists[v,and[equal[pair[V,V],v],equal[v,x]]]]] /;
         Not[MemberQ[x,varlist[w]]]

(* unconventional definition for FUNCTION revised 2001 November 24 *)
class[w_,FUNCTION[x_]] := Module[{z = Unique[]},
      class[w,and[subclass[x,cart[V,V]],forall[z,or[
      not[member[z,x]],not[member[z,composite[Di,x]]]]]]]]

Print["Loading Simplification Rules"];

(* unconditional rules *)

(* Theorem A-3 in A1 *)
A[0] := V

(* Theorem ACL-A in ACL1 proved 2001 September 29 *)
A[Aclosure[x_]] := A[x]

(* derived 2004 December 10 in AP-IMG.NB *)
A[cart[x_,intersection[z_,image[V,y_]]]] := union[A[cart[x,z]],complement[image[V,y]]]

(* temporary rule added 2002 January 1 based on PAIR-MEM.NB *)
A[cart[set[x_],set[y_]]] := PAIR[x,y]

(* temporary rule added 2002 January 1 based on PAIR-MEM.NB *)
A[cart[cart[set[x_],set[y_]],set[z_]]] := PAIR[PAIR[x,y],z]

(* Theorem SP-A-C-A in SP3  *)
A[complement[A[x_]]] := complement[image[V,x]]

(* Theorem A-C-IM-V in A1 added 1998 April 19 *)
A[complement[image[V,x_]]] := image[V,x] 

(* Theorem SR-A-C in SR1 proved 1998 October 18 *)
A[complement[image[S,set[x_]]]] := complement[image[V,x]]

(* Theorem DI-A-PC in DI added 1998 July 2 *)
A[complement[P[x_]]] := complement[image[Di,complement[x]]]     

(* Theorem REG-C-A in REG2 proved 1999 March 18 *)
A[complement[REGULAR]] := complement[image[V,complement[REGULAR]]]

(* Corollary SP-A-C1 in SP3 proved 1998 December 8 *) 
A[complement[set[x_]]] := 0 

(* Theorem DESC-A in REG1 proved 1999 March 18 *)
A[DESCENDING] := 0

(* Theorem FIN-A in FINITE proved 2000 March 18 *)
A[FINITE] := 0

(* added 2003 February 22 based on FIX-HULL.NB *)
A[fix[HULL[x_]]] := A[x]

(* added 2002 July 27 based on A-FP-UCL.NB *)
A[fix[UCLOSURE]] := set[0]

(* Theorem FUL-A-0 in FUL3 added 1998 February 7 *)
A[FULL] := 0

(* added 2001 March 28 based on ADJOIN.NB *)
A[image[ADJOIN[x_],y_]] := union[x,A[y],complement[image[V,set[x]]]]

(* Theorem BA-A-SC in BIGCAP/BA1 proved 1998 December 9 *)
A[image[BIGCAP,x_]] := A[U[x]]

(* added 1999 October 5 based on CAP-CUP.1 *)
A[image[CAP,x_]] := intersection[A[domain[x]],A[range[x]]] 

(* added 1999 October 5 based on CART.1 *)
A[image[CART,x_]] := union[cart[A[domain[x]],A[range[x]]],
                           complement[image[V,domain[x]]]]

(* added 2003 October 28 based on APPLY.NB *)
A[image[x_,cart[set[y_],set[z_]]]] := APPLY[x,PAIR[y,z]]

(* added 2001 April 30 based on CLIQUES2.NB *)
A[image[CLIQUES,x_]] := cliques[A[x]]

(* added 1999 October 5 based on CAP-CUP.2 *)
A[image[CUP,x_]] := complement[fix[composite[complement[inverse[E]],x,complement[E]]]]

(* added 1999 October 5 based on CUP-SR.1 *)
A[image[CUP,cart[x_,y_]]] := union[A[x],A[y]]

(* Theorem SP-A-DI in SP3 proved 1998 October 8 *)
A[image[Di,x_]] := complement[image[V,x]]

(* added 2000 January 5 based on A-IM-DIF.NB *)
A[image[DIF,x_]] := intersection[A[domain[x]],complement[U[range[x]]]]

(* Theorem DJT-A-IM in DJT proved 1998 October 18 *)
A[image[DISJOINT,x_]] := complement[image[V,x]]

(* derived 2005 May 5 in S-DIV.NB *)
A[image[DIV,x_]] := complement[image[V,intersection[omega,x]]]

(* added 2001 April 10 based on HC-BA.NB *)
A[image[HC,x_]] := H[A[x]]

(* added 2001 December 03 based on HULL.NB *)
A[image[HULL[x_],y_]] := A[intersection[x,image[S,y]]]

(* added 2001 February 27 based on STUDY.NB *)
A[image[IMAGE[id[x_]],y_]] := 
        union[complement[image[V,y]],intersection[x,A[y]]]

(* added 1999 October 7 based on FP-A.LOG *)
A[image[IMAGE[inverse[DUP]],x_]] := fix[A[x]]

(* derived 2005 May 17 based on NATMOD.NB *)
A[image[image[inverse[NATADD],set[x_]],image[DIV,set[y_]]]] := natmod[x,y]

(* added 2001 May 3 based on BA-IMG.NB *)
A[image[IMAGE[inverse[POWER]],x_]] := image[inverse[POWER],A[x]]

(* added 2002 February 17 based on IMG-IMG.NB *)
A[image[IMAGE[SWAP],x_]] := union[complement[image[V,x]],inverse[A[x]]]

(* added 2002 April 10 based on INVAR.NB *)
A[image[INVAR,x_]] := complement[image[V,x]]

(* added 1999 October 29 based on 1999 October 28 FIX-IDP.LOG *)
A[image[inverse[IMAGE[DUP]],x_]] := fix[A[intersection[x,P[Id]]]]

(* Theorem SR-IN-A in SR3 proved 1998 October 18 *)
A[image[inverse[S],x_]] := complement[image[V,x]]

(* added 1999 October 30 based on IMAGEINT.2 *)
A[image[PAIRSET,x_]] := complement[fix[composite[Di,x,Di]]]

(* Theorem POW-A in POW3 proved 1998 November 12 *)
A[image[POWER,x_]] := P[A[x]]

(* added 2000 May 9 based on Q-C-E.NB *)
A[image[Q,x_]] := complement[image[V,x]]

(* derived 2004 April 17 in REPLACE.NB *)
A[image[RC[x_],y_]] := union[complement[image[V,intersection[y,P[x]]]],
  complement[image[V,set[x]]],intersection[x,complement[core[y,x]]]]

(* Theorem SR-IM-A in SR3 proved 1998 August 15 *)
A[image[S,x_]] := A[x]

(* Theorem AP-SG-A in AP2 proved 1998 September 8 *)
A[image[SINGLETON,x_]] := complement[image[Di,x]]

(* added 2003 October 28 based on APPLY.NB *)
A[image[x_,set[y_]]] := APPLY[x,y]

(* added 2000 January 7 based on TC-CO.TXT *)
A[image[TC,x_]] := A[intersection[FULL,image[S,x]]]

(* Theorem A-IM-V in A1 *)
A[image[V,x_]] := complement[image[V,x]]

(* derived 2004 February 19 in REPLACE2.NB *)
A[image[VERTSECT[x_],y_]] := ub[x,intersection[y,domain[VERTSECT[x]]]]

(* added 2001 July 15 based on ZN-AGAIN.NB *)
A[image[ZN,x_]] := complement[image[V,x]]

(* added 2002 May 31 based on ALEPH-0.NB *)
A[intersection[complement[omega],fix[CARD]]] := omega

(* Theorem A-U-IMV in A1 proved 1998 December 10 *)
A[intersection[x_,complement[image[V,y_]]]] := union[A[x],image[V,y]]

(* Theorem SUC-IND5 in SUC-RELATION proved 1998 July 9 *)
A[intersection[complement[P[complement[set[0]]]],invar[SUCC]]] := omega

(* derived 2004 April 25 in ADJOIN.NB *)
A[intersection[image[S,x_],image[S,y_]]] := union[A[x],A[y]]

(* derived 2004 March 29 based on HULL.NB *)
A[intersection[x_,image[S,set[y_]]]] := hull[x,y]

(* Theorem A-I-IMV in A1 proved 1998 December 10 *)
A[intersection[x_,image[V,y_]]] := union[A[x],complement[image[V,y]]]

(* derived 2005 February 19 in ITR-OM-E.NB *)
A[intersection[omega,complement[nat[x_]]]] := nat[x]

(* added 2002 May 31 based on DICHOT.NB *)
A[intersection[OMEGA,complement[omega]]] := omega

(* added 2003 January 20 based on ONSUC7OT.NB       *)
(* singleton of 0 is the least ordinal that holds 0 *)
A[intersection[OMEGA,complement[set[0]]]] := set[0]

(* added 2003 January 20 based on ON-SUC-7.NB *)
(* omega is the least limit ordinal           *)
A[intersection[OMEGA,complement[set[0]],fix[BIGCUP]]] := omega

(* added 2001 July 12 based on RANK-1.NB *)
A[intersection[OMEGA,image[inverse[ZN],set[x_]]]] := rank[x]

(* added 2001 December 1 based on CARD-X.NB *)
A[intersection[OMEGA,image[Q,set[x_]]]] := card[x]

(* added 1999 August 13 based on session A-I-SS.LOG *)
A[intersection[x_,set[y_]]] := union[y,complement[image[V,intersection[x,set[y]]]]]

(* Theorem IVR-0-A in INVAR *)
A[invar[x_]] := 0

(* Theorem OM-A in OM1 added 1998 February 7 *)
A[omega] := 0

(* Theorem ON-A-DEM in ON5 added 1998 February 7 *)
A[OMEGA] := 0

(* Theorem PC-A in PC1 *)
A[P[x_]] := 0

(* derived 2005 February 22 in PRIMES.NB *)
A[PRIMES] := succ[set[0]]

(* added 1999 November 6 based on CO-2.LOG *)
A[range[CART]] := 0

(* Theorem POW-RA-1 in POW5 *)
A[range[POWER]] := set[0]

(* Theorem SG-RA-A in SG2 proved 1998 February 3 *)
A[range[SINGLETON]] := 0

(* added 2002 April 8 based on UCL-ACL.NB *)
A[range[SUBVAR]] := set[0]

(* Theorem REG-A in REG2 *)
A[REGULAR] := 0

(* Theorem RUS-A in RUS2 *)
A[RUSSELL] := 0

(* Theorem A-SS in A1 proved 1998 July 13 *)
A[set[x_]] := union[x,complement[image[V,set[x]]]]

(* derived 2004 August 29 in A-SS-AP.NB *)
A[set[APPLY[x_,y_]]] := APPLY[x,y]

(* derived 2004 August 1 in COMMON2.NB *)
A[succ[set[x_]]] := intersection[x,set[x]]

(* added 2001 December 9 based on EQUAL-V.NB *)
A[TOPS] := set[0]

(* Theorem A-7 in A1 *)
A[union[x_,y_]] := intersection[A[x],A[y]]

(* Theorem A-4 in A1 *)
A[V] := 0

(* added 2003 February 25 based on Z.NB *)
A[Z] := 0

(* Theorem ACL-0 in ACL1 proved 2001 September 29 *)
Aclosure[0] := 0

(* added 2003 October 15 based on ACYCLIC.NB *)
Aclosure[ACYCLIC] := ACYCLIC

(* added 2002 January 17 based on ANTISYM3.NB *)
Aclosure[ANTISYM] := ANTISYM

(* added 2001 October 15 based on ACL-IMS.NB *)
Aclosure[BIJ] := BIJ

(* added 2003 May 21 based on BINCLOSE.NB *)
Aclosure[binclosed[x_]] := binclosed[x]

(* added 2002 May 11 based on PAIR.NB *)
Aclosure[cart[set[x_],set[y_]]] := cart[set[x],set[y]]

(* added 2001 October 15 based on ACL-IMS.NB *)
Aclosure[cliques[x_]] := cliques[x]

(* added 2003 February 23 based on ACL-CIMS.NB *)
Aclosure[complement[image[S,x_]]] := complement[image[S,x]]

(* added 2002 January 9 based on ACLOSURE.NB *)
Aclosure[complement[P[complement[set[x_]]]]] := 
      complement[P[complement[set[x]]]]

(* added 2002 May 2 based on ACLOSED.NB *)
Aclosure[EQV] := EQV

(* added 2002 January 31 based on FIX-ACL.NB *)
Aclosure[fix[ACLOSURE]] := fix[ACLOSURE]

(* added 2002 January 18 based on CLIQUES.NB *)
Aclosure[fix[composite[DISJOINT,IMAGE[x_]]]] := 
         fix[composite[DISJOINT,IMAGE[x]]]

(* added 2002 January 17 based on CLIQSWAP.NB *)
Aclosure[fix[composite[DISJOINT,INVERSE]]] := 
         fix[composite[DISJOINT,INVERSE]]

(* derived 2004 May 4 in ALLCLOSED.NB *)
Aclosure[fix[composite[S,IMAGE[x_],POWER]]] := fix[composite[S,IMAGE[x],POWER]]

(* added 2001 October 14 based on ACL-4.NB *)
Aclosure[fix[IMAGE[inverse[S]]]] := fix[IMAGE[inverse[S]]]

(* added 2001 January 31 based on FIX-UCL.NB *)
Aclosure[fix[UCLOSURE]] := fix[UCLOSURE]

(* Corollary of Theorem IVR-FUL5 in INVAR proved 1999 December 29 *)
Aclosure[FULL] := FULL

(* added 2001 October 15 based on ACL-IMS.NB *)
Aclosure[FUNS] := FUNS

(* added 2001 October 15 based on ACL-IMS.NB *)
Aclosure[FINITE] := FINITE

(* added 2003 September 5 based on FIXHULL.NB *)
Aclosure[fix[HULL[x_]]] := fix[HULL[x]]

(* added 2001 October 15 based on ACL-IMS.NB *)
Aclosure[H[FINITE]] := H[FINITE]

(* added 2003 May 18 based on ACL-SQ.NB *)
Aclosure[image[CART,Id]] := image[CART,Id]

(* added 2003 May 18 based on ACL-SQ.NB *)
Aclosure[image[CART,id[x_]]] := image[CART,id[Aclosure[x]]]

(* restored 2001 October 14 based on IMS.NB *)
Aclosure[image[inverse[S],x_]] := image[inverse[S],x]

(* added 2003 June 22 based on HULL-RC.NB *)
Aclosure[image[RC[x_],y_]] := 
         image[RC[x],intersection[image[S,y],Uclosure[y]]]

(* restored 2001 October 14 based on ACL-3.NB *)
Aclosure[image[S,set[x_]]] := image[S,set[x]]

(* added 2003 February 23 based on ACL-CIMS.NB *)
Aclosure[image[V,x_]] := image[V,x]

(* derived 2005 September 17 in ACL-DIV.NB *)
Aclosure[image[VERTSECT[DIV],omega]] := image[VERTSECT[DIV],omega]

(* added 2002 May 6 based on HULL-ACL.NB *)
Aclosure[intersection[x_,image[S,set[y_]]]] :=
         intersection[Aclosure[x],image[S,set[y]]]

(* derived 2005 July 24 in ACL-P-OM.NB *)
Aclosure[intersection[omega,x_]] := intersection[omega,x]

(* derived 2005 July 24 in ACL-P-OM.NB *)
Aclosure[intersection[OMEGA,x_]] := intersection[OMEGA,x]

(* added 2001 October 28 based on IVR-RFX.NB *)
Aclosure[intersection[RFX,SYM]] := intersection[RFX,SYM]

(* Corollary of Theorem IVR-BA in INVAR proved 1999 January 9 *)
Aclosure[invar[x_]] := invar[x]

(* Corollary of Theorem ON-BA1 in ON5 proved 1999 December 30 *)
Aclosure[OMEGA] := OMEGA

(* Theorem ACL-PC1 in ACL1 proved 2001 September 29 *)
Aclosure[P[x_]] := P[x]

(* derived 2005 July 24 in ACL-P-OM.NB *)
Aclosure[PRIMES] := PRIMES

(* derived 2004 April 27 in UCL-SS.NB *)
Aclosure[set[0,x_]] := set[0,x]

(* added 2002 March 9 based on PO-ACL.NB *)
Aclosure[PO] := PO

(* restored 2001 October 14 based on RA-POW.NB *)
Aclosure[range[POWER]] := range[POWER]

(* derived 2005 September 8 in RAVS-DIV.NB *)
Aclosure[range[VERTSECT[DIV]]] := range[VERTSECT[DIV]]

(* Theorem ACL-REG in ACL1 proved 2001 September 29 *)
Aclosure[REGULAR] := REGULAR

(* added 2001 October 28 based on IVR-RFX.NB *)
Aclosure[RFX] := RFX

(* derived 2004 August 7 in RS-1.NB *)
Aclosure[RS[x_]] := RS[x]

(* added 2001 October 15 based on ACL-UCL.NB *)
Aclosure[set[x_]] := set[x]

(* added 2001 October 14 based on RA-POW.NB *)
Aclosure[SYM] := SYM

(* added 2003 May 21 based on BINCLOSE.NB *)
Aclosure[TOPS] := TOPS

(* added 2002 January 30 based on ACL-TRV.NB *)
Aclosure[TRV] := TRV

(* added 2002 January 9 based on ACLOSURE.NB *)
Aclosure[union[x_,complement[image[V,y_]]]] := 
      union[Aclosure[x],complement[image[V,y]]]

(* added 2002 January 9 based on ACLOSURE.NB *)
Aclosure[union[x_,image[V,y_]]] := union[Aclosure[x],image[V,y]]

(* added 2002 May 2 based on ACLOSED.NB *)
Aclosure[union[range[SINGLETON],set[0]]] := 
               union[range[SINGLETON],set[0]]

(* added 2002 November 20 based on UCL-U.NB *)
Aclosure[union[x_,set[0]]] := union[Aclosure[x],set[0]]

(* Theorem ACL-V-1 in ACL1 proved 2001 September 29 *)
Aclosure[V] := V

(* added 2003 September 29 based on WF.NB *)
Aclosure[WF] := WF

(* added 2003 February 26 based on ACL-Z.NB *)
Aclosure[Z] := union[Z,set[0]]

(* Theorem ADJ-0 in ADJ proved 1999 March 11 *)
ADJOIN[0] := Id

(* added 2003 February 20 based on ADJOIN-V.NB *)
ADJOIN[complement[image[V,x_]]] := id[image[V,x]]

(* added 2003 February 20 based on ADJOIN-V.NB *)
ADJOIN[image[V,x_]] := id[complement[image[V,x]]]

(* derived 2004 April 25 in ADJOIN.NB *)
ADJOIN[union[x_,complement[image[V,y_]]]] := composite[id[image[V,y]],ADJOIN[x]]

ADJOIN[V] := 0

(* added 2001 November 15 based on EQ-0.NB *)
and[equal[0,x_],equal[y_,x_]] := and[equal[0,x],equal[0,y]]

(* added 2001 November 15 based on EQ-0.NB *)
and[equal[0,x_],equal[x_,y_]] := and[equal[0,x],equal[0,y]]

(* added 2002 September 10 based on IMV-RULE.NB *)
and[equal[0,x_],equal[0,intersection[x_,y_]]] := equal[0,x]

(* added 2002 September 8 based on REPLACE.NB *)
and[equal[0,x_],equal[y_,union[x_,z_]]] := and[equal[0,x],equal[y,z]]

(* added 2002 December 23 based on REPLACE.NB *)
and[equal[0,fix[composite[y_,inverse[x_],Di]]],subclass[x_,y_],
    subclass[x_,cart[V,V]]] := subclass[x,funpart[y]]

(* derived 2004 April 4 in IRR-TRV.NB *)
and[equal[0,fix[composite[x_,x_]]],TRANSITIVE[x_]] := and[equal[0,fix[x]],TRANSITIVE[x]]

(* derived 2004 December 30 in AXREG.NB *)
and[equal[0,fix[E]],member[x_,x_]] := False

(* added 2002 September 7 based on REPLACE.NB *)
and[equal[0,intersection[x_,y_]],equal[V,union[x_,y_]]] := equal[y,complement[x]]

(* derived 2004 April 4 in IRR-TRV.NB *)
and[equal[0,intersection[x_,inverse[x_]]],TRANSITIVE[x_]] := and[equal[0,fix[x]],TRANSITIVE[x]]

(* derived 2005 February 6 in DESCEND.NB *)
and[equal[0,intersection[x_,P[complement[x_]]]],member[x_,y_]] := and[member[x,DESCENDING],member[x,y]]

(* added 2002 December 23 based on REPLACE.NB *)
and[equal[0,intersection[x_,y_]],subclass[x_,z_],
    subclass[z_,union[x_,y_]]] := equal[x,intersection[z,complement[y]]]

(* added 2002 September 8 based on REPLACE.NB *)
and[equal[0,intersection[x_,y_]],subclass[x_,union[y_,z_]]] :=
    and[equal[0,intersection[x,y]],subclass[x,z]]

(* added 1998 October 3 *)
and[equal[0,x_],member[y_,x_]] := False

(* derived 2005 June 29 in OO-TIMES.NB *)
and[equal[0,x_],member[x_,omega]] := equal[0,x]

(* added 2001 October 20 based in CART-SQ.NB *)
and[equal[0,x_],member[x_,V]] := equal[0,x]

(* derived 2005 January 21 in SS-0.NB *)
and[equal[0,x_],not[member[x_,range[SINGLETON]]]] := equal[0,x]

(* added 2001 November 15 *)
and[equal[0,x_],not[member[x_,V]]] := False

(* added 2001 November 17 based on UNWRAP.NB *)
and[equal[0,second[x_]],not[member[first[x_],V]]] := False

(* added 2001 November 15 based on EQ-0.NB *)
and[equal[0,x_],subclass[x_,y_]] := equal[0,x]

(* added 2001 November 15 based on EQ-0.NB *)
and[equal[0,x_],subclass[y_,x_]] := and[equal[0,x],equal[0,y]]

(* derived 2004 June 20 in X1604-56.NB *)
and[equal[cart[fix[x_],fix[x_]],union[x_,inverse[x_]]],PARTIALORDER[x_]] := TOTALORDER[x]

(* derived 2004 June 26 in TOTALORD.NB 
   removed 2004 June 27 because it causes looping
and[equal[cart[fix[x_],fix[x_]],union[x_,inverse[x_]]],
    subclass[intersection[x_,inverse[x_]],Id],TRANSITIVE[x_]] := TOTALORDER[x]
*)

(* derived 2004 March 20 in EQV-WRAP.NB *)
and[equal[composite[Id,x_],inverse[x_]],TRANSITIVE[composite[Id,x_]]] := EQUIVALENCE[composite[Id,x]]

(* derived 2004 October 28 in X.NB *)
and[equal[domain[y_],domain[funpart[x_]]],subclass[y_,funpart[x_]]] := equal[y,funpart[x]]

(* added 2001 December 16 based on COMMUTE.NB *)
and[equal[x_,image[S,x_]],
    equal[x_,image[inverse[S],x_]]] := or[equal[0,x],equal[V,x]]

(* derived 2004 January 15 in RC-OP.NB *)
and[equal[x_,intersection[y_,complement[z_]]],
    equal[z_,intersection[y_,complement[x_]]]] := 
    and[equal[0,intersection[x,z]],equal[y,union[x,z]]]

(* added 2001 December 19 based on INV-IM.NB *)
and[equal[x_,intersection[y_,z_]],subclass[y_,z_]] := and[equal[x,y],subclass[x,z]]

(* derived 2004 March 20 in EQV-WRAP.NB *)
and[equal[x_,inverse[x_]],TRANSITIVE[x_]] := EQUIVALENCE[x]

(* derived 2004 March 20 in EQV-WRAP.NB *)
and[equal[x_,inverse[x_]],TRANSITIVE[composite[Id,x_]]] := EQUIVALENCE[x]

(* added 2001 November 15 based on UNWRAP-1.NB *)
and[equal[x_,y_],member[x_,z_],member[y_,V]] := and[equal[x,y],member[x,z]]

(* derived 2003 January 3 in OO-SUC-OM.NB *)
and[equal[x_,y_],member[x_,omega],member[x_,y_]] := False

(* derived 2005 April 26 in TRICHOT.NB *)
and[equal[x_,nat[y_]],member[x_,nat[y_]]] := False

(* derived 2005 April 28 in NATORDER.NB *)
and[equal[x_,nat[y_]],member[nat[y_],x_]] := False

(* derived 2005 April 26 in TRICHOT.NB *)
and[equal[x_,nat[y_]],not[member[x_,nat[y_]]]] := equal[x,nat[y]]

(* derived 2005 July 4 in SUCC-NAT.NB *)
and[equal[nat[x_],succ[y_]],member[y_,nat[x_]]] := equal[nat[x],succ[y]]

(* derived 2005 May 17 based on NATMOD.NB *)
and[equal[z_,natmod[x_,y_]],member[z_,V]] := and[equal[z,natmod[x,y]],member[x,omega],member[y,omega]]

(* added 2003 May 24 based on DIFCLOS.NB *)
and[equal[x_,y_],not[subclass[x_,y_]]] := False

(* derived 2005 February 10 in X3557.NB *)
and[equal[omega,x_],member[x_,V]] := equal[omega,x]

(* derived 2004 July 18 in WO-PO.NB *)
and[equal[P[fix[x_]],union[domain[LEAST[x_]],set[0]]],PARTIALORDER[x_]] := WELLORDER[x]

(* derived 2004 July 18 in WO-PO.NB *)
and[equal[P[fix[x_]],union[domain[LEAST[x_]],set[0]]],TOTALORDER[x_]] := WELLORDER[x]

(* added 2001 November 15 *)
and[equal[set[x_],y_],member[y_,V]] := equal[set[x],y]

(* added 2002 January 1 based on PAIR.NB *)
and[equal[set[x_],set[y_]],member[x_,V]] := and[equal[x,y],member[x,V]]

(* added 2000 October 4 based on NONEMPTY.LOG *)
and[equal[x_,y_],subclass[x_,y_]] := equal[x,y]

(* added 2001 November 16 based on INVERSE.NB *)
and[equal[x_,y_],subclass[y_,x_]] := equal[x,y]

(* added 2002 September 10 based on IMV-RULE.NB *)
and[equal[x_,y_],subclass[x_,union[y_,z_]]] := equal[x,y]

(* derived 2003 January 3 in OO-SUC-OM.NB *)
and[equal[succ[x_],succ[y_]],member[x_,omega]] := and[equal[x,y],member[x,omega]]

(* derived 204 August 22 in PARTREC.NB *)
and[equal[V,domain[x_]],member[x_,V]] := False

(* added 2001 November 22 based on THIN.NB *)
and[equal[V,domain[VERTSECT[x_]]],FUNCTION[x_]] := FUNCTION[x]

(* added 2001 November 27 based on IN-SS.NB *)
and[equal[V,domain[VERTSECT[x_]]],FUNCTION[composite[Id,x_]]] := 
                                           FUNCTION[composite[Id,x]]

(* added 2001 November 15 based on EQ-V.NB *)
and[equal[V,x_],equal[x_,y_]] := and[equal[V,x],equal[V,y]]

(* added 2001 November 15 based on EQ-V.NB *)
and[equal[V,x_],equal[y_,x_]] := and[equal[V,x],equal[V,y]]

(* added 2002 September 10 based on IMV-RULE.NB *)
and[equal[V,x_],equal[V,union[x_,y_]]] := equal[V,x]

(* added 2001 November 15 based on EQ-V.NB *)
and[equal[V,x_],member[x_,y_]] := False

(* added 2001 November 15 based on EQ-V.NB *)
and[equal[V,x_],subclass[x_,y_]] := and[equal[V,x],equal[V,y]]

(* added 2001 November 15 based on EQ-V.NB *)
and[equal[V,x_],subclass[y_,x_]] := equal[V,x]

(* added 2002 September 7 based on REPLACE.NB *)
and[equal[V,union[x_,y_]],member[x_,V],member[y_,V]] := False

(* derived 2004 October 26 in AXCH.NB *)
and[equal[V,union[x_,set[y_]]],not[member[y_,x_]]] := equal[x,complement[set[y]]]

(* derived 2004 April 1 in EQV-EQ.NB *)
and[EQUIVALENCE[x_],FUNCTION[x_]] := subclass[x,Id]

(* derived 2004 December 5 in MAP-CO.NB *)
and[FUNCTION[composite[Id,z_]],subclass[z_,cart[x_,y_]]] := and[FUNCTION[z],subclass[z,cart[x,y]]]

(* derived 2004 November 12 in SETPFUNP.NB *)
and[FUNCTION[x_],member[funpart[x_],y_]] := and[FUNCTION[x],member[x,y]]

(* derived 2004 March 18 in RFX-WRAP.NB *)
and[FUNCTION[x_],REFLEXIVE[x_]] := subclass[x,Id]

(* derived 2004 November 12 in SETPFUNP.NB *)
and[FUNCTION[setpart[x_]],member[x_,y_]] := and[FUNCTION[x],member[x,y]]

(* derived 2004 December 5 in REPLACE.NB *)
and[FUNCTION[x_],subclass[x_,cart[V,V]]] := FUNCTION[x]

(* derived 2005 February 6 in DESCEND.NB *)
and[member[0,x_],member[x_,DESCENDING]] := False

(* derived 2004 June 19 in X14--.NB *)
and[member[complement[x_],V],member[intersection[x_,y_],V]] := and[member[y,V],member[complement[x],V]]

(* derived 2005 January 27 in DK-SU.NB *)
and[member[x_,DEDEKIND],member[pair[x_,omega],Q]] := False

(* derived 2005 January 27 in FINITE.NB *)
and[member[x_,FINITE],member[pair[x_,omega],Q]] := False

(* derived 2004 October 30 in MEMB-CO.NB *)
and[member[first[w_],y_],member[pair[first[w_],second[w_]],x_]] := and[member[w,x],member[first[w],y]]

(* revised 2003 June 2 based on SETHOOD.NB *)
and[member[first[x_],y_],not[member[x_,V]]] := False

(* added 2002 November 3 based on FLIP.NB *)
and[member[first[x_],V],member[first[second[x_]],y_]] := member[first[second[x]],y]

(* added 2001 November 16 based on INVERSE.NB *)
and[member[first[x_],V],member[second[x_],y_]] := member[second[x],y]

(* derived 2004 August 18 in X3080.NB *)
and[member[x_,y_],member[domain[x_],V]] := member[x,y]

(* derived 2004 August 18 in X3080.NB *)
and[member[x_,y_],member[fix[x_],V]] := member[x,y]

(* added 2002 October 8 based on INVAR-I.NB *)
and[member[x_,y_],member[intersection[x_,z_],V]] := member[x,y]

(* derived 2005 April 28 in NATORDER.NB *)
and[member[x_,y_],member[y_,nat[z_]],not[member[x_,nat[z_]]]] := False

(* derived 2005 May 26 in DIV-I.NB *)
and[member[y_,x_],member[pair[x_,y_],DIV]] := and[equal[0,y],member[x,omega],not[equal[0,x]]]

(* derived 2004 August 18 in X3080.NB *)
and[member[x_,y_],member[range[x_],V]] := member[x,y]

(* derived 2004 August 18 in X3080.NB *)
and[member[x_,y_],member[rotate[x_],V]] := member[x,y]

and[member[x_,y_],member[x_,V]] := member[x,y]

(* derived 2005 February 13 in NAT.NB *)
and[member[y_,nat[x_]],member[nat[x_],y_]] := False

(* derived 2005 July 4 in SUCC-NAT.NB *)
and[member[x_,nat[y_]],member[succ[x_],nat[y_]]] := member[succ[x],nat[y]]

(* derived 2005 April 26 in TRICHOT.NB *)
and[member[x_,nat[y_]],not[equal[x_,nat[y_]]]] := member[x,nat[y]]

(* derived 2005 July 4 in SUCC-NAT.NB *)
and[member[x_,nat[y_]],not[equal[nat[y_],succ[x_]]]] := member[succ[x],nat[y]]

(* derived 2005 April 26 in TRICHOT.NB *)
and[member[x_,nat[y_]],not[member[nat[y_],x_]]] := member[x,nat[y]]

(* derived 2005 July 4 in SUCC-NAT.NB *)
and[member[x_,nat[y_]],not[member[succ[x_],nat[y_]]]] := equal[nat[y],succ[x]]

(* derived 2005 April 28 in NATORDER.NB *)
and[member[x_,nat[y_]],not[subclass[x_,nat[y_]]]] := False

(* derived 2005 June 27 in NAT-SUCC.NB *)
and[member[x_,nat[y_]],subclass[x_,nat[y_]]] := member[x,nat[y]]

(* derived 2005 April 28 in NATORDER.NB *)
and[member[x_,nat[y_]],subclass[nat[y_],x_]] := False

(* derived 2005 April 28 in NATORDER.NB *)
and[member[nat[x_],y_],subclass[y_,nat[x_]]] := False

(* added 2001 November 15 based on UNWRAP-1.NB *)
and[member[x_,y_],not[member[x_,V]]] := False

(* derived 2005 May 17 in DIVRULES.NB *)
and[member[x_,omega],member[y_,image[inverse[DIV],succ[x_]]]] := and[member[x,omega],member[y,omega]]

(* derived 2005 June 7 in O7COR1.NB *)
and[member[x_,omega],member[x_,y_],member[y_,omega]] := and[member[x,y],member[y,omega]]

(* derived 2005 April 26 in DICHOT.NB *)
and[member[x_,omega],member[nat[y_],x_],not[subclass[nat[y_],x_]]] := False

(* derived 2005 March 29 in DIV-SUB.NB *)
and[member[x_,omega],member[pair[x_,y_],DIV]] := member[pair[x,y],DIV]

(* derived 2005 March 29 in DIV-SUB.NB *)
and[member[y_,omega],member[pair[x_,y_],DIV]] := member[pair[x,y],DIV]

(* derived 2005 May 25 in MOD-A.NB *)
and[member[y_,omega],member[pair[x_,natsub[y_,z_]],DIV]] := member[pair[x,natsub[y,z]],DIV]

(* derived 2005 May 25 in MOD-A.NB *)
and[member[z_,omega],member[pair[x_,natsub[y_,z_]],DIV]] := member[pair[x,natsub[y,z]],DIV]

(* derived 2005  February 16 in X3730-38.NB *)
and[member[x_,OMEGA],member[U[x_],OMEGA]] := member[x,OMEGA]

(* derived 2005 February 19 in ITR-OM-E.NB *)
and[member[x_,omega],not[equal[0,intersection[omega,x_]]]] := and[member[x,omega],not[equal[0,x]]]

(* derived 2005 January 3 in ZERO.NB *)
and[member[x_,omega],not[member[0,x_]]] := equal[0,x]

(* derived 2005 February 17 in X3741-49.NB *)
and[member[x_,OMEGA],subclass[x_,omega]] := or[equal[omega,x],member[x,omega]]

(* derived 2005  February 16 in X3730-38.NB *)
and[member[x_,OMEGA],subclass[U[x_],x_]] := member[x,OMEGA]

(* derived 2005 January 29 in DIV.NB *)
and[member[pair[x_,y_],DIV],member[pair[y_,x_],DIV]] := and[equal[x,y],member[x,omega]]

(* derived 2005 May 26 in DIV-I.NB *)
and[member[pair[x_,y_],DIV],not[subclass[x_,y_]]] := and[equal[0,y],member[x,omega],not[equal[0,x]]]

(* derived 2005 May 25 in MOD-A.NB *)
and[member[pair[x_,natsub[y_,z_]],DIV],subclass[z_,y_]] := member[pair[x,natsub[y,z]],DIV]

(* derived 2005 January 21 in SS-A.NB *)
and[member[x_,range[SINGLETON]],not[equal[0,x_]]] := member[x,range[SINGLETON]]

(* added 2003 June 2 based on SETHOOD.NB *)
and[member[second[x_],y_],not[member[x_,V]]] := False

(* derived 2004 May 4 in ALLCLOSED.NB *)
and[member[y_,z_],subclass[y_,domain[VERTSECT[x_]]]] := and[member[y,z],member[image[x,y],V]]

(* derived 2005 January 15 in HILBERT.NB *)
and[member[x_,y_],subclass[P[x_],x_]] := False

(* derived 2004 May 4 in ALLCLOSED.NB *)
and[member[y_,z_],subclass[P[y_],domain[VERTSECT[x_]]]] := and[member[y,z],member[image[x,P[y]],V]]

(* added 2001 November 15 *)
and[member[x_,y_],subclass[y_,set[x_]]] := and[equal[set[x],y],member[x,V]]

(* added 2001 June 28 based on SETHOOD.NB *)
and[member[x_,V],member[complement[x_],V]] := False

(* added 2001 June 28 based on SETHOOD.NB *)
and[member[x_,V],member[domain[x_],V]] := member[x,V]

(* added 2002 November 3 based on FIRST.NB *)
and[member[x_,V],member[first[x_],y_]] := member[first[x],y]

(* added 2002 June 22 based on X-RO-ASS.NB *)
and[member[x_,V],member[first[first[x_]],V]] := member[first[first[x]],V]

(* derived 2004 March 29 based on HULL.NB *)
and[member[y_,V],member[hull[x_,y_],z_]] := member[hull[x,y],z]

(* derived 2004 August 1 in THINNESS.NB *)
and[member[y_,V],member[image[trv[x_],y_],V]] := member[iterate[x,y],V]

(* derived 2004 June 19 in X14--.NB *)
and[member[x_,V],member[intersection[y_,complement[x_]],V]] := and[member[x,V],member[y,V]]

(* derived 2004 April 18 in REPLACE.NB *)
and[member[x_,V],member[intersection[y_,P[x_]],V]] := member[x,V]

(* added 2003 January 25 based on INVAR.NB *)
and[member[x_,V],member[invar[x_],V]] := False

(* added 2002 October 15 based on MEMBER.NB *)
and[member[u_,V],member[pair[u_,v_],composite[x_,y_]]] := member[pair[u,v],composite[x,y]]

(* added 2002 October 15 based on MEMBER.NB *)
and[member[v_,V],member[pair[u_,v_],composite[x_,y_]]] := member[pair[u,v],composite[x,y]]

(* derived 2005 January 27 in DIV.NB *)
and[member[x_,V],member[pair[x_,y_],DIV]] := member[pair[x,y],DIV]

(* derived 2005 January 27 in DIV.NB *)
and[member[y_,V],member[pair[x_,y_],DIV]] := member[pair[x,y],DIV]

(* derived 2005 January 7 in CARD-K.NB *)
and[member[x_,V],member[pair[x_,y_],K]] := member[pair[x,y],K]

(* derived 2005 January 7 in CARD-K.NB *)
and[member[y_,V],member[pair[x_,y_],K]] := member[pair[x,y],K]

(* derived 2005 January 27 in Q.NB *)
and[member[x_,V],member[pair[x_,y_],Q]] := member[pair[x,y],Q]

(* derived 2005 January 27 in Q.NB *)
and[member[y_,V],member[pair[x_,y_],Q]] := member[pair[x,y],Q]

(* derived 2005 January 27 in ZN.NB *)
and[member[x_,V],member[pair[x_,y_],ZN]] := member[pair[x,y],ZN]

(* derived 2005 January 27 in ZN.NB *)
and[member[y_,V],member[pair[x_,y_],ZN]] := member[pair[x,y],ZN]

(* added 2001 June 28 based on SETHOOD.NB *)
and[member[x_,V],member[range[x_],V]] := member[x,V]

(* added 2002 November 3 based on FIRST.NB *)
and[member[x_,V],member[second[x_],y_]] := member[second[x],y]

(* added 2003 June 29 based on POWER.NB *)
and[member[x_,V],member[U[x_],y_]] := member[U[x],y]

(* added 2001 December 6 based on MEMBER.NB *)
and[member[x_,V],member[y_,V],subclass[x_,y_]] := and[member[y,V],subclass[x,y]]

(* derived 2004 July 22 in REPLACE.NB *)
and[member[x_,V],not[equal[0,y_]],not[member[x_,A[y_]]]] := and[member[x,V],not[member[x,A[y]]]]

(* added 2001 November 14 based on DI.NB *)
and[member[x_,V],not[equal[V,x_]]] := member[x,V]

(* derived 2004 September 23 in WF-LEX.NB *)
and[member[x_,V],subclass[x_,image[wf[y_],x_]]] := equal[0,x]

(* added 2002 May 14 based on IND-C.NB *)
and[member[x_,V],subclass[x_,omega]] := subclass[x,omega]

(* derived 2004 July 25 in CANTOR.NB *)
and[member[x_,V],subclass[P[domain[funpart[x_]]],range[funpart[x_]]]] := False

(* added 2003 June 5 based on REG.NB *)
and[member[x_,V],subclass[x_,REGULAR]] := member[x,REGULAR]

(* added 2001 November 15 *)
and[member[x_,V],subclass[x_,set[y_]]] := subclass[x,set[y]]

(* derived 2005 June 28 in O-MUL.NB *)
and[not[equal[0,nat[x_]]],not[member[set[0],nat[x_]]]] := equal[nat[x],set[0]]

(* derived 2005 May 17 in NATRULES.NB *)
and[not[equal[0,nat[x_]]],subclass[nat[x_],set[0]]] := equal[nat[x],set[0]]

(* derived 2004 July 22 in REPLACE.NB *)
and[not[equal[0,y_]],not[subclass[x_,A[y_]]]] := not[subclass[x,A[y]]]

(* derived 2005 April 26 in TRICHOT.NB *)
and[not[equal[nat[x_],nat[y_]]],not[member[nat[x_],nat[y_]]]] := member[nat[y],nat[x]]

(* derived 2005 February 13 in NAT.NB *)
and[not[member[nat[x_],nat[y_]]],not[member[nat[y_],nat[x_]]]] := equal[nat[x],nat[y]]

(* derived 2004 July 25 in CANTOR.NB *)
and[not[member[x_,V]],not[member[x_,y_]]] := not[member[x,V]]

(* added 2003 October 7 based on WF-IND.NB *)
and[not[member[x_,V]],not[member[first[x_],V]]] := not[member[x,V]]

(* derived 2005 April 7 in WF-TO.NB *)
and[PARTIALORDER[x_],subclass[cart[fix[x_],fix[x_]],union[x_,inverse[x_]]]] := TOTALORDER[x]

(* derived 2004 March 18 in RFX-WRAP.NB *)
and[REFLEXIVE[composite[Id,x_]],subclass[x_,cart[V,V]]] := REFLEXIVE[x]

(* derived 2004 March 18 in RFX-TRV.NB *)
and[REFLEXIVE[composite[Id,x_]],TRANSITIVE[x_]] := and[REFLEXIVE[x],TRANSITIVE[x]]

(* derived 2004 March 18 in RFX-TRV.NB *)
and[REFLEXIVE[x_],subclass[x_,cart[V,V]]] := REFLEXIVE[x]

(* derived 2004 March 21 in PO-WRAP.NB *)
and[REFLEXIVE[x_],subclass[intersection[x_,inverse[x_]],Id],TRANSITIVE[x_]] := PARTIALORDER[x]

(* derived 2004 March 18 in RFX-TRV.NB *)
and[REFLEXIVE[x_],TRANSITIVE[composite[Id,x_]]] := and[REFLEXIVE[x],TRANSITIVE[x]]

(* added 2001 November 17 based on EQ.NB *)
and[subclass[x_,cart[V,z_]],subclass[x_,cart[y_,V]]] := subclass[x,cart[y,z]]

(* added 2003 September 21 based on RFX-CORE.NB *)
and[subclass[x_,cart[V,V]],subclass[x_,cart[y_,z_]]] := subclass[x,cart[y,z]]

(* added 2001 March 4 based on SU-IN.NB *)
and[subclass[x_,cart[V,V]],subclass[inverse[x_],y_]] := subclass[x,inverse[y]] 

(* derived 2004 March 18 in RFX-TRV.NB *)
and[subclass[x_,cart[V,V]],TRANSITIVE[composite[Id,x_]]] := TRANSITIVE[x]

(* derived 2004 March 18 in RFX-TRV.NB *)
and[subclass[x_,cart[V,V]],TRANSITIVE[x_]] := TRANSITIVE[x]

(* added 2003 October 7 based on WF-IND.NB *)
and[subclass[x_,cart[V,V]],WELLFOUNDED[composite[Id,x_]]] := WELLFOUNDED[x]

(* added 2003 July 6 based on ASSOCDEF.NB *)
and[subclass[composite[u_,cross[v_,Id],inverse[ASSOC]],composite[x_,cross[y_,z_]]],
    subclass[image[inverse[v_],domain[domain[u_]]],cart[V,V]]] := 
    subclass[composite[u,cross[v,Id]],composite[x,cross[y,z],ASSOC]]

(* added 2001 December 20 based on SUBST-2.NB *)
and[subclass[composite[Id,x_],y_],subclass[composite[Id,y_],x_]] := 
                                  equal[composite[Id,x],composite[Id,y]]

(* added 2002 October 25 based on ROTATE.NB *)
and[subclass[composite[x_,id[w_]],y_],
    subclass[composite[y_,id[w_]],x_]] :=
    equal[composite[x,id[w]],composite[y,id[w]]]

(* derived 2004 March 18 in RFX-WRAP.NB *)
and[subclass[domain[x_],fix[x_]],subclass[range[x_],fix[x_]]] := REFLEXIVE[composite[Id,x]]

(* added 2001 April 27 based on MAP2.NB *)
and[subclass[z_,FUNS],subclass[image[IMAGE[FIRST],z_],set[x_]]] := subclass[z,map[x,V]]

(* derived 2004 April 20 in ID-REVU.NB *)
and[subclass[x_,Id],subclass[y_,Id],subclass[domain[x_],domain[y_]]] := and[subclass[x,y],subclass[y,Id]]

(* added 2001 April 27 based on MAP2.NB *)
and[subclass[image[IMAGE[id[cart[V,V]]],z_],FUNS],
             subclass[U[z_],cart[V,V]]] := subclass[z,FUNS]

(* added 2003 November 2 based on CHARHULL.NB *)
and[subclass[x_,image[inverse[S],y_]],subclass[y_,image[inverse[S],x_]]] := 
    equal[image[inverse[S],x],image[inverse[S],y]]

(* added 2002 January 3 based on COMPOSE.NB *)
and[subclass[intersection[x_,z_],y_],subclass[intersection[y_,z_],x_]] := 
    equal[intersection[x,z],intersection[y,z]]

(* derived 2004 March 20 in EQV-WRAP.NB *)
and[subclass[inverse[x_],x_],TRANSITIVE[x_]] := EQUIVALENCE[x]

(* derived 2004 March 20 in EQV-WRAP.NB *)
and[subclass[x_,inverse[x_]],TRANSITIVE[x_]] := EQUIVALENCE[x]

(* derived 2004 March 20 in EQV-WRAP.NB *)
and[subclass[x_,inverse[x_]],TRANSITIVE[composite[Id,x_]]] := EQUIVALENCE[x]

(* derived 2004 December 27 in TRV-RS.NB *)
and[subclass[inverse[x_],x_],TRANSITIVE[composite[Id,x_]]] := EQUIVALENCE[composite[Id,x]]

(* added 2001 April 27 based on MAP2.NB *)
and[subclass[z_,map[x_,V]],subclass[U[z_],cart[V,y_]]] := subclass[z,map[x,y]]

(* derived 2005 February 10 in X3557.NB *)
and[subclass[x_,omega],subclass[image[BIGCUP,x_],x_]] := or[equal[omega,x],member[x,omega]]

(* derived 2005 February 10 in X3557.NB *)
and[subclass[x_,omega],subclass[image[inverse[SUCC],x_],x_]] := or[equal[omega,x],member[x,omega]]

(* derived 2005 February 10 in X3557.NB *)
and[subclass[x_,omega],subclass[image[inverse[SUCC],intersection[omega,x_]],x_]] := or[equal[omega,x],member[x,omega]]

(* added 2001 November 17 based on EQ.NB *)
and[subclass[P[x_],y_],subclass[U[y_],x_]] := equal[P[x],y]

and[subclass[x_,y_],subclass[y_,x_]] := equal[x,y]

(* derived 2004 August 7 in RS-1.NB *)
and[subclass[x_,y_],subclass[x_,cart[V,V]],subclass[composite[y_,id[domain[x_]]],x_]] := equal[x,composite[y,id[domain[x]]]]

(* derived 2004 December 25 in SELCO-LT.NB *)
and[subclass[x_,y_],subclass[composite[Id,x_],y_]] := subclass[x,y]

(* added 2001 December 19 based on INV-IM.NB *)
and[subclass[x_,y_],subclass[intersection[x_,y_],z_]] := and[subclass[x,y],subclass[x,z]]

(* derived 2004 July 23 in X23--.NB *)
and[subclass[x_,y_],subclass[intersection[x_,z_],y_]] := subclass[x,y]

(* added 2002 October 3 based on MONOSUB2.NB *)
and[subclass[x_,y_],subclass[x_,z_],subclass[y_,z_]] := and[subclass[x,y],subclass[y,z]]

(* added 2001 November 16 *)
and[subclass[z_,x_],subclass[z_,y_],
    subclass[intersection[x_,y_],z_]] := equal[intersection[x,y],z]

(* added 2001 November 17 based on EQ.NB *)
and[subclass[x_,z_],subclass[y_,z_],subclass[z_,union[x_,y_]]] := equal[union[x,y],z]

(* derived 2005 January 5 in TC-HC.NB *)
and[subclass[x_,y_],subclass[U[x_],H[y_]]] := subclass[x,H[y]]

(* derived 2005 April 7 in WF-TO.NB *)
and[TOTALORDER[x_],WELLFOUNDED[intersection[Di,x_]]] := WELLORDER[x]

(* added 2002 January 17 based on ANTISYM1.NB *)
ANTISYMMETRIC[x_] := and[subclass[x,cart[V,V]],subclass[intersection[x,inverse[x]],Id]]

(* Definition DF-AP in AP1.DEM *)
apply[x_,y_] := U[image[x,set[y]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[0,x_] := V

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[ACLOSURE,x_] := union[Aclosure[x],complement[image[V,set[x]]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[ADJOIN[x_],y_] := union[x,y,
      complement[image[V,set[x]]],complement[image[V,set[y]]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[BIGCAP,x_] := union[A[x],complement[image[V,set[x]]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[BIGCUP,x_] := union[complement[image[V,set[x]]],U[x]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[CAP,PAIR[x_,y_]] := union[complement[image[V,set[x]]],complement[image[V,set[y]]],intersection[x,y]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[CARD,x_] := union[card[x],complement[image[V,intersection[OMEGA,image[Q,set[x]]]]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[cart[x_,y_],z_] := union[A[y],complement[image[V,intersection[x,set[z]]]]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[CART,PAIR[x_,y_]] := union[cart[x,y],complement[image[V,set[x]]],complement[image[V,set[y]]]]

(* derived 2005 August 16 in AP-E-S.NB *)
APPLY[complement[E],x_] := complement[image[V,set[x]]]

(* derived 2005 August 16 in AP-E-S.NB *)
APPLY[complement[inverse[E]],x_] := complement[image[V,set[x]]]

(* derived 2005 August 16 in AP-E-S.NB *)
APPLY[complement[inverse[S]],x_] := complement[image[V,set[x]]]

(* derived 2005 August 16 in AP-E-S.NB *)
APPLY[complement[S],x_] := union[complement[image[V,x]],complement[image[V,set[x]]]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[COMPOSE,PAIR[x_,y_]] := union[complement[image[V,set[x]]],complement[image[V,set[y]]],composite[x,y]]

(* added 2003 October 28 based on APPLY.NB *)
APPLY[composite[x_,y_],z_] := A[image[x,image[y,set[z]]]]

(* derived 2004 April 17 in REPLACE.NB *)
APPLY[CORE[x_],y_] := union[complement[image[V,set[y]]],core[x,y]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[CROSS,PAIR[x_,y_]] := union[complement[image[V,set[x]]],complement[image[V,set[y]]],cross[x,y]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[cross[funpart[u_],funpart[v_]],PAIR[x_,y_]] := PAIR[APPLY[funpart[u],x],APPLY[funpart[v],y]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[CUP,PAIR[x_,y_]] := union[x,y,complement[image[V,set[x]]],complement[image[V,set[y]]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[Di,x_] := complement[image[V,set[x]]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[DIF,PAIR[x_,y_]] := union[complement[image[V,set[x]]],complement[image[V,set[y]]],intersection[x,complement[y]]]

(* derived 2004 December 10 in AP-IMG.NB *)
APPLY[DORA,x_] := union[complement[image[V,set[x]]],PAIR[domain[x],range[x]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[DUP,x_] := PAIR[x,x]

(* derived 2005 August 16 in AP-E-S.NB *)
APPLY[E,x_] := union[complement[image[V,set[x]]],set[x]]

(* derived 2004 May 12 in EQUIV.NB *)
APPLY[EQUIV,x_] := union[complement[image[V,set[x]]],eqv[x]]

(* derived 2005 August 7 in FACT-AP.NB *)
APPLY[FACTORIAL,0] := set[0]

(* derived 2005 August 7 in FACT-AP.NB *)
APPLY[FACTORIAL,set[0]] := set[0]

(* derived 2005 August 7 in FACT-AP.NB *)
APPLY[FACTORIAL,succ[set[0]]] := succ[set[0]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[FIRST,PAIR[x_,y_]] := union[x,complement[image[V,set[x]]],complement[image[V,set[y]]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[FUNPART,x_] := union[complement[image[V,set[x]]],funpart[x]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[HC,x_] := union[complement[image[V,set[x]]],H[x]]

(* revised 2004 March 29 based on HULL.NB *)
APPLY[HULL[x_],y_] := hull[x,y]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[Id,x_] := union[x,complement[image[V,set[x]]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[id[x_],y_] := union[y,complement[image[V,intersection[x,set[y]]]]]

(* derived 2004 December 10 in AP-IMG.NB *)
APPLY[IMAGE[x_],y_] := union[complement[image[V,set[y]]],complement[image[V,set[image[x,y]]]],image[x,y]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[image[inverse[NATADD],set[x_]],y_] := natsub[x,y]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[IMG,PAIR[x_,y_]] := union[complement[image[V,set[x]]],complement[image[V,set[y]]],image[x,y]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[INTADD,PAIR[x_,y_]] := intadd[x,y]

(* added 2004 July 14 based on X2530-41.NB *)
APPLY[inverse[DUP],x_] := union[first[x],
      image[V,intersection[complement[first[x]],second[x]]],
      image[V,intersection[complement[second[x]],first[x]]]]

(* derived 2005 August 16 in AP-E-S.NB *)
APPLY[inverse[E],x_] := union[A[x],complement[image[V,set[x]]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[inverse[plus[x_]],y_] := natsub[y,x]

(* derived 2005 August 16 in AP-E-S.NB *)
APPLY[inverse[S],x_] := complement[image[V,set[x]]]

(* derived 2004 July 17 in AP-IN-SG.NB *)
APPLY[inverse[SINGLETON],x_] := union[A[x],complement[image[V,intersection[range[SINGLETON],set[x]]]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[LAMBHULL,x_] := union[complement[image[V,set[x]]],HULL[x]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[LEFT[x_],y_] := PAIR[x,y]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[MAP,PAIR[x_,y_]] := union[complement[image[V,set[x]]],complement[image[V,set[y]]],map[x,y]]

(* derived 2005 July 18 in MODULO.NB *)
APPLY[modulo[x_],y_] := natmod[y,x]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[NATADD,PAIR[x_,y_]] := natadd[x,y]

(* derived 2005 May 17 based on NATMOD.NB *)
APPLY[NATMOD,PAIR[x_,y_]] := natmod[x,y]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[NATMUL,PAIR[x_,y_]] := natmul[x,y]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[PAIRSET,PAIR[x_,y_]] := union[complement[image[V,set[x]]],complement[image[V,set[y]]],set[x,y]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[PLUS,x_] := union[complement[image[V,intersection[omega,set[x]]]],plus[x]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[plus[x_],y_] := natadd[x,y]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[POWER,x_] := union[complement[image[V,set[x]]],P[x]]

(* derived 2005 August 17 in PRIMESEQ.NB *)
APPLY[PRIMESEQ,0] := succ[set[0]]

(* derived 2005 August 17 in PRIMESEQ.NB *)
APPLY[PRIMESEQ,set[0]] := succ[succ[set[0]]]

(* derived 2005 August 17 in PRIMESEQ.NB *)
APPLY[PRIMESEQ,succ[set[0]]] := succ[succ[succ[succ[set[0]]]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[RANK,x_] := union[complement[image[V,intersection[REGULAR,set[x]]]],rank[x]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[RC[x_],y_] := union[complement[image[V,set[x]]],
      image[V,intersection[y,complement[x]]],intersection[x,complement[y]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[RCF,x_] := union[complement[image[V,set[x]]],RC[x]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[RIGHT[x_],y_] := PAIR[y,x]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[rotate[w_],PAIR[x_,y_]] :=  APPLY[image[inverse[w],set[x]],y]

(* added 2003 October 28 based on APPLY.NB *)
APPLY[S,x_] := union[x,complement[image[V,set[x]]]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[SECOND,PAIR[x_,y_]] := union[y,complement[image[V,set[x]]],complement[image[V,set[y]]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[SINGLETON,x_] := union[complement[image[V,set[x]]],set[x]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[SUBVAR,x_] := union[complement[image[V,set[x]]],subvar[x]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[SUCC,x_] := union[complement[image[V,set[x]]],succ[x]]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[SWAP,PAIR[x_,y_]] := PAIR[y,x]

(* derived 2004 August 17 in AP-PAIR.NB *)
APPLY[SYMDIF,PAIR[x_,y_]] := union[complement[image[V,set[x]]],complement[image[V,set[y]]],
                                   intersection[x,complement[y]],intersection[y,complement[x]]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[TC,x_] := union[complement[image[V,set[x]]],tc[x]]

(* derived 2005 July 17 in TIMES.NB *)
APPLY[times[x_],y_] := natmul[x,y]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[UCLOSURE,x_] := union[complement[image[V,set[x]]],Uclosure[x]]

(* added 2003 October 28 based on APPLY.NB *)
APPLY[union[x_,y_],z_] := intersection[APPLY[x,z],APPLY[y,z]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[V,x_] := complement[image[V,set[x]]]

(* derived 2005 January 25 *)
APPLY[VERTSECT[x_],y_] := union[complement[image[V,set[y]]],complement[image[V,set[image[x,set[y]]]]],image[x,set[y]]]

(* derived 2004 August 10 in RS-3.NB *)
APPLY[VERTSECT[RESTRICT],x_] := union[complement[image[V,set[x]]],RS[x]]

(* added 2003 November 13 based on APPLY-SP.NB *)
APPLY[VS,x_] := union[complement[image[V,set[x]]],composite[VERTSECT[x],id[domain[x]]]]

(* derived 2004 September 25 in LAMB-WF.NB *)
APPLY[WFPART,x_] := union[complement[image[V,set[x]]],wf[x]]

(* derived 2004 November 16 in XS.NB *)
APPLY[XS,x_] := union[complement[image[V,set[x]]],X[x]]

(* assertions *)
assert[p_] := Module[{w = Unique[]},equal[V,class[w,p]]]

(* added 2003 July 1 based on ASSOC.NB *)
associative[0] := True

(* added 2003 July 1 based on ASSOC.NB *)
associative[CAP] := True

(* added 2003 July 1 based on ASSOC.NB *)
associative[cart[cart[x_,x_],y_]] := True

(* derived 2005 July 30 in CATORELN.NB *)
associative[CATOFUNS] := True

(* derived 2005 July 30 in CATORELN.NB *)
associative[CATORELN] := True

(* added 2003 July 1 based on ASSOC.NB *)
associative[COMPOSE] := True

(* added 2003 July 20 based on DIRECT12.NB *)
associative[composite[CART,cross[IMAGE[FIRST],IMAGE[SECOND]]]] := True

(* derived 2004 December 3 in TRVASSOC.NB *)
associative[composite[COMPOSE,cross[IMAGE[id[trv[x_]]],IMAGE[id[trv[x_]]]]]] := True

(* derived 2004 December 2 in PRECISE.NB *)
associative[composite[COMPOSE,id[composite[inverse[IMAGE[SECOND]],IMAGE[FIRST]]]]] := True

(* derived 2005 July 30 in CATORELN.NB *)
associative[composite[cross[COMPOSE,FIRST],TWIST]] := True

(* added 2003 August 9 based on ASS-ADDZ.NB *)
associative[composite[cross[NATADD,NATADD],TWIST]] := True

(* derived 2004 December 7 in ASV-DIV.NB *)
associative[composite[FIRST,id[x_]]] := and[subclass[composite[x,inverse[x]],x],TRANSITIVE[composite[Id,x]]]

(* added 2003 July 1 based on IN-DUP.NB *)
associative[composite[id[x_],inverse[DUP]]] := True

(* derived 2005 July 22 in MOD-ASS.NB *)
associative[composite[modulo[x_],NATADD]] := True

(* derived 2005 July 22 in MOD-ASS.NB *)
associative[composite[modulo[x_],NATADD,id[cart[x_,x_]]]] := True

(* derived 2005 July 22 in MOD-ASS.NB *)
associative[composite[modulo[x_],NATMUL]] := True

(* derived 2005 July 22 in MOD-ASS.NB *)
associative[composite[modulo[x_],NATMUL,id[cart[x_,x_]]]] := True

(* added 2003 July 7 based on PRGPOID.NB *)
associative[composite[RIF,cross[SWAP,SWAP]]] := True

(* derived 2004 December 7 in ASV-DIV.NB *)
associative[composite[SECOND,id[x_]]] := and[subclass[composite[inverse[x],x],x],TRANSITIVE[composite[Id,x]]]

(* added 2003 July 1 based on ASS-TRV.NB *)
associative[composite[x_,SWAP]] := associative[composite[x,id[cart[V,V]]]]

(* added 2003 July 13 based on ASS-1X2.NB *)
associative[composite[SWAP,cross[x_,y_]]] := associative[cross[y,x]]

(* added 2003 July 7 based on PRGPOID.NB *)
associative[composite[SWAP,RIF]] := True

(* derived 2004 December 3 in TRVASSOC.NB *)
associative[composite[SWAP,RIF,id[cart[trv[x_],trv[x_]]]]] := True

(* added 2003 July 13 based on ASS-1X2.NB *)
associative[cross[FIRST,SECOND]] := True

(* added 2003 July 13 based on ASS-1X2.NB *)
associative[cross[SECOND,FIRST]] := False

(* added 2003 July 1 based on ASSOC.NB *)
associative[CUP] := True

(* added 2003 July 1 based on ASSOC.NB *)
associative[FIRST] := True

(* added 2003 July 1 based on ASSOC.NB *)
associative[Id] := False

(* added 2003 August 9 based on ASS-ADDZ.NB *)
associative[INTADD] := True

(* added 2003 July 1 based on IN-DUP.NB *)
associative[inverse[DUP]] := True

(* added 2003 July 1 based on ASSOC.NB *)
associative[NATADD] := True

(* added 2003 July 1 based on ASSOC.NB *)
associative[NATMUL] := True

(* added 2003 July 7 based on PRGPOID.NB *)
associative[RIF] := False

(* added 2003 July 1 based on ASSOC.NB *)
associative[SECOND] := True

(* added 2003 July 1 based on ASSOC.NB *)
associative[SYMDIF] := True

(* added 2003 July 1 based on ASSOC.NB *)
associative[V] := False

(* added 2003 May 23 based on BINCLOSE.NB *)
binclosed[0] := V

(* added 2003 May 23 based on BINCLOSE.NB *)
binclosed[cart[x_,y_]] := union[cliques[complement[x]],image[S,set[y]]]

(* added 2003 May 23 based on BINCLOSE.NB *)
binclosed[composite[Id,x_]] := binclosed[x]

(* added 2003 May 23 based on BINCLOSE.NB *)
binclosed[composite[x_,id[cart[V,V]]]] := binclosed[x]

(* added 2003 May 21 based on BINCLOSE.NB *)
binclosed[composite[x_,inverse[DUP]]] := invar[x]

(* added 2003 May 23 based on BCL-TRV.NB *)
binclosed[composite[x_,inverse[IMAGE[DUP]],E]] := invar[composite[x,E]]

(* added 2003 May 23 based on BINCLOSE.NB *)
binclosed[composite[SWAP,RIF]] := 
          image[inverse[IMAGE[id[cart[V,V]]]],TRV]

(* added 2003 May 23 based on BINCLOSE.NB *)
binclosed[FIRST] := V

(* added 2003 May 23 based on BINCLOSE.NB *)
binclosed[inverse[DUP]] := V

(* derived 2004 May 2 in REGULAR.NB *)
binclosed[REGULAR] := P[complement[REGULAR]]

(* added 2003 May 23 based on BINCLOSE.NB *)
binclosed[SECOND] := V

(* added 2003 May 23 based on BINCLOSE.NB *)
binclosed[union[x_,y_]] := intersection[binclosed[x],binclosed[y]]

(* added 2003 May 23 based on BINCLOSE.NB *)
binclosed[V] := set[0]

(* Definition DF-CA in DF-FP-5 *)
cantor[z_] := intersection[complement[fix[composite[inverse[E],z]]],
                           domain[z]]

(* revised 2003 May23 based on DEF-CLOS.NB *)
CAPclosed := binclosed[CAP]

(* added 2001 December 1 based on CARD-X.NB *)
card[0] := 0

(* added 2001 December 10 based on CARD-ALL.NB *)
card[card[x_]] := card[x]

(* derived 2005 July 22 in CARD-MUL.NB *)
card[cart[nat[x_],nat[y_]]] := natmul[nat[x],nat[y]]

(* derived 2005 July 22 in CARD-MUL.NB *)
card[cart[x_,set[y_]]] := intersection[card[x],image[V,set[y]]]

(* derived 2004 January 10 in CARD-FUN.NB *)
card[domain[funpart[x_]]] := card[funpart[x]]

(* derived 2004 January 10 in CARD-FUN.NB *)
card[id[x_]] := card[x]

(* derived 2004 January 10 in CARD-FUN.NB *)
card[intersection[x_,image[V,y_]]] := intersection[card[x],image[V,y]]

(* derived 2005 April 27 in CARDRANK.NB *)
card[nat[x_]] := nat[x]

(* derived 2005 July 16 in DBLCOUNT.NB *)
card[natadd[x_,y_]] := natadd[x,y]

(* derived 2005 August 6 in CARD-NAT.NB *)
card[natmod[x_,y_]] := natmod[x,y]

(* derived 2005 August 6 in CARD-NAT.NB *)
card[natmul[x_,y_]] := natmul[x,y]

(* derived 2005 August 6 in CARD-NAT.NB *)
card[natsub[x_,y_]] := natsub[x,y]

(* added 2002 May 29 based on ALEPH0.NB *)
card[omega] := omega

(* derived 2005 January 11 in SET-SUCC.NB *)
card[P[succ[set[0]]]] := succ[succ[succ[set[0]]]]

(* derived 2004 January 10 in CARD-FUN.NB *)
card[plus[x_]] := intersection[omega,image[V,intersection[omega,set[x]]]]

(* derived 2005 August 17 in PRIMESEQ.NB *)
card[PRIMES] := omega

(* derived 2004 January 10 in CARD-FUN.NB *)
card[RC[x_]] := intersection[card[P[x]],image[V,set[x]]]

(* added 2001 December 1 based on CARD-X.NB *)
card[set[0]] := set[0]

(* derived 2005 January 7 in CARD-ONE.NB *)
card[set[x_]] := intersection[image[V,set[x]],set[0]]

(* derived 2005 January 7 in CARD-OM.NB *)
card[succ[omega]] := omega

(* added 2001 December 2 based on CARD-FUN.NB *)
card[union[x_,complement[image[V,set[y_]]]]] := 
     union[card[x],complement[image[V,set[y]]]]

(* Theorem CP-3A in CP1 *)
cart[x_,0] := 0

(* Theorem CP-3B in CP1 *)
cart[0,x_] := 0

(* Theorem IMV-CP01 in IM2 proved 1998 July 21 *)
cart[complement[image[V,x_]],y_] := 
                cart[V,intersection[complement[image[V,x]],y]]

(* Theorem IMV-CP02 in IM2 proved 1998 July 21 *)
cart[domain[x_],image[V,x_]] := cart[domain[x],V]

(* Theorem IM-V-CP in IM2 proved 1998 February 5 *)
cart[x_,image[V,x_]] := cart[x,V]

(* Theorem IMV-CP03 in IM2 proved 1998 July 22 *)
cart[image[z_,x_],image[V,x_]] := cart[image[z,x],V]

(* Theorem IMV-CP04 in IM2 proved 1998 July 22 *)
cart[image[z_,x_],intersection[y_,image[V,x_]]] := cart[image[z,x],y]

(* Theorem IMV-CP05 in IM2 proved 1998 July 22 *)
cart[image[V,x_],y_] := cart[V,intersection[image[V,x],y]]

(* added 2001 November 22 based on CP-I-IMV.NB *)
cart[intersection[x_,complement[image[V,y_]]],z_] := 
     cart[x,intersection[z,complement[image[V,y]]]]

(* Theorem IMV-CP06 in IM2 proved 1998 July 22 *)
cart[x_,intersection[y_,image[V,x_]]] := cart[x,y]

(* Theorem IMV-CP07 in IM2 proved 1998 July 22 *)
cart[intersection[x_,image[V,y_]],z_] := 
                        cart[x,intersection[image[V,y],z]]

(* added 2002 October 22 based on CO-ID.NB *)
cart[inverse[x_],intersection[y_,image[V,domain[x_]]]] := cart[inverse[x],y]

(* Theorem IMV-CP08 in IM2 proved 1998 July 22 *)
cart[range[x_],image[V,x_]] := cart[range[x],V]

(* dangerous rule found 2002 January 1 in PAIR-MEM.NB 
   replaced with temporary rules for A[...]
cart[set[x_],set[y_]] := set[PAIR[x,y]]
*)

(* added 2001 November 29 based on CO-SS.NB *)
cart[union[x_,intersection[y_,complement[image[V,z_]]]],w_] := 
     union[cart[x,w],cart[y,intersection[w,complement[image[V,z]]]]]

(* added 2001 November 29 based on CO-SS.NB *)
cart[union[x_,intersection[y_,image[V,z_]]],w_] := 
     union[cart[x,w],cart[y,intersection[w,image[V,z]]]]

(* introduced 2004 October 26 in AXCH.NB *)
choicefunction[x_,y_] := and[FUNCTION[x],subclass[x,inverse[E]],equal[domain[x],y]]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[0] := set[0]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[cart[x_,y_]] := P[intersection[x,y]]

(* added 2000 December 9 based on MORECLIQ.NB *)
cliques[complement[cart[x_,y_]]] := union[P[complement[x]],P[complement[y]]]

(* corrected 2002 June 4 *)
cliques[complement[composite[inverse[x_],x_]]] := P[complement[domain[x]]]

(* added 2000 December 14 based on CLIQUES.NB *)
cliques[complement[composite[x_,inverse[x_]]]] := P[complement[range[x]]]

(* derived 2004 January 13 in RA-RCF.NB *)
cliques[complement[cross[x_,complement[inverse[y_]]]]] := 
        cliques[complement[cross[inverse[x],complement[y]]]]

(* added 2000 December 9 based on REPLACE.NB *)
cliques[complement[cross[Di,Id]]] := image[inverse[IMAGE[SWAP]],FUNS]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[complement[cross[Id,Di]]] := 
        image[inverse[IMAGE[id[cart[V,V]]]],FUNS]

(* added 2000 December 17 based on Q.NB *)
cliques[complement[E]] := fix[composite[DISJOINT,BIGCUP]]

(* added 2000 December 17 based on Q.NB *)
cliques[complement[inverse[x_]]] := cliques[complement[x]]

(* added 2000 December 17 based on Q.NB *)
cliques[complement[Q]] := set[0]

(* derived 2004 May 2 in REGULAR.NB *)
cliques[complement[REGULAR]] := P[complement[REGULAR]]

(* added 2000 December 17 based on Q.NB *)
cliques[complement[S]] := set[0]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[composite[Id,x_]] := cliques[x]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[composite[id[x_],y_]] := intersection[cliques[y],P[x]]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[composite[x_,id[y_]]] := intersection[cliques[x],P[y]]

(* added 2001 December 31 based on DORA-DJ.NB *)
cliques[composite[inverse[SECOND],Di,FIRST]] := 
        intersection[image[inverse[DORA],DISJOINT],P[cart[V,V]]]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[Di] := set[0]

(* revised 2002 April 18 based on REPLACE.NB *)
cliques[DISJOINT] := succ[set[0]]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[Id] := union[range[SINGLETON],set[0]]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[id[x_]] := union[image[SINGLETON,x],set[0]]

(* added 2003 October 8 based on FS-CUP.NB *)
cliques[image[inverse[CUP],FUNS]] := image[inverse[BIGCUP],FUNS]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[intersection[x_,y_]] := intersection[cliques[x],cliques[y]]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[inverse[x_]] := cliques[x]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[PS] := set[0]

(* derived 2004 May 2 in REGULAR.NB *)
cliques[REGULAR] := REGULAR

(* added 2000 December 14 based on CLIQUES.NB *)
cliques[S] := union[range[SINGLETON],set[0]]

(* added 2002 January 17 based on ANTISYM3.NB *)
cliques[union[cart[Id,V],composite[Di,SWAP,id[Di]]]] := ANTISYM

(* added 2002 January 18 based on THINRULE.NB *)
cliques[union[x_,complement[cart[y_,y_]]]] := 
        image[inverse[IMAGE[id[y]]],cliques[x]]

(* added 2002 April 23 based on TRICHOT.NB *)
cliques[union[E,inverse[S]]] := cliques[union[S,inverse[E]]]

(* added 2000 December 9 based on CLIQUES.NB *)
cliques[V] := V

(* derived 2004 December 21 in COMUTANT.NB *)
commutant[0] := V

(* derived 2004 December 21 in COMUTANT.NB *)
commutant[composite[Id,x_]] := commutant[x]

(* derived 2004 December 21 in COMUTANT.NB *)
commutant[E] := P[complement[cart[V,V]]]

(* derived 2004 December 21 in COMUTANT.NB *)
commutant[Id] := V

(* derived 2004 December 21 in COMUTANT.NB *)
commutant[id[x_]] := P[intersection[complement[cart[x,complement[x]]],complement[cart[complement[x],x]]]]

(* derived 2004 December 21 in COMUTANT.NB *)
commutant[inverse[x_]] := image[inverse[IMAGE[SWAP]],commutant[x]]

(* derived 2004 December 21 in COMUTANT.NB *)
commutant[S] := P[complement[cart[V,V]]]

(* derived 2004 December 21 in COMUTANT.NB *)
commutant[V] := P[complement[cart[V,V]]]

(* added 2001 May 18 *)
commute[x_,y_] := equal[composite[x,y],composite[y,x]]

(* Theorem C-2A in C1 *)
complement[0] := V

(* from ADJ-C.LOG *)
complement[ADJOIN[x_]] := union[complement[cart[V,image[V,set[x]]]],
                    composite[Di,ADJOIN[x]]]

(* Theorem BA-DI2 in BIGCAP/BA1 proved 1998 December 11 *)
complement[BIGCAP] := union[complement[cart[complement[set[0]],V]],
                            composite[Di,BIGCAP]]

(* Theorem BC-C in BIGCUP/BC proved 1998 December 12 *)
complement[BIGCUP] := union[complement[cart[V,V]],
                            composite[Di,BIGCUP]]

(* Theorem C-1 in C1 *)
complement[complement[x_]] := x

(* derived 2004 April 22 in PSM-VS.NB *)
complement[composite[complement[E],x_]] := union[complement[cart[V,V]],composite[S,VERTSECT[x]]]

(* added 2002 October 22 based on C-CO-X.NB *)
complement[composite[cross[w_,composite[id[x_],y_]],z_]] :=
     union[complement[cart[V,cart[V,x]]],complement[composite[cross[w,y],z]]]

(* added 2002 October 22 based on C-CO-X.NB *)
complement[composite[cross[composite[id[w_],x_],y_],z_]] :=
     union[complement[cart[V,cart[w,V]]],complement[composite[cross[x,y],z]]]

(* added 2002 October 22 based on C-CO-X.NB *)
complement[composite[w_,cross[x_,composite[y_,id[z_]]]]] :=
     union[complement[cart[cart[V,z],V]],complement[composite[w,cross[x,y]]]]

(* added 2002 October 22 based on C-CO-X.NB *)
complement[composite[w_,cross[composite[x_,id[y_]],z_]]] :=
     union[complement[cart[cart[y,V],V]],complement[composite[w,cross[x,z]]]]

(* added 2000 November 26 based on GLB-LUB.NB
complement[composite[x_,inverse[E]]] := 
           union[complement[cart[V,V]],UB[complement[x]]]
*)

(* added 2000 November 14 based on MAX.NB *)
complement[composite[complement[x_],inverse[E]]] := 
                               union[complement[cart[V,V]],UB[x]]

(* Theorem DJT-DEF in DJT proved 1998 July 27 *)
complement[composite[E,inverse[E]]] := 
                  union[complement[cart[V,V]],DISJOINT]

(* removed 2000 November 7
complement[cross[x_,y_]] := union[complement[cart[cart[V,V],cart[V,V]]],
                  composite[inverse[FIRST],complement[x],FIRST],
                  composite[inverse[SECOND],complement[y],SECOND]]
*)

(* added 2002 October 22 based on C-CO-X.NB *)
complement[cross[composite[id[w_],x_],y_]] :=
     union[complement[cart[V,cart[w,V]]],complement[cross[x,y]]]

(* added 2002 October 22 based on C-CO-X.NB *)
complement[cross[w_,composite[id[x_],y_]]] :=
     union[complement[cart[V,cart[V,x]]],complement[cross[w,y]]]

(* added 2002 October 22 based on C-CO-X.NB *)
complement[cross[x_,composite[y_,id[z_]]]] :=
     union[complement[cart[cart[V,z],V]],complement[cross[x,y]]]

(* added 2002 October 22 based on C-CO-X.NB *)
complement[cross[composite[x_,id[y_]],z_]] :=
     union[complement[cart[cart[y,V],V]],complement[cross[x,z]]]

(* Theorem DI-C-ID in DI added 1998 July 2 *)
complement[Di] := union[Id,complement[cart[V,V]]]

(* Theorem DJT-C2 in DJT *)
complement[DISJOINT] := union[composite[E,inverse[E]],        
                              complement[cart[V,V]]]

(* added 1998 July 2 *)
complement[DUP] := union[complement[cart[V,Id]],
                         composite[DUP,Di]]

(* added 1998 July 2 *)
complement[FIRST] := union[complement[cart[cart[V,V],V]],
                           composite[Di,FIRST]]

(* added 1998 February 7 *)
complement[fix[E]] := RUSSELL

(* added 1998 July 2 *)
complement[id[x_]] := union[complement[cart[x,x]],composite[id[x],Di,id[x]]]

(* Theorem DI-ID-C in DI added 1998 July 2 *)
complement[Id] := union[Di,complement[cart[V,V]]]


(* added 1998 July 2; revised 1999 July 14; removed 2000 November 7
complement[IMAGE[z_]] := union[
         complement[cart[P[domain[VERTSECT[z]]],range[IMAGE[z]]]],
         composite[id[range[IMAGE[z]]],Di,IMAGE[z]]]
*)

(* Theorem C-4B in C1 *)
complement[intersection[x_,y_]] := union[complement[x],complement[y]]

(* added 1998 August 11 *)
complement[inverse[BIGCAP]] := 
          union[complement[cart[V,complement[set[0]]]],
                            composite[inverse[BIGCAP],Di]]

(* added 1998 July 2 *)
complement[inverse[BIGCUP]] := union[complement[cart[V,V]],
                               composite[inverse[BIGCUP],Di]]

(* added 1998 July 2 *)
complement[inverse[DUP]] := union[complement[cart[Id,V]],
                                  composite[Di,inverse[DUP]]]

(* added 1998 July 2 *)
complement[inverse[FIRST]] := union[complement[cart[V,cart[V,V]]],
                              composite[inverse[FIRST],Di]]

(* added 2000 November 23 based on VS-3.NB *)
complement[inverse[LB[x_]]] := union[complement[cart[V,V]],
                                     composite[E,complement[x]]]

(* added 1998 August 11 *)
complement[inverse[POWER]] := union[complement[cart[V,V]],
                              composite[inverse[POWER],Di]]

(* added 2002 May 25 based on ON-SUC-1.NB *)
complement[inverse[PS]] := union[Id,complement[inverse[S]]]

(* added 1998 July 2 *)
complement[inverse[SECOND]] := union[complement[cart[V,cart[V,V]]],
                              composite[inverse[SECOND],Di]]

(* added 1998 July 3 *)
complement[inverse[SINGLETON]] := union[complement[cart[V,V]],
                            composite[inverse[SINGLETON],Di]]

(* revised 2002 November 26 based on C-SUCC.NB *)
complement[inverse[SUCC]] := 
           union[complement[cart[range[SUCC],V]],composite[inverse[SUCC],Di]]

(* added 2000 November 7 based on UB-1.NB *)
complement[inverse[UB[x_]]] := union[complement[cart[V,V]],
                                     composite[E,complement[inverse[x]]]]

(* added 2000 November 7 based on LB-2.NB *)
complement[LB[x_]] := union[complement[cart[V,V]],
                            composite[complement[inverse[x]],inverse[E]]]

(* added 1998 August 11 *)
complement[POWER] := union[complement[cart[V,V]],composite[Di,POWER]]

(* Theorem PS-C1 in PS1 proved 1998 November 28 *)
complement[PS] := union[Id,complement[S]]

(* Theorem RUS-C in RUS/1 *)
complement[RUSSELL] := fix[E]

(* added 1998 July 2 *)
complement[SECOND] := union[complement[cart[cart[V,V],V]],
                            composite[Di,SECOND]]

(* Theorem AP-DI-SG proved 1998 December 16 *)
complement[SINGLETON] := union[complement[cart[V,V]],
                               composite[Di,SINGLETON]]

(* revised 2002 November 26 based on C-SUCC.NB *)
complement[SUCC] := union[complement[cart[V,range[SUCC]]],composite[Di,SUCC]]

(* added 1998 July 2; removed 2002 November 26 based on SWAP-DI.NB
complement[SWAP] := union[complement[cart[cart[V,V],cart[V,V]]],
                          composite[id[cart[V,V]],Di,SWAP]]
*)

(* added 2000 November 7 based on UB-1.NB *)
complement[UB[x_]] := union[complement[cart[V,V]],
                            composite[complement[x],inverse[E]]]

(* Theorem C-4A in C1 *)
complement[union[x_,y_]] := intersection[complement[x],complement[y]]

(* Theorem C-2B in C1 *)
complement[V] := 0

(* Theorem CO-0A in CO1 *) 
composite[0,x_] := 0

(* Theorem CO-0B in CO1 *)
composite[x_,0] := 0

(* added 2001 May 10 based on ACLOSURE.NB *)
composite[ACLOSURE,ACLOSURE] := ACLOSURE

(* added 2002 November 20 based on UCL-U.NB *)
composite[ACLOSURE,ADJOIN[set[0]]] := composite[ADJOIN[set[0]],ACLOSURE]

(* added 2001 October 15 based on ACL-IMS.NB *)
composite[ACLOSURE,CLIQUES] := CLIQUES

(* derived 2005 February 17 in NAT-ACL.NB *)
composite[ACLOSURE,id[omega]] := id[omega]

(* derived 2005 February 17 in NAT-ACL.NB *)
composite[ACLOSURE,id[OMEGA]] := id[OMEGA]

(* added 2003 May 19 based on CAPCLOSE.NB *)
composite[ACLOSURE,IMAGE[CAP],CART,DUP] := ACLOSURE

(* added 2003 May 18 based on ACL-SQ.NB *)
composite[ACLOSURE,IMAGE[CART],IMAGE[DUP]] := 
          composite[IMAGE[CART],IMAGE[DUP],ACLOSURE]

(* added 2001 October 2 based on IMS.NB *)
composite[ACLOSURE,IMAGE[inverse[S]]] := IMAGE[inverse[S]]

(* added 2003 May 19 based on ACL-IPOW.NB *)
composite[ACLOSURE,IMAGE[POWER]] := composite[IMAGE[POWER],ACLOSURE]

(* added 2001 May 10 based on ACLOSURE.NB *)
composite[ACLOSURE,POWER] := POWER

(* added 2002 April 8 based on UCL-ACL.NB *)
composite[ACLOSURE,SINGLETON] := SINGLETON

(* derived 2004 August 10 in RS-3.NB *)
composite[ACLOSURE,VERTSECT[RESTRICT]] := VERTSECT[RESTRICT]

(* added 1999 November 3 based on CURRY.NB *)
composite[ADJOIN[x_],ADJOIN[y_]] := ADJOIN[union[x,y]]

(* added 2002 August 18 based on DISTRIB.NB *)
composite[ADJOIN[x_],CAP] := composite[CAP,cross[ADJOIN[x],ADJOIN[x]]]

(* added 2000 September 22 based on LEFT.NB *)
composite[ADJOIN[complement[image[V,set[x_]]]],LEFT[x_]] := LEFT[x]

(* added 2000 September 22 based on LEFT.NB *)
composite[ADJOIN[complement[image[V,set[x_]]]],RIGHT[x_]] := RIGHT[x]

(* added 2001 May 2 based on ADJOIN.NB *)
composite[ADJOIN[x_],complement[inverse[S]]] := 
          composite[id[image[S,set[x]]],complement[inverse[S]]]

(* added 1999 November 21 based on 1999/NOV/20/CUT-ADJ.NB *)
composite[ADJOIN[x_],id[image[S,set[x_]]]] := id[image[S,set[x]]]

(* added 2003 September 11 based on ID-IMV.NB *)
composite[ADJOIN[x_],y___,id[image[V,set[x_]]]] := composite[ADJOIN[x],y]

(* added 2002 May 24 based on ADJOIN.NB *)
composite[ADJOIN[x_],IMAGE[id[complement[x_]]]] := ADJOIN[x]

(* Theorem ADJ-CO3 in ADJ proved 1999 November 23 *)
composite[ADJOIN[x_],S] := composite[id[image[S,set[x]]],S]

(* added 2002 May 24 based on ADJOIN.NB *)
composite[ADJOIN[set[0]],id[omega],SUCC] := composite[id[omega],SUCC]

(* added 2002 May 24 based on ADJOIN.NB *)
composite[ADJOIN[set[0]],IMAGE[SUCC],id[omega]] := composite[id[omega],SUCC]

(* added 2001 May 20 based on IDEA.NB *)
composite[ADJOIN[set[0]],POWER] := POWER

(* added 2002 October 24 based on SUBVAR.NB *)
composite[ADJOIN[set[0]],SUBVAR] := SUBVAR

(* added 2003 May 30 based on RESTRICT.NB *)
composite[ASSOC,cross[cross[x_,y_],z_]] := composite[cross[x,cross[y,z]],ASSOC]

(* added 2002 June 25 based on ASSOC.NB *)
composite[ASSOC,cross[inverse[FIRST],Id]] := cross[Id,inverse[SECOND]]

(* added 2002 June 16 based on LEFT-ROT.NB *)
composite[ASSOC,cross[RIGHT[x_],Id]] := cross[Id,LEFT[x]]

(* added 2002 October 22 based on CO-ID.NB *)
composite[ASSOC,id[cart[cart[V,V],V]]] := ASSOC

(* derived 2004 March 23 in TRV-K.NB *)
composite[ASSOC,id[cart[x_,y_]],inverse[FIRST]] := 
          composite[cross[Id,composite[id[cart[V,y]],inverse[FIRST]]],id[x]]

(* added 1999 October 17 based on ASSOC.2 *)
composite[ASSOC,id[cart[V,V]]] := ASSOC

(* added 1999 November 6 based on CO-4.LOG *)
composite[ASSOC,inverse[FIRST]] := cross[Id,inverse[FIRST]]

(* added 1999 October 31 based on ASSOC.1 *)
composite[ASSOC,inverse[ROT]] := composite[SWAP,ROT]

(* added 1999 November 6 based on CO-4.LOG *)
composite[ASSOC,inverse[SECOND]] := composite[inverse[SECOND],inverse[SECOND]]

(* added 2002 June 16 based on LEFT-ROT.NB *)
composite[ASSOC,LEFT[x_]] := composite[LEFT[first[x]],LEFT[second[x]]]

(* added 1999 November 3 based on ASS-DIF.TXT *)
composite[ASSOC,RIGHT[x_]] := cross[Id,RIGHT[x]]

(* modified 1999 December 15 based on PERMUTE.NB *)
composite[ASSOC,ROT] := composite[SWAP,id[cart[cart[V,V],V]]]

(* added 2001 May 10 based on UCLOS-2.NB *)
composite[BIGCAP,ACLOSURE] := BIGCAP

(* added 2001 May 8 based on BC-BA.NB *)
composite[BIGCAP,CLIQUES] := cart[V,set[0]]

(* Corollary BA-5C in BIGCAP/BA1 proved 1998 December 15 *)
composite[BIGCAP,complement[inverse[S]]] :=
          composite[inverse[S],complement[inverse[E]]]

(* added 1999 December 16 based on BIGCAP.NB *)
composite[BIGCAP,CUP] := union[composite[BIGCAP,inverse[LEFT[0]]],
                               composite[BIGCAP,inverse[RIGHT[0]]],
                               composite[CAP,cross[BIGCAP,BIGCAP]]]

(* Theorem BA-E3 in BIGCAP/BA1 proved 1998 October 1 *)
composite[BIGCAP,E] := inverse[S]

(* added 2002 October 22 based on CO-ID.NB *)
composite[BIGCAP,id[complement[set[0]]]] := BIGCAP

(* derived 2004 December 15 in LB-UB-RS.NB *)
composite[BIGCAP,id[intersection[x_,complement[set[0]]]]] := composite[BIGCAP,id[x]]

(* derived 2005 January 27 in BA-OM.NB *)
composite[BIGCAP,id[omega]] := cart[intersection[omega,complement[set[0]]],set[0]]

(* derived 2005 January 27 in BA-ON.NB *)
composite[BIGCAP,id[OMEGA]] := cart[intersection[OMEGA,complement[set[0]]],set[0]]

(* corrected 1998 August 9 *)
composite[BIGCAP,id[range[POWER]]] := cart[range[POWER],set[0]]

(* added 1998 July 31 *)
composite[BIGCAP,id[range[SINGLETON]]] := inverse[SINGLETON]

(* added 2001 May 2 based on ADJOIN.NB *)
composite[BIGCAP,IMAGE[ADJOIN[x_]]] := composite[ADJOIN[x],BIGCAP]

(* added 1999 September 24 based on BIGCAP.LOG *)
composite[BIGCAP,IMAGE[BIGCAP]] := composite[BIGCAP,BIGCUP]

(* revised 2001 December 24 based on REPLACE.NB *)
composite[BIGCAP,IMAGE[CAP]] := composite[CAP,cross[BIGCAP,BIGCAP],DORA]

(* revised 2001 December 24 based on REPLACE.NB *)
composite[BIGCAP,IMAGE[CART]] := composite[CART,cross[BIGCAP,BIGCAP],DORA]

(* added 2001 April 30 based on CLIQUES2.NB *)
composite[BIGCAP,IMAGE[CLIQUES]] := composite[CLIQUES,BIGCAP]

(* revised 2001 December 24 based on BC-BA.NB *)
composite[BIGCAP,IMAGE[DIF]] := composite[DIF,cross[BIGCAP,BIGCUP],DORA]

(* added 2001 April 10 based on HC-BA.NB *)
composite[BIGCAP,IMAGE[HC]] := composite[HC,BIGCAP]

(* added 2001 March 9 based on IMG-CUT.NB *)
composite[BIGCAP,IMAGE[IMAGE[id[x_]]]] := composite[IMAGE[id[x]],BIGCAP]

(* added 2001 May 3 based on BA-IMG.NB *)
composite[BIGCAP,IMAGE[IMAGE[inverse[DUP]]]] := 
          composite[IMAGE[inverse[DUP]],BIGCAP]

(* added 2001 May 3 based on BA-IMG.NB *)
composite[BIGCAP,IMAGE[IMAGE[inverse[POWER]]]] := 
          composite[IMAGE[inverse[POWER]],BIGCAP]

(* added 2002 February 17 based on IMG-IMG.NB *)
composite[BIGCAP,IMAGE[IMAGE[SWAP]]] := composite[IMAGE[SWAP],BIGCAP]

(* added 2001 May 3 based on BA-IMG.NB *)
composite[BIGCAP,IMAGE[inverse[IMAGE[DUP]]]] := 
          composite[IMAGE[inverse[DUP]],BIGCAP,IMAGE[id[P[Id]]]]

(* added 2000 January 18 based on BIGCAP.NB *)
composite[BIGCAP,IMAGE[inverse[S]]] := 
          cart[complement[set[0]],set[0]]

(* added 1999 September 23 based on BIGCAP.LOG *)
composite[BIGCAP,IMAGE[POWER]] := composite[POWER,BIGCAP]

(* added 2000 January 18 based on BIGCAP.NB *)
composite[BIGCAP,IMAGE[SINGLETON]] := union[id[range[SINGLETON]],
                 cart[intersection[complement[range[SINGLETON]],
                      complement[set[0]]],set[0]]]

(* derived 2004 May 14 in REPLACE.NB *)
composite[BIGCAP,IMAGE[VERTSECT[x_]]] := composite[VERTSECT[UB[x]],IMAGE[id[domain[VERTSECT[x]]]]]

(* added 2003 May 12 based on APPLY.NB *)
composite[BIGCAP,IMG,cross[FUNPART,SINGLETON]] := 
          composite[inverse[SINGLETON],IMG,cross[Id,SINGLETON]]

(* added 2003 June 6 based on ACL-UCL.NB *)
composite[BIGCAP,inverse[ACLOSURE],E] := inverse[S]

(* added 2000 December 20 based on BA-BC.NB *)
composite[BIGCAP,inverse[BIGCUP]] := inverse[S]

(* added 2002 April 10 based on INVAR.NB *)
composite[BIGCAP,inverse[LB[INVAR]]] := INVAR

(* added 2001 May 10 based on UCLOS-1.NB *)
composite[BIGCAP,inverse[S]] := composite[inverse[E],ACLOSURE]

(* added 2002 January 11 based on KURA.NB *)
composite[BIGCAP,KURA] := composite[SINGLETON,FIRST]

(* added 1999 October 6 based on CAP.1 *)
composite[BIGCAP,PAIRSET] := CAP

(* corrected 1998 August 9 *)
composite[BIGCAP,POWER] := cart[V,set[0]]

(* added 1998 July 31 *)
composite[BIGCAP,SINGLETON] := Id

(* added 1998 July 30 *)
composite[BIGCAP,S] := 
          union[cart[set[0],V],composite[inverse[S],BIGCAP]]

(* added 2001 May 8 based on BC-BA.NB *)
composite[BIGCAP,SUBVAR] := cart[V,set[0]]

(* added 2001 May 10 based on UCLOS-1.NB *)
composite[BIGCAP,UCLOSURE] := cart[V,set[0]]

(* added 2002 January 29 based on FUNPART.NB *)
composite[BIGCAP,VERTSECT[x_],id[domain[funpart[x_]]]] := funpart[x]

(* added 2001 September 9 based on ACLOSURE.NB *)
composite[BIGCUP,ACLOSURE] := BIGCUP

(* added 2002 November 19 based on ADJOIN.NB *)
composite[BIGCUP,ADJOIN[x_]] := composite[ADJOIN[U[x]],BIGCUP]

(* added 2002 January 22 based on UCLUCL.NB *)
composite[BIGCUP,BIGCUP,IMAGE[id[P[x_]]],VERTSECT[inverse[BIGCUP]]] := 
    union[cart[union[complement[Uclosure[x]],set[0]],set[0]],id[Uclosure[x]]]

(* added 2001 May 8 based on BC-BA.NB *)
composite[BIGCUP,CLIQUES] := IMAGE[inverse[DUP]]

(* added 2003 July 4 based on COARSER.NB *)
composite[BIGCUP,COARSER] := BIGCUP

(* Theorem POW-C-BC in POW3 proved 1998 December 15 *)
composite[BIGCUP,complement[inverse[S]]] := composite[inverse[POWER],complement[inverse[S]]]

(* added 1999 October 9 based on CUP-LOG.1 *)
composite[BIGCUP,CUP] := composite[CUP,cross[BIGCUP,BIGCUP]]

(* Theorem BC-CO-E2 in BIGCUP/BC proved 1998 February 5 *)
composite[BIGCUP,E] := S

(* derived 2005 February 16 in BC-OM.NB *)
composite[BIGCUP,id[intersection[omega,complement[set[0]]]]] := composite[inverse[SUCC],id[omega]]

(* added 2002 May 25 based on SUCC-ID.NB