|
% Additions to standard prelude theory function_inverse_alt
%
% David Lester, Manchester University, NIA, Université Perpignan 8/6/06
function_inverse_alt_aux[D,R:TYPE]: THEORY
BEGIN
ASSUMING
inverse_types: ASSUMPTION (EXISTS (d: D): TRUE) OR (FORALL (r: R): FALSE)
ENDASSUMING
f: VAR [D -> R]
inverse_inverse_alt: LEMMA bijective?[D,R](f) =>
inverse_alt(inverse_alt(f)) = f
END function_inverse_alt_aux
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
