| products/sources/formale sprachen/PVS/groups/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: cauchy.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(cauchy
(IMP_finite_cyclic_groups_TCC1 0 (IMP_finite_cyclic_groups_TCC1-1 nil 3531317209 ("" (rewrite "fullset_is_group") nil nil) ((fullset_is_group formula-decl nil cauchy nil)) nil)) (fseq_product_TCC1 0 (fseq_product_TCC1-1 nil 3529790042 ("" (subtype-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (fseq_product_TCC2 0 (fseq_product_TCC2-1 nil 3529790042 ("" (termination-tcc) nil nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty_seq const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (T formal-type-decl nil cauchy nil) (rest const-decl "finseq" seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (S_TCC1 0 (S_TCC1-1 nil 3529800017 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans 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) (>= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil)) nil)) (fseq_product_in 0 (fseq_product_in-1 nil 3529792046 ("" (measure-induct+ "length(fs)" "fs") (("" (skosimp) (("" (expand* "member" "finseq_appl") (("" (case "length(x!1) = 0") (("1" (hide (-2 -3)) (("1" (expand "fseq_product") (("1" (assert) (("1" (rewrite "one_in") nil nil)) nil)) nil)) nil) ("2" (inst -1 "rest(x!1)") (("2" (inst?) (("2" (prop) (("1" (expand "fseq_product" 2) (("1" (assert) (("1" (expand "finseq_appl") (("1" (rewrite "product_in") (("1" (hide (-1 2 3)) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (case "length(rest(x!1)) = 0") (("1" (hide 1) (("1" (expand "fseq_product") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 4) (("2" (typepred "i!1") (("2" (inst -2 "i!1 + 1") (("1" (lemma "rest_pos") (("1" (inst?) (("1" (assert) (("1" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil) ("2" (hide (-2 3)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 3)) (("3" (rewrite "length_rest") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (monad nonempty-type-eq-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (one_in formula-decl nil monad "algebra/") (length_rest formula-decl nil seq_extras "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (x!1 skolem-const-decl "finseq[T]" cauchy nil) (i!1 skolem-const-decl "below[length(rest(x!1))]" cauchy nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (rest_pos formula-decl nil seq_extras "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (product_in formula-decl nil group "algebra/") (rest const-decl "finseq" seq_extras "structures/") (fseq_product def-decl "T" cauchy nil) (member const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" cauchy nil) (* formal-const-decl "[T, T -> T]" cauchy nil) (set type-eq-decl nil sets nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil cauchy nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (fseq_product_o 0 (fseq_product_o-1 nil 3529875529 ("" (measure-induct+ "length(fs1)" "fs1") (("" (skosimp) (("" (case "length(x!1) = 0") (("1" (hide (-2 -3)) (("1" (expand "fseq_product" 1 2) (("1" (assert) (("1" (rewrite "empty_0") (("1" (replaces -1) (("1" (rewrite "empty_o_seq") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "fseq_product" 2 (1 2)) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (hide-all-but (-1 1 3)) (("1" (grind) nil nil)) nil) ("2" (expand "o" 2 1) (("2" (rewrite "rest_compo") (("2" (case "length(rest(x!1)) = 0") (("1" (hide-all-but (-1 2)) (("1" (expand "fseq_product" 1 2) (("1" (assert) (("1" (rewrite "empty_0") (("1" (replaces -1) (("1" (rewrite "empty_o_seq") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -1 "rest(x!1)") (("2" (inst -1 "G!1" "fs2!1") (("2" (prop) (("1" (replaces -1) (("1" (hide-all-but 3) (("1" (rewrite "assoc") nil nil)) nil)) nil) ("2" (hide (-2 4 5 6)) (("2" (skosimp) (("2" (inst -1 "i!1 + 1") (("1" (lemma "rest_pos") (("1" (inst?) (("1" (assert) (("1" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil) ("2" (hide (-1 2 3)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (2 3 4)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (rest_compo formula-decl nil seq_extras "structures/") (assoc formula-decl nil group "algebra/") (rest_pos formula-decl nil seq_extras "structures/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (NOT const-decl "[bool -> bool]" booleans nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (i!1 skolem-const-decl "below[length(rest(x!1))]" cauchy nil) (x!1 skolem-const-decl "finseq[T]" cauchy nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (one_right formula-decl nil group "algebra/") (rest const-decl "finseq" seq_extras "structures/") (one_left formula-decl nil group "algebra/") (empty_o_seq formula-decl nil seq_extras "structures/") (empty_0 formula-decl nil seq_extras "structures/") (O const-decl "finseq" finite_sequences nil) (fseq_product def-decl "T" cauchy nil) (= const-decl "[T, T -> boolean]" equalities nil) (member const-decl "bool" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" cauchy nil) (* formal-const-decl "[T, T -> T]" cauchy nil) (set type-eq-decl nil sets nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil cauchy nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (fseq_product_one 0 (fseq_product_one-1 nil 3529795198 ("" (measure-induct+ "length(fs)" "fs") (("" (skosimp) (("" (expand* "member" "finseq_appl") (("" (case "length(x!1) = 0") (("1" (hide (-2 -3)) (("1" (expand "fseq_product") (("1" (assert) nil nil)) nil)) nil) ("2" (inst -1 "rest(x!1)") (("2" (inst?) (("2" (prop) (("1" (expand "fseq_product" 2) (("1" (assert) nil nil)) nil) ("2" (case "length(rest(x!1)) = 0") (("1" (hide (-2 1)) (("1" (expand "fseq_product") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 4) (("2" (skosimp) (("2" (typepred "i!1") (("2" (inst -2 "i!1 + 1") (("1" (lemma "rest_pos") (("1" (inst?) (("1" (assert) (("1" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil) ("2" (hide (-2 3)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 3)) (("3" (rewrite "length_rest") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((one_right formula-decl nil group "algebra/") (inv_one formula-decl nil group "algebra/") (length_rest formula-decl nil seq_extras "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (x!1 skolem-const-decl "finseq[T]" cauchy nil) (i!1 skolem-const-decl "below[length(rest(x!1))]" cauchy nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (rest_pos formula-decl nil seq_extras "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (inv_left formula-decl nil group "algebra/") (rest const-decl "finseq" seq_extras "structures/") (fseq_product def-decl "T" cauchy nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (member const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" cauchy nil) (* formal-const-decl "[T, T -> T]" cauchy nil) (set type-eq-decl nil sets nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil cauchy nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (fseq_product_power 0 (fseq_product_power-1 nil 3530017945 ("" (measure-induct+ "length(fs)" "fs") (("" (skosimp) (("" (case "length(x!1) = 0") (("1" (hide (-2 -3)) (("1" (expand "fseq_product") (("1" (assert) (("1" (replaces -1) (("1" (rewrite "expt_0") nil nil)) nil)) nil)) nil)) nil) ("2" (inst -1 "rest(x!1)") (("2" (inst -1 "G!1" "g!1") (("2" (prop) (("1" (expand "fseq_product" 2) (("1" (assert) (("1" (replaces -1) (("1" (expand "same_element") (("1" (inst?) (("1" (replaces -1) (("1" (lemma "expt_mult") (("1" (inst -1 "g!1" "1" "length(rest(x!1))") (("1" (rewrite "expt_1") (("1" (replaces -1) (("1" (case-replace "1 + length(rest(x!1)) = length(x!1)") (("1" (hide 3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (case "length(rest(x!1)) = 0") (("1" (hide (-2 2)) (("1" (expand "same_element") (("1" (grind) nil nil)) nil)) nil) ("2" (expand "same_element") (("2" (skosimp) (("2" (inst -1 "i!1 + 1") (("1" (lemma "rest_pos") (("1" (inst?) (("1" (assert) (("1" (inst -1 "i!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 3)) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rest const-decl "finseq" seq_extras "structures/") (int_plus_int_is_int application-judgement "int" integers nil) (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt_1 formula-decl nil group "algebra/") (expt_mult formula-decl nil group "algebra/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (rest_pos formula-decl nil seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "below[length(rest(x!1))]" cauchy nil) (x!1 skolem-const-decl "finseq[T]" cauchy nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (expt_0 formula-decl nil group "algebra/") (^ const-decl "T" group "algebra/") (fseq_product def-decl "T" cauchy nil) (= const-decl "[T, T -> boolean]" equalities nil) (same_element const-decl "bool" cauchy nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" cauchy nil) (* formal-const-decl "[T, T -> T]" cauchy nil) (set type-eq-decl nil sets nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil cauchy nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (one_in_SE 0 (one_in_SE-1 nil 3530019013 ("" (skosimp) (("" (expand "member") (("" (expand "SE") (("" (expand "extend") (("" (prop) (("1" (inst?) (("1" (rewrite "one_in") nil nil)) nil) ("2" (expand "S") (("2" (assert) (("2" (prop) (("1" (skosimp) (("1" (expand "same_element") (("1" (inst?) (("1" (replaces -2) (("1" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "fseq_product_power") (("2" (inst -1 "G!1" "fs!1" "one") (("1" (assert) (("1" (replaces -2) (("1" (rewrite "one_expt") nil nil)) nil)) nil) ("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (extend const-decl "R" extend nil) (S const-decl "set[finseq]" cauchy nil) (same_element const-decl "bool" cauchy nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals 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) (one_expt formula-decl nil group "algebra/") (fseq_product_power formula-decl nil cauchy nil) (T formal-type-decl nil cauchy nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" cauchy nil) (one formal-const-decl "T" cauchy nil) (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (G!1 skolem-const-decl "finite_group[T, *, one]" cauchy nil) (one_in formula-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (monad nonempty-type-eq-decl nil monad "algebra/") (SE const-decl "set[finseq]" cauchy nil)) shostak)) (order_SE 0 (order_SE-1 nil 3530094223 ("" (skosimp*) (("" (expand "member") (("" (expand "SE") (("" (expand "extend") (("" (assert) (("" (prop) (("" (hide -2) (("" (expand "S") (("" (flatten) (("" (hide -2) (("" (lemma "fseq_product_power") (("" (inst?) (("" (assert) (("" (replaces -2) (("" (replaces -2) (("" (lemma "one_iff_divides[T,*,one]") (("1" (inst?) (("1" (assert) (("1" (expand "prime?") (("1" (prop) (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (hide (-1 -2 -4 -5 2)) (("1" (lemma "period_is_generated_order") (("1" (inst?) (("1" (assert) (("1" (replaces -2) (("1" (expand "order") (("1" (lemma "generated_by_card_1") (("1" (inst -1 "G!1" "g!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "fullset_is_group") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (extend const-decl "R" extend nil) (S const-decl "set[finseq]" cauchy nil) (T formal-type-decl nil cauchy nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" cauchy nil) (one formal-const-decl "T" cauchy nil) (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (one_iff_divides formula-decl nil groups_scaf nil) (fullset const-decl "set" sets nil) (group? const-decl "bool" group_def "algebra/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (generated_by_card_1 formula-decl nil finite_groups "algebra/") (order const-decl "posnat" monad "algebra/") (period_is_generated_order formula-decl nil finite_groups "algebra/") (period const-decl "posnat" finite_groups "algebra/") (prime? const-decl "bool" primes "ints/") (posnat 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) (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) (fullset_is_group formula-decl nil cauchy nil) (fseq_product_power formula-decl nil cauchy nil) (SE const-decl "set[finseq]" cauchy nil)) shostak)) (S_bij_set_seq_TCC1 0 (S_bij_set_seq_TCC1-1 nil 3529790452 ("" (subtype-tcc) nil nil) nil nil)) (S_bij_set_seq_TCC2 0 (S_bij_set_seq_TCC2-1 nil 3529790452 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil cauchy nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" cauchy nil) (one formal-const-decl "T" cauchy nil) (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (member const-decl "bool" sets nil) (star_closed? const-decl "bool" groupoid_def "algebra/") (one_member formula-decl nil monad "algebra/") (one_right formula-decl nil group "algebra/") (restrict const-decl "R" restrict nil) (one_left formula-decl nil group "algebra/") (identity? const-decl "bool" operator_defs nil) (monad? const-decl "bool" monad_def "algebra/") (associative? const-decl "bool" operator_defs nil) (monoid? const-decl "bool" monoid_def "algebra/") (inv_exists? const-decl "bool" group_def "algebra/") (group? const-decl "bool" group_def "algebra/") (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil)) nil)) (S_bij_set_seq 0 (S_bij_set_seq-1 nil 3529790556 ("" (skosimp*) (("" (skoletin* 1) (("" (inst 1 "(LAMBDA (s:(A)): add_first(inv(fseq_product(s)), s))") (("1" (expand "bijective?") (("1" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (lemma "first_equal") (("1" (inst -1 "x1!1" "x2!1" "inv(fseq_product(x1!1))" "inv(fseq_product(x2!1))") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (replaces -2) (("2" (expand "S") (("2" (flatten) (("2" (case "length(rest(y!1))=0") (("1" (inst 1 "rest(y!1)") (("1" (expand "fseq_product") (("1" (assert) (("1" (expand "finseq_appl") (("1" (expand "fseq_product" -4) (("1" (lemma "length_rest_0") (("1" (inst?) (("1" (assert) (("1" (hide (-3 -4 -6)) (("1" (rewrite "empty_0") (("1" (replaces -2) (("1" (rewrite "add_first_empty_seq") (("1" (decompose-equality 1) (("1" (grind) nil nil) ("2" (decompose-equality 1) (("2" (typepred "x!1") (("2" (expand "#" -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -5) (("2" (hide (-3 -4)) (("2" (lemma "length_rest_0") (("2" (inst?) (("2" (assert) (("2" (replaces -1) (("2" (replace -2 1 rl) (("2" (assert) (("2" (expand "set_seq") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "rest(y!1)") (("1" (hide -4) (("1" (expand "fseq_product" -3) (("1" (lift-if) (("1" (assert) (("1" (expand "finseq_appl") (("1" (case-replace "inv(fseq_product(rest(y!1))) = y!1`seq(0)" :hide? T) (("1" (lemma "seq_first_rest") (("1" (inst?) (("1" (assert) (("1" (expand* "first" "finseq_appl") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 3)) (("2" (lemma "divby") (("2" (inst -1 "one" "y!1`seq(0)" "fseq_product(rest(y!1))") (("2" (assert) (("2" (replace -1 1 rl) (("2" (rewrite "inv_inv") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -4) (("2" (expand "set_seq") (("2" (prop) (("1" (hide (-2 -3)) (("1" (grind) nil nil)) nil) ("2" (skosimp) (("2" (expand* "member" "finseq_appl") (("2" (inst -2 "i!1 + 1") (("2" (lemma "rest_pos") (("2" (inst?) (("2" (prop) (("2" (expand "finseq_appl") (("2" (inst -1 "i!1") (("1" (assert) nil nil) ("2" (hide (-2 -3 2)) (("2" (typepred "i!1") (("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) ("2" (skosimp) (("2" (typepred "s!1") (("2" (replaces -2) (("2" (replaces -2) (("2" (expand* "set_seq" "S") (("2" (prop) (("1" (hide -2) (("1" (expand "add_first") (("1" (expand "insert?") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand* "member" "finseq_appl") (("2" (expand "add_first") (("2" (expand "insert?") (("2" (prop) (("1" (rewrite "inv_in") (("1" (hide 2) (("1" (lemma "fseq_product_in") (("1" (inst -1 "G!1" "s!1") (("1" (expand* "member" "finseq_appl") (("1" (skosimp) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "finseq_appl") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "fseq_product" 1 1) (("3" (lift-if) (("3" (prop) (("3" (expand "finseq_appl") (("3" (rewrite "rest_add_first") (("3" (expand "add_first") (("3" (expand "insert?") (("3" (lemma "fseq_product_one") (("3" (inst -1 "G!1" "s!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" cauchy nil) (* formal-const-decl "[T, T -> T]" cauchy nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil cauchy nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions 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) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_set type-eq-decl nil finite_sets nil) (set_seq const-decl "set[finseq]" cauchy_scaf nil) (S const-decl "set[finseq]" cauchy nil) (rest_add_first formula-decl nil seq_extras "structures/") (inv_left formula-decl nil group "algebra/") (fseq_product_one formula-decl nil cauchy nil) (fseq_product_in formula-decl nil cauchy nil) (inv_in formula-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (i!1 skolem-const-decl "below[p!1]" cauchy nil) (insert? const-decl "finseq" seq_extras "structures/") (surjective? const-decl "bool" functions nil) (rest const-decl "finseq" seq_extras "structures/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (add_first_empty_seq formula-decl nil seq_extras "structures/") (empty_0 formula-decl nil seq_extras "structures/") (one_right formula-decl nil group "algebra/") (length_rest_0 formula-decl nil seq_extras "structures/") (inv_one formula-decl nil group "algebra/") (member const-decl "bool" sets nil) (y!1 skolem-const-decl "(B)" cauchy nil) (empty_seq const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rest_pos formula-decl nil seq_extras "structures/") (p!1 skolem-const-decl "posnat" cauchy nil) (i!1 skolem-const-decl "below[p!1 - 1]" cauchy nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (first const-decl "T" seq_extras "structures/") (seq_first_rest formula-decl nil seq_extras "structures/") (divby formula-decl nil group "algebra/") (inv_inv formula-decl nil group "algebra/") (injective? const-decl "bool" functions nil) (first_equal formula-decl nil seq_extras "structures/") (fseq_product def-decl "T" cauchy nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (add_first const-decl "finseq" seq_extras "structures/") (B skolem-const-decl "set[finseq]" cauchy nil) (A skolem-const-decl "set[finseq[T]]" cauchy nil)) shostak)) (S_is_finite 0 (S_is_finite-1 nil 3529841429 ("" (skosimp) (("" (case "n!1 = 0") (("1" (replaces -1) (("1" (case-replace "S(G!1)(0) = singleton(empty_seq)" :hide? T) (("1" (rewrite "finite_singleton") nil nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand* "S" "singleton") (("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil)) nil) ("2" (expand* "S" "singleton") (("2" (lemma "empty_0") (("2" (inst?) (("2" (assert) (("2" (prop) (("1" (skosimp) nil nil) ("2" (expand "fseq_product") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "S_bij_set_seq") (("2" (inst?) (("1" (assert) (("1" (lemma "set_seq_is_finite") (("1" (inst -1 "G!1" "n!1-1") (("1" (assert) (("1" (lemma "bijection_finite_set2[finseq,finseq]") (("1" (inst -1 "set_seq(G!1)(n!1-1)" "S(G!1)(n!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide (-1 2 3)) (("2" (typepred "G!1") (("2" (expand "finite_group?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" countable_props "sets_aux/") (below type-eq-decl nil nat_types nil) (T formal-type-decl nil cauchy nil) (finseq type-eq-decl nil finite_sequences nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" cauchy nil) (one formal-const-decl "T" cauchy nil) (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (S const-decl "set[finseq]" cauchy nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (empty_seq const-decl "finseq" finite_sequences nil) (finite_singleton judgement-tcc nil finite_sets nil) (empty_0 formula-decl nil seq_extras "structures/") (member const-decl "bool" sets nil) (fseq_product def-decl "T" cauchy nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (n!1 skolem-const-decl "nat" cauchy nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (set_seq_is_finite formula-decl nil cauchy_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (set_seq const-decl "set[finseq]" cauchy_scaf nil) (bijection_finite_set2 formula-decl nil finite_sets_eq "finite_sets/") (finite_set type-eq-decl nil finite_sets nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (G!1 skolem-const-decl "finite_group[T, *, one]" cauchy nil) (is_finite const-decl "bool" finite_sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (S_bij_set_seq formula-decl nil cauchy nil)) shostak)) (S_card_TCC1 0 (S_card_TCC1-1 nil 3529842528 ("" (skosimp) (("" (rewrite "S_is_finite") nil nil)) nil) ((S_is_finite formula-decl nil cauchy nil) (T formal-type-decl nil cauchy nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" cauchy nil) (one formal-const-decl "T" cauchy nil) (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil)) nil)) (S_card 0 (S_card-1 nil 3529842529 ("" (skosimp*) (("" (lemma "S_bij_set_seq") (("" (inst?) (("" (assert) (("" (lemma "set_seq_is_finite") (("" (inst -1 "G!1" "p!1-1") (("" (assert) (("" (lemma "card_eq_bij[finseq,finseq]") (("" (inst?) (("" (prop) (("" (hide (-2 -3 -4)) (("" (lemma "card_set_seq") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.70 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 |
