| products/sources/formale sprachen/PVS/orders/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: non_empty_bounded_sets.pvs Sprache: Unknown
|
(function_props_aux
(inverse_image_composition 0 (inverse_image_composition-1 nil 3449912055 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (expand "inverse_image") (("" (expand "o ") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((T1 formal-type-decl nil function_props_aux nil) (boolean nonempty-type-decl nil booleans nil) (O const-decl "T3" function_props nil) (T3 formal-type-decl nil function_props_aux nil) (inverse_image const-decl "set[D]" function_image nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (T2 formal-type-decl nil function_props_aux nil) (member const-decl "bool" sets nil)) shostak)) (composition_inverse_alt_TCC1 0 (composition_inverse_alt_TCC1-1 nil 3301539767 ("" (skosimp) (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (expand "bijective?") (("" (flatten) (("" (expand "surjective?") (("" (skosimp*) (("" (inst - "r!1") (("" (skosimp) (("" (inst - "x!1") (("" (skosimp) (("" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (T2 formal-type-decl nil function_props_aux nil) (T1 formal-type-decl nil function_props_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (surjective? const-decl "bool" functions nil) (T3 formal-type-decl nil function_props_aux nil)) shostak)) (composition_inverse_alt_TCC2 0 (composition_inverse_alt_TCC2-1 nil 3301539767 ("" (skosimp*) (("" (typepred "f1!1") (("" (expand "bijective?") (("" (expand "surjective?") (("" (flatten) (("" (inst - "r!1") (("" (skosimp) (("" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (T2 formal-type-decl nil function_props_aux nil) (T1 formal-type-decl nil function_props_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (surjective? const-decl "bool" functions nil)) shostak)) (composition_inverse_alt_TCC3 0 (composition_inverse_alt_TCC3-1 nil 3301539767 ("" (skosimp) (("" (typepred "f2!1") (("" (expand "bijective?") (("" (expand "surjective?") (("" (flatten) (("" (skosimp) (("" (inst - "r!1") (("" (skosimp) (("" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (T3 formal-type-decl nil function_props_aux nil) (T2 formal-type-decl nil function_props_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (surjective? const-decl "bool" functions nil)) shostak)) (composition_inverse_alt 0 (composition_inverse_alt-1 nil 3301540008 ("" (skosimp) (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (apply-extensionality :hide? t) (("1" (lemma "composition_bijective[T1,T2,T3]" ("f1" "f1!1" "f2" "f2!1")) (("1" (lemma "unique_bijective_inverse_alt[T1,T3]" ("f" "f2!1 o f1!1" "r" "x!1")) (("1" (lemma "unique_bijective_inverse_alt[T2,T3]" ("f" "f2!1" "r" "x!1")) (("1" (lemma "unique_bijective_inverse_alt[T1,T2]" ("f" "f1!1" "r" "inverse_alt(f2!1)(x!1)")) (("1" (expand "o" 1 2) (("1" (expand "bijective?") (("1" (flatten) (("1" (expand "injective?") (("1" (inst - "inverse_alt(f2!1 o f1!1)(x!1)" "inverse_alt(f1!1)(inverse_alt(f2!1)(x!1))") (("1" (split -4) (("1" (propax) nil nil) ("2" (replace -3) (("2" (expand "o" 1) (("2" (replace -1) (("2" (replace -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-8 1)) (("2" (expand "surjective?") (("2" (flatten) (("2" (skosimp) (("2" (inst - "r!1") (("2" (skosimp) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -6)) (("3" (expand "surjective?") (("3" (skosimp*) (("3" (inst - "r!1") (("3" (skosimp) (("3" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-4 1)) (("4" (expand "surjective?") (("4" (skosimp*) (("4" (inst - "r!1") (("4" (skosimp) (("4" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 1)) (("2" (expand "bijective?") (("2" (expand "surjective?") (("2" (flatten) (("2" (skosimp) (("2" (inst - "r!1") (("2" (skosimp) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "bijective?") (("2" (expand "surjective?") (("2" (flatten) (("2" (skosimp) (("2" (inst - "r!1") (("2" (skosimp) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "bijective?") (("2" (expand "surjective?") (("2" (flatten) (("2" (skosimp) (("2" (inst - "r!1") (("2" (skosimp) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (expand "bijective?") (("2" (expand "surjective?") (("2" (flatten) (("2" (skosimp) (("2" (inst - "r!1") (("2" (skosimp) (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1) (("3" (expand "bijective?") (("3" (expand "surjective?") (("3" (flatten) (("3" (skosimp) (("3" (inst - "r!1") (("3" (skosimp) (("3" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "bijective?") (("4" (expand "surjective?") (("4" (flatten) (("4" (skosimp) (("4" (inst - "r!1") (("4" (skosimp) (("4" (inst - "x!1") (("4" (skosimp) (("4" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (T2 formal-type-decl nil function_props_aux nil) (T1 formal-type-decl nil function_props_aux nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (O const-decl "T3" function_props nil) (inverse_alt const-decl "inverses(f)" function_inverse_alt nil) (inverses nonempty-type-eq-decl nil function_inverse_alt nil) (inverse? const-decl "bool" function_inverse_def nil) (unique_bijective_inverse_alt application-judgement "{d | f(d) = r}" function_inverse_alt nil) (bijective_inverse_alt_is_bijective application-judgement "(bijective?[R, D])" function_inverse_alt nil) (composition_bijective application-judgement "(bijective?[T1, T3])" function_props nil) (composition_surjective application-judgement "(surjective?[T1, T3])" function_props nil) (composition_injective application-judgement "(injective?[T1, T3])" function_props nil) (unique_bijective_inverse_alt judgement-tcc nil function_inverse_alt nil) (injective? const-decl "bool" functions nil) (composition_bijective judgement-tcc nil function_props nil) (T3 formal-type-decl nil function_props_aux nil)) shostak))) [ zur Elbe Produktseite wechseln0.13Quellennavigators Analyse erneut starten ] |