%--------------------------------------------------------------% % Author: Dragan Stosic % %--------------------------------------------------------------% TYPE +]: THEORY BEGIN IMPORTING relational_choice[T, U]LEMMA fun_choice IMPLIES parametric_definite_descriptionLEMMA fun_choice IMPLIES rel_unique_choiceLEMMA fun_choice IMPLIES rel_choiceLEMMA IMPLIES rel_choice IMPLIES parametric_definite_descriptionLEMMA IMPLIES rel_choice AND parametric_definite_descriptionLEMMA IMPLIES rel_unique_choice IMPLIES parametric_definite_descriptionLEMMA IMPLIES rel_unique_choice AND parametric_definite_descriptionLEMMA IMPLIES rel_unique_choice IMPLIES fun_choiceLEMMA AND rel_unique_choice IMPLIES fun_choiceLEMMA IMPLIES proof_irrelevance IMPLIES conditional_relational_choiceLEMMA IMPLIES independence_of_premises IMPLIES conditional_relational_choiceTHEOREM IFF rel_unique_choice AND parametric_definite_descriptionEND relational_choice_propertiesquality 89%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
