Print["CONVERT.M created 1998 September 21 at 10:30 a.m. "] (* Modified 2001 January 23 to run on the Gateway computer *) (* 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[{d},d=Date[]; Print["It is now: ", Part[d,1],Month[Part[d,2]],Part[d,3], " at ", Part[d,4],":",Part[d,5]]] PrintDate[] (* $IterationLimit = $RecursionLimit=20; *) count = 0 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"]] (* New: Definitions of FUNCTION and INDUCTIVE needed for Quaife's axioms. *) (* Rules that must be assigned before attributes are set. *) and[p_] := p or[p_] := p Attributes[and] := {Flat, Orderless, OneIdentity} Attributes[or] := {Flat, Orderless, OneIdentity} composite[x_] := composite[Id,x] intersection[x_] := x union[x_] := x Attributes[composite] := {Flat,OneIdentity} Attributes[intersection] := {Flat, Orderless, OneIdentity} 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] (* definitions of other connectives *) implies[p_,q_] := or[not[p],q] equiv[p_,q_] := and[implies[p,q],implies[q,p]] (* conversion of set theory to equations *) (* rules for conversion of literals *) subclass[x_,y_] := equal[V,union[complement[x],y]] equal[V,V] := True equal[V,0] := False equal[x_,y_] := equal[V,union[intersection[x,y], intersection[complement[x],complement[y]]]] /; Not[V === x] member[x_,y_] := equal[V,image[V,intersection[singleton[x],y]]] (* rules for Boolean operations *) not[equal[V,x_]] := equal[V,image[V,complement[x]]] or[equal[V,x_],equal[V,y_]] := equal[V,union[complement[image[V,complement[x]]], complement[image[V,complement[y]]]]] and[equal[V,x_],equal[V,y_]] := equal[V,intersection[x,y]] (* some predicates *) empty[x_] := equal[0,x] disjoint[x_,y_] := equal[V,union[complement[x],complement[y]]] INDUCTIVE[x_] := and[member[0,x],subclass[image[SUCC,x],x]] SINGVAL[x_] := subclass[composite[x,inverse[x]],Id] FUNCTION[x_] := and[subclass[x,cart[V,V]],SINGVAL[x]] ONEONE[x_] := and[FUNCTION[x],FUNCTION[inverse[x]]] (* simplification rules *) complement[0] := V complement[complement[x_]] := x complement[intersection[x_,y_]] := union[complement[x],complement[y]] complement[union[x_,y_]] := intersection[complement[x],complement[y]] complement[V] := 0 domain[0] := 0 domain[V] := V equal[V,complement[image[V,x_]]] := equal[V,complement[x]] equal[V,image[V,intersection[image[V,x_],image[V,y_]]]] := equal[V,intersection[image[V,x],image[V,y]]] equal[V,intersection[complement[x_],image[V,x_]]] := False equal[V,intersection[x_,image[V,complement[x_]]]] := False equal[V,intersection[x_,complement[image[V,y_]]]] := equal[V,intersection[x,complement[y]]] equal[V,union[intersection[complement[z_],complement[image[V,x_]]], intersection[z_,complement[image[V,x_]]]]] := equal[V,complement[x]] equal[V,union[intersection[complement[image[V,x_]],y_], intersection[complement[image[V,x_]],z_]]] := equal[V,union[intersection[complement[x],y], intersection[complement[x],z]]] image[x_,0] := 0 image[x_,image[V,y_]] := intersection[range[x],image[V,y]] image[x_,complement[image[V,y_]]] := intersection[range[x],complement[image[V,y]]] image[V,image[x_,y_]] := image[V,intersection[domain[x],y]] image[x_,intersection[y_,image[V,z_]]] := intersection[image[x,y],image[V,z]] image[x_,intersection[y_,complement[image[V,z_]]]] := intersection[image[x,y],complement[image[V,z]]] image[x_,union[y_,z_]] := union[image[x,y],image[x,z]] image[x_,V] := range[x] intersection[x_,x_] := x intersection[0,x_] := 0 intersection[complement[x_],x_] := 0 intersection[image[V,x_],x_] := x intersection[union[x_,y_],z_] := union[intersection[x,z],intersection[y,z]] intersection[V,x_] := x range[0] := 0 range[V] := V union[x_,x_] := x union[x_,0] := x union[complement[x_],x_] := V union[complement[x_],complement[image[V,x_]]] := complement[x] union[complement[x_],intersection[x_,y_]] := union[complement[x],y] union[image[x_,y_],image[x_,complement[y_]]] := range[x] union[image[V,x_],x_] := image[V,x] union[image[V,x_],complement[image[V,intersection[x_,y_]]]] := V union[x_,intersection[x_,y_]] := x union[x_,intersection[complement[x_],y_]] := union[x,y] union[intersection[complement[x_],y_,z_],intersection[x_,y_]] := union[intersection[x,y],intersection[y,z]] union[intersection[complement[x_],y_],intersection[x_,y_,z_]] := union[intersection[complement[x],y],intersection[y,z]] union[intersection[complement[x_],complement[y_]], intersection[x_,z_],intersection[y_,z_]] := union[intersection[complement[x],complement[y]],z] union[intersection[complement[x_],z_], intersection[complement[y_],z_],intersection[x_,y_]] := union[intersection[x,y],z] union[intersection[complement[x_],z_],intersection[y_,z_], intersection[y_,x_]] := union[intersection[complement[x],z], intersection[y,x]] union[intersection[complement[x_],y_], intersection[complement[y_],z_],intersection[x_,z_]] := union[intersection[complement[x],y],z] union[V,x_] := V