Predicates

definition
  let X, Y be set;
  pred X = Y means phi_1[X,Y];
end;

definition
  let X, Y be set;
  pred X = 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
  proof
    thus C1[X,Y] & C2[X,Y] implies (phi_1[X,Y] iff phi_2[X,Y]);
    thus C1[X,Y] & C3[X,Y] implies (phi_1[X,Y] iff phi_3[X,Y]);
    thus C2[X,Y] & C3[X,Y] implies (phi_2[X,Y] iff phi_3[X,Y]);
  end;
end;

Modes

definition
  let X be set;
  mode Subset of X -> set means phi[it,X];
  existence
  proof
    thus ex A being set st phi[A,X];
  end;
end;

definition
  let X be set;
  mode Subset of X -> set means
    phi_1[X,it] if C1[X],
    phi_2[X,it] if C2[X],
    phi_3[X,it] if C3[X]
    otherwise phi_4[X,it];
  existence
  proof
    thus C1[X] implies ex A being set st phi_1[X,A];
    thus C2[X] implies ex A being set st phi_2[X,A];
    thus C3[X] implies ex A being set st phi_3[X,A];
    thus not C1[X] & not C2[X] & not C3[X] implies ex A being set st phi_4[X,A];
  end;
  consistency
  proof
    let IT be set;
    thus C1[X] & C2[X] implies (phi_1[X,IT] iff phi_2[X,IT]);
    thus C1[X] & C3[X] implies (phi_1[X,IT] iff phi_3[X,IT]);
    thus C2[X] & C3[X] implies (phi_2[X,IT] iff phi_3[X,IT]);
  end;
end;

Functors

definition
  let X, Y be set;
  func X \/ Y -> set means phi[it,X,Y];
  existence
  proof
    thus ex A being set st phi[A,X,Y];
  end;
  uniqueness
  proof
    thus for A, B being set st phi[A,X,Y] & phi[B,X,Y] holds A = B;
  end;
end;

definition
  let X, Y be set;
  func X \/ Y -> set means
    phi_1[it,X,Y] if C1[X,Y],
    phi_2[it,X,Y] if C2[X,Y],
    phi_3[it,X,Y] if C3[X,Y]
    otherwise phi_4[it,X,Y];
  existence
  proof
    thus C1[X,Y] implies ex A being set st phi_1[A,X,Y];
    thus C2[X,Y] implies ex A being set st phi_2[A,X,Y];
    thus C3[X,Y] implies ex A being set st phi_3[A,X,Y];
    thus not C1[X,Y] & not C2[X,Y] & not C3[X,Y] implies 
         ex A being set st phi_4[A,X,Y]];
  end;
  uniqueness
  proof
    let A, B be set;
    thus C1[X,Y] & phi_1[A,X,Y] & phi_1[B,X,Y] implies A = B;
    thus C2[X,Y] & phi_2[A,X,Y] & phi_2[B,X,Y] implies A = B;
    thus C3[X,Y] & phi_3[A,X,Y] & phi_3[B,X,Y] implies A = B;
    thus not C1[X,Y] & not C2[X,Y] & not C3[X,Y] & 
         phi_4[A,X,Y] & phi_4[B,X,Y] implies A = B;
  end;
  consistency
  proof
    let IT be set;
    thus C1[X,Y] & C2[X,Y] implies (phi_1[IT,X,Y] iff phi_2[IT,X,Y]);
    thus C1[X,Y] & C3[X,Y] implies (phi_1[IT,X,Y] iff phi_3[IT,X,Y]);
    thus C2[X,Y] & C3[X,Y] implies (phi_2[IT,X,Y] iff phi_3[IT,X,Y]);
  end;
end;

definition
  let X, Y be set;
  func X \/ Y -> set equals tau(X,Y);
  coherence
  proof
    thus tau(X,Y) is set;
  end;
end;

definition
  let X, Y be set;
  func X \/ Y -> set equals
    tau_1(X,Y) if C1[X,Y],
    tau_2(X,Y) if C2[X,Y],
    tau_3(X,Y) if C3[X,Y]
    otherwise tau_4(X,Y);
  coherence
  proof
    thus C1[X,Y] implies tau_1(X,Y) is set;
    thus C2[X,Y] implies tau_2(X,Y) is set;
    thus C3[X,Y] implies tau_3(X,Y) is set;
    thus not C1[X,Y] & not C2[X,Y] & not C3[X,Y] implies tau_4(X,Y) is set;
  end;
  consistency
  proof
    let IT be set;
    thus phi_1[X,Y] & phi_2[X,Y] implies (IT = tau_1(X,Y) iff IT = tau_2(X,Y));
    thus phi_1[X,Y] & phi_3[X,Y] implies (IT = tau_1(X,Y) iff IT = tau_3(X,Y));
    thus phi_2[X,Y] & phi_3[X,Y] implies (IT = tau_2(X,Y) iff IT = tau_3(X,Y));
  end;
end;

Attributes

definition
  let X be set;
  attr X is empty means phi[X];
end;

definition
  let X be set;
  attr X 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];
  consistency
  proof
    thus C1[X] & C2[X] implies (phi_1[X] iff phi_2[X]);
    thus C1[X] & C3[X] implies (phi_1[X] iff phi_3[X]);
    thus C2[X] & C3[X] implies (phi_2[X] iff phi_3[X]);
  end;
end;