definition let X, Y be set;redefinepredX c= Y means phi_1[X,Y];compatibilityproof thus X c= Y iff phi_1[X,Y]; end; end;

definition let X, Y be set;redefinepredX c= Y means phi_1[X,Y] if C1[X,Y], phi_2[X,Y] if C2[X,Y], phi_3[X,Y] if C3[X,Y] otherwise phi_4[X,Y]; consistency;compatibilityproof thus C1[X,Y] implies (X c= Y iff phi_1[X,Y]); thus C2[X,Y] implies (X c= Y iff phi_2[X,Y]); thus C3[X,Y] implies (X c= Y iff phi_3[X,Y]); thus not C1[X,Y] & not C2[X,Y] & not C3[X,Y] implies (X c= Y iff phi_4[X,Y]); end; end;

definition let X be set;Modes - definiens is being changedredefinemodeSubset of X -> new_type;coherenceproof thus for A being Subset of X holds A is new_type; end; end;

definition let X be set;redefinemodeSubset of X means phi_1[it,X];compatibilityproof let A be set; thus A is Subset of X iff phi_1[A,X]; end; end;

definition let X be set;redefinemodeSubset of X means phi_1[it,X] if G1[X], phi_2[it,X] if G2[X], phi_3[it,X] if G3[X] otherwise phi_4[it,X];compatibilityproof let A be set; thus G1[X] implies (A is Subset of X iff phi_1[A,X]); thus G2[X] implies (A is Subset of X iff phi_2[A,X]); thus G3[X] implies (A is Subset of X iff phi_3[A,X]); thus not G1[X] & not G2[X] & not G3[X] implies (A is Subset of X iff phi_4[A,X]); end; consistency; end;

definition let X be set;redefinefunc+X -> new_type;coherenceproof thus +X is new_type; end; end;

definition let X be set;redefinefunc+Xmeansphi_1[it,X];compatibilityproof let A be set; thus A = +X iff phi_1[A,X]; end; end;

definition let X be set;redefinefunc+Xmeansphi_1[it,X] if G1[X], phi_2[it,X] if G2[X], phi_3[it,X] if G3[X] otherwise phi_4[it,X]; consistency;compatibilityproof let A be set; thus G1[X] implies (A = +X iff phi_1[A,X]); thus G2[X] implies (A = +X iff phi_2[A,X]); thus G3[X] implies (A = +X iff phi_3[A,X]); thus not G1[X] & not G2[X] & not G3[X] implies (A = +X iff phi_4[A,X]); end; end;

definition let X be set;redefinefunc+Xequalstau_1(X);compatibilityproof let A be set; thus A = +X iff A = tau_1(X); end; end;

definition let X be set;redefinefunc+Xequalstau_1(X) if G1[X], tau_2(X) if G2[X], tau_3(X) if G3[X] otherwise tau_4(X); consistency;compatibilityproof let A be set; thus G1[X] implies (A = +X iff A = tau_1(A)); thus G2[X] implies (A = +X iff A = tau_2(A)); thus G3[X] implies (A = +X iff A = tau_3(A)); thus not G1[X] & not G2[X] & not G3[X] implies (A = +X iff A = tau_4(A)); end; end;

definition let X be set;redefineattrX is empty means phi_1[X];compatibilityproof thus X is empty iff phi_1[X]; end; end;

definition let X be set;redefineattrX is empty means phi_1[X] if C1[X], phi_2[X] if C2[X], phi_3[X] if C3[X] otherwise phi_4[X];compatibilityproof thus C1[X] implies (X is empty iff phi_1[X]); thus C2[X] implies (X is empty iff phi_2[X]); thus C3[X] implies (X is empty iff phi_3[X]); thus not C1[X] & not C2[X] & not C3[X] implies (X is empty iff phi_4[X]); end; consistency; end;