| products/Sources/formale Sprachen/PVS/algebra/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: trig_inverses.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(finite_groups
(IMP_group_TCC1 0 (IMP_group_TCC1-1 nil 3407081817 ("" (lemma "fullset_is_group") (("" (propax) nil nil)) nil) ((fullset_is_group formula-decl nil finite_groups nil)) nil)) (finite_generated_by 0 (finite_generated_by-1 nil 3306144725 ("" (skosimp*) (("" (lemma "generated_is_subgroup" ("a" "a!1" "G" "G!1")) (("" (assert) (("" (expand "subgroup?") (("" (assert) (("" (typepred "G!1") (("" (expand "finite_group?") (("" (flatten) (("" (lemma "finite_subset[T]") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((one formal-const-decl "T" finite_groups nil) (* formal-const-decl "[T, T -> T]" finite_groups nil) (T formal-nonempty-type-decl nil finite_groups nil) (finite_group nonempty-type-eq-decl nil group nil) (finite_group? const-decl "bool" group_def nil) (group nonempty-type-eq-decl nil group nil) (group? const-decl "bool" group_def nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (generated_is_subgroup formula-decl nil group nil) (subgroup? const-decl "bool" group_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (is_finite const-decl "bool" finite_sets nil) (G!1 skolem-const-decl "finite_group[T, *, one]" finite_groups nil) (generated_by const-decl "group" group nil) (finite_set type-eq-decl nil finite_sets nil) (finite_subset formula-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil)) shostak)) (finite_generated_by_def_TCC1 0 (finite_generated_by_def_TCC1-1 nil 3293285775 ("" (skosimp*) (("" (lemma "finite_generated_by") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((finite_generated_by formula-decl nil finite_groups nil) (member const-decl "bool" sets nil) (finite_group nonempty-type-eq-decl nil group nil) (finite_group? const-decl "bool" group_def nil) (one formal-const-decl "T" finite_groups nil) (* formal-const-decl "[T, T -> T]" finite_groups nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil finite_groups nil)) shostak)) (finite_generated_by_def 0 (finite_generated_by_def-2 nil 3407237397 ("" (skosimp*) (("" (case "S!1(a!1)") (("1" (assert) (("1" (typepred "G!1") (("1" (expand "finite_group?") (("1" (flatten) (("1" (lemma "finite_subset" ("s" "S!1" "A" "G!1")) (("1" (assert) (("1" (lemma "nonempty_card" ("S" "S!1")) (("1" (flatten -1) (("1" (hide -2) (("1" (case-replace "nonempty?(S!1)") (("1" (name "X" "{t: T | EXISTS (n: posnat): n <= card(S!1) AND t = a!1 ^ n}") (("1" (replace -1) (("1" (case "subset?(X,S!1)") (("1" (name "N" "card(S!1)") (("1" (replace -1) (("1" (case "FORALL (n:posnat): n < N => a!1^n /= one") (("1" (case "FORALL (i,j:posnat): i <= N & j <= N & i /= j => a!1^i /= a!1^j") (("1" (lemma "card_bij" ("S" "X" "N" "N")) (("1" (case "(EXISTS (f: [(X) -> below[N]]): bijective?(f))") (("1" (replace -1 -2) (("1" (flatten -2) (("1" (lemma "same_card_subset" ("A" "X" "B" "S!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (name "F" "LAMBDA (n: below[N]): IF n = 0 THEN a!1 ^ N ELSE a!1 ^ n ENDIF") (("2" (case "bijective?[below[N],(X)](F)") (("1" (lemma "bijective_inverse_exists[below[N],(X)]" ("f" "F")) (("1" (expand "exists1") (("1" (flatten) (("1" (skolem!) (("1" (lemma "bij_inv_is_bij_alt[below[N],(X)]" ("f" "F" "g" "x!1")) (("1" (inst + "x!1") nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide 2) (("2" (expand "F" 1) (("2" (assert) (("2" (hide-all-but (-2 -3 -4 1)) (("2" (expand "bijective?") (("2" (split) (("1" (expand "injective?") (("1" (skosimp*) (("1" (case-replace "x1!1=0") (("1" (assert) (("1" (inst -3 "N" "x2!1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case-replace "x2!1=0") (("1" (inst - "x1!1" "N") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst - "x1!1" "x2!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (expand "X" -1) (("2" (skolem!) (("2" (flatten) (("2" (expand "<=" -1) (("2" (split -1) (("1" (replace -2) (("1" (inst + "n!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -5) (("2" (replace -2) (("2" (replace -1) (("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (hide 2) (("3" (expand "X" 1) (("3" (expand "F" 1) (("3" (skosimp*) (("3" (replace -4) (("3" (typepred "x1!1") (("3" (case-replace "x1!1=0") (("1" (inst + "N") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst + "x1!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "generated_is_subgroup" ("a" "a!1" "G" "G!1")) (("2" (expand "subgroup?") (("2" (assert) (("2" (lemma "finite_subset" ("s" "X" "A" "S!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (lemma "trichotomy" ("x" "i!1-j!1")) (("2" (split -1) (("1" (lemma "cancel_right" ("z" "a!1^(-j!1)" "x" "a!1^i!1" "y" "a!1^j!1")) (("1" (rewrite "expt_mult" -1) (("1" (rewrite "expt_mult" -1) (("1" (assert) (("1" (inst - "i!1-j!1") (("1" (assert) (("1" (rewrite "expt_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (lemma "cancel_right" ("z" "a!1^(-i!1)" "x" "a!1 ^ i!1" "y" "a!1 ^ j!1")) (("3" (rewrite "expt_mult" -1) (("3" (rewrite "expt_mult" -1) (("3" (assert) (("3" (inst - "j!1-i!1") (("3" (assert) (("3" (rewrite "expt_0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "subset?(S!1,X)") (("1" (lemma "subset_antisymmetric" ("a" "S!1" "b" "X")) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (replace -6 1 rl) (("2" (expand "generated_by") (("2" (assert) (("2" (replace -14 -1) (("2" (simplify -1) (("2" (skolem!) (("2" (typepred "n!1") (("2" (case "EXISTS (k:below[N],j:int): i!1 = j*n!1+k") (("1" (skolem!) (("1" (typepred "k!1") (("1" (case-replace "k!1=0") (("1" (replace -3 -5) (("1" (lemma "expt_expt" ("a" "a!1" "i" "n!1" "j" "j!1")) (("1" (replace -8 -1) (("1" (assert) (("1" (replace -1 * rl) (("1" (replace -6) (("1" (inst + "n!1") (("1" (assert) (("1" (rewrite "one_expt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2 -4) (("2" (lemma "expt_expt" ("a" "a!1" "i" "n!1" "j" "j!1")) (("2" (replace -7) (("2" (assert) (("2" (rewrite "expt_mult" -5 :dir rl) (("2" (replace -1 * rl) (("2" (assert) (("2" (inst + "k!1") (("2" (assert) (("2" (rewrite "one_expt") (("2" (assert) (("2" (rewrite "left_identity") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but (-1 -3 1)) (("2" (inst + "fractional(i!1/n!1)*n!1" "floor(i!1/n!1)") (("1" (lemma "real_parts" ("x" "i!1/n!1")) (("1" (rewrite "div_cancel3" -1) nil nil)) nil) ("2" (typepred "fractional(i!1 / n!1)") (("2" (mult-by -1 "n!1") (("2" (mult-by -2 "n!1") (("2" (assert) (("2" (expand "fractional") (("2" (case-replace "i!1 / n!1 * n!1 = i!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (replace -1 * rl) (("2" (hide 2) (("2" (skosimp*) (("2" (expand "member") (("2" (expand "generated_by") (("2" (skosimp*) (("2" (replace -2 1) (("2" (replace -11 1) (("2" (simplify 1) (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "a!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "generated_is_subgroup" ("a" "a!1" "G" "G!1")) (("2" (expand "subgroup?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2) (("2" (hide-all-but 1) (("2" (expand "generated_by") (("2" (inst + "1") (("2" (assert) (("2" (rewrite "expt_1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil finite_groups nil) (finite_group nonempty-type-eq-decl nil group nil) (finite_group? const-decl "bool" group_def nil) (one formal-const-decl "T" finite_groups nil) (* formal-const-decl "[T, T -> T]" finite_groups nil) (NOT const-decl "[bool -> bool]" booleans nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (int_minus_int_is_int application-judgement "int" integers nil) (trichotomy formula-decl nil real_axioms nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (cancel_right formula-decl nil group nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt_0 formula-decl nil group nil) (int_plus_int_is_int application-judgement "int" integers nil) (expt_mult formula-decl nil group nil) (card_bij formula-decl nil finite_sets nil) (exists1 const-decl "bool" exists1 nil) (inverse? const-decl "bool" function_inverse_def nil) (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil) (bijective_inverse_exists formula-decl nil function_inverse_def nil) (F skolem-const-decl "[below[N] -> T]" finite_groups nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (injective? const-decl "bool" functions nil) (X skolem-const-decl "[T -> boolean]" finite_groups nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (n!1 skolem-const-decl "posnat" finite_groups nil) (S!1 skolem-const-decl "(nonempty?[T])" finite_groups nil) (N skolem-const-decl "{n: nat | n = Card(S!1)}" finite_groups nil) (surjective? const-decl "bool" functions nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (same_card_subset formula-decl nil finite_sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bijective? const-decl "bool" functions nil) (below type-eq-decl nil nat_types nil) (subgroup? const-decl "bool" group_def nil) (group nonempty-type-eq-decl nil group nil) (group? const-decl "bool" group_def nil) (generated_is_subgroup formula-decl nil group nil) (subset_antisymmetric formula-decl nil sets_lemmas nil) (generated_by const-decl "group" group nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (left_identity formula-decl nil monad nil) (one_expt formula-decl nil group nil) (expt_expt formula-decl nil group nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (real_parts formula-decl nil floor_ceil nil) (real_plus_real_is_real application-judgement "real" reals nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (integer nonempty-type-from-decl nil integers nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (n!1 skolem-const-decl "posnat" finite_groups nil) (i!1 skolem-const-decl "int" finite_groups nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (fractional const-decl "{x | 0 <= x & x < 1}" floor_ceil nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (subset? const-decl "bool" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (^ const-decl "T" group nil) (empty? const-decl "bool" sets nil) (nonempty_card formula-decl nil finite_sets nil) (finite_subset formula-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (member const-decl "bool" sets nil) (expt_1 formula-decl nil group nil)) nil) (finite_generated_by_def-1 nil 3293256444 ("" (skosimp*) (("" (case "S!1(a!1)") (("1" (assert) (("1" (typepred "G!1") (("1" (expand "finite_group?") (("1" (flatten) (("1" (lemma "finite_subset" ("s" "S!1" "A" "G!1")) (("1" (assert) (("1" (lemma "nonempty_card" ("S" "S!1")) (("1" (flatten -1) (("1" (hide -2) (("1" (case-replace "nonempty?(S!1)") (("1" (name "X" "{t: T | EXISTS (n: posnat): n <= card(S!1) AND t = a!1 ^ n}") (("1" (replace -1) (("1" (case "subset?(X,S!1)") (("1" (name "N" "card(S!1)") (("1" (replace -1) (("1" (case "FORALL (n:posnat): n < N => a!1^n /= one") (("1" (case "FORALL (i,j:posnat): i <= N & j <= N & i /= j => a!1^i /= a!1^j") (("1" (lemma "card_bij" ("S" "X" "N" "N")) (("1" (case "(EXISTS (f: [(X) -> below[N]]): bijective?(f))") (("1" (replace -1 -2) (("1" (flatten -2) (("1" (lemma "same_card_subset" ("A" "X" "B" "S!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (name "F" "LAMBDA (n: below[N]): IF n = 0 THEN a!1 ^ N ELSE a!1 ^ n ENDIF") (("2" (case "bijective?[below[N],(X)](F)") (("1" (lemma "bijective_inv_exists[below[N],(X)]" ("f" "F")) (("1" (expand "exists1") (("1" (flatten) (("1" (skolem!) (("1" (lemma "bij_inv_is_bij_alt[below[N],(X)]" ("f" "F" "g" "x!1")) (("1" (inst + "x!1") nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -1) (("2" (skosimp*) (("2" (expand "X" 1) (("2" (expand "F" 1) (("2" (case-replace "x1!1=0") (("1" (inst + "N") (("1" (assert) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.108 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
