| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis_ax/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
SSL csequence_concatenate_extract.prf
Interaktion und |
|||||||||
|
(csequence_concatenate_extract
(o_extract 0 (o_extract-1 nil 3513610241 ("" (auto-rewrite "o_empty_left") (("" (auto-rewrite "o_empty_right") (("" (induct "fseq" :name "is_finite_induction") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp*) (("3" (ground) (("1" (expand "^") (("1" (assert) nil nil)) nil) ("2" (expand "^" +) (("2" (smash) (("1" (inst - "i!1 - 1" "j!1 - 1" "k!1 - 1") (("1" (assert) nil nil)) nil) ("2" (rewrite "o_add") (("2" (decompose-equality) nil nil)) nil) ("3" (rewrite "o_add") (("3" (decompose-equality 5) (("3" (inst - "i!1" "j!1 - 1" "k!1 - 1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (o_add formula-decl nil csequence_concatenate nil) (o_empty_left formula-decl nil csequence_concatenate nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt nil) (csequence_add_extensionality formula-decl nil csequence_codt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (add_finite application-judgement "nonempty_finite_csequence[T]" csequence_concatenate_extract nil) (o_nonempty_left application-judgement "nonempty_csequence" csequence_concatenate_extract nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (o_empty_right formula-decl nil csequence_concatenate nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (o_finite application-judgement "finite_csequence" csequence_concatenate_extract nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (is_finite_induction formula-decl nil csequence_props nil) (T formal-type-decl nil csequence_concatenate_extract nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ def-decl "finite_csequence" csequence_extract nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (O const-decl "csequence" csequence_concatenate nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (is_finite inductive-decl "bool" csequence_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (o_extract_eta 0 (o_extract_eta-1 nil 3513610334 ("" (skosimp) (("" (lemma "o_extract") (("" (inst - "fseq!1" 0 "i!1" "j!1") (("" (assert) (("" (replace -1) (("" (rewrite "extract_def" 1) (("" (expand "^" +) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((o_extract formula-decl nil csequence_concatenate_extract nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (o_finite application-judgement "finite_csequence" csequence_concatenate_extract nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty_finite_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (extract_def formula-decl nil csequence_extract nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ def-decl "finite_csequence" csequence_extract nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_concatenate_extract nil)) shostak))) ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.2Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28