| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 896 B |
|
Quelle fun_below_props.pvs Sprache: PVS |
|||||||||
|
fun_below_props : THEORY
%------------------------------------------------------------------------ % by Bruno Dutertre Royal Holloway & Bedford New College %------------------------------------------------------------------------ BEGIN n, m : VAR nat p : VAR posnat % ----- Cartesian product of {0 ... n-1} and {0 ... m-1} ----- cartesian_bijection : THEOREM (EXISTS (f: [[below[n], below[m]] -> below[n * m]]): bijective?(f)) % ----- Functions from {0 ... n-1} to {0 ... m-1} ----- empty_domain1 : LEMMA (EXISTS (f: [below[0] -> below[m]]): TRUE) empty_domain2 : LEMMA (FORALL (f1, f2: [below[0] -> below[m]]): f1 = f2) empty_range : LEMMA m = 0 IMPLIES (FORALL (f: [below[p]-> below[m]]): FALSE) funset_bijection : THEOREM (EXISTS (f: [[below[n] -> below[m]] -> below[m ^ n]]): bijective?(f)) END fun_below_props ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28