% inclusion, disjointness: defFoAs( subseteq(P,Q), z_setminus(P,Q)). defFoAs( supseteq(P,Q), subseteq(Q,P)). defFoAs( 'Disj'(P,Q), z_int(P,Q) ). % right-totality, right-absoluteness, left-absoluteness, % diagonality, functionality, left-uniqueness: defFoAs( 'Tot'( R ), u_rA(R) ). defFoAs( 'RAbs'( R ), is_rA(R) ). % "row-constant" characterization of collection defFoAs( 'LAbs'( R), is_lA(R) ). % "column-constant" characterization of collection defFoAs( 'Coll'( R ), is_diag(R) ). % "subdiagonal" characterization of collection defFoAs( 'RUniq'( R ), z_mult(R) ). % "P is a function" % Alternatively: defFoAs( 'RUniq'( R ), 'Coll'( bros(R) ) ). defFoAs( 'LUniq'( R ), 'Coll'( sibs(R,R) ) ). % "P is the converse of a function" % Alternatively: defFoAs( 'LUniq'( R ), 'RUniq'( rev(R) ) ). % relativization of the above "uniqueness" notions to a domain P: defFoAs( 'RUniq'( P, R ), 'Disj'(mult(R),rA(P)) ). defFoAs( 'LUniq'( P, R ), 'RUniq'(P,rev(R)) ). % "sends-to" and surjectivity properties: defFoAs(sends( R, E, F ), subseteq( circ( E, R ), lA( F ) ) ). defFoAs(isSurj( R, F, E ), subseteq( F, img( circ( E, R ) ) ) ). defThAs(isSurj( R, F ), [% equivalent to isSurj( R, F, id ) 'Coll'( F ), subseteq( F, lA( R ) ) ]). %=== three useful variadic constructs ========== defThAs( equiv([P]), [true(P)] ). defThAs( equiv([P,Q|T]), [equiv(P,Q)|equiv([P|T])]). defThAs( subseteq([P]), [true(P)] ). defThAs( subseteq([P,Q|T]), [subseteq(P,Q)|subseteq([Q|T])]). defThAs( nameLets([]), [] ). defThAs( nameLets([LN,L|T]), [defAs(@(LN),L)|nameLets(T)] ). %=== useful parametric constructs ========== % Two maps, L[eft] and R[ight], are used to navigate "tuples": defAs(th((L,_;one)),L). defAs(th((L,R;incr(I))),circ(th(R,R,I),L)). defAs(succth((L,R;decr(H))),th(L,R,H)). defAs(tuples((R;H)), setminus(int(img(R),dom(th(R,R,H))),dom(succth(R,R,H)))). defAs(sibs((L,R;nil)),u). defAs(sibs((L,R;sng(H))),sibs([succth(L,R,H)])). defAs(sibs((L,R;cons(H,B))),int(sibs([succth(L,R,H)]),sibs(L,R,B))).