| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/groups/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 204 kB |
|
Quelle cauchy.prfSprache: Lisp |
|||||||||||||||
|
(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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((S_bij_set_seq formula-decl nil cauchy nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/") (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (card_set_seq formula-decl nil cauchy_scaf nil) (set_seq const-decl "set[finseq]" cauchy_scaf nil) (S const-decl "set[finseq]" cauchy nil) (set_seq_is_finite formula-decl nil cauchy_scaf nil) (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) (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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cauchy nil)) shostak)) (F_TCC1 0 (F_TCC1-1 nil 3529848984 ("" (subtype-tcc) nil nil) ((mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers 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/") (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (Zn const-decl "set[below(n)]" zp_group nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (S const-decl "set[finseq]" cauchy nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (G!1 skolem-const-decl "finite_group[T, *, one]" cauchy nil) (is_finite const-decl "bool" finite_sets nil) (injective? const-decl "bool" functions nil) (group? const-decl "bool" group_def "algebra/") (inv_exists? const-decl "bool" group_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (associative? const-decl "bool" operator_defs nil) (monad? const-decl "bool" monad_def "algebra/") (identity? const-decl "bool" operator_defs nil) (one_left formula-decl nil group "algebra/") (restrict const-decl "R" restrict nil) (one_right formula-decl nil group "algebra/") (one_member formula-decl nil monad "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (member const-decl "bool" sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (F_1_TCC1 0 (F_1_TCC1-1 nil 3529874518 ("" (subtype-tcc) nil nil) nil nil)) (F_1_TCC2 0 (F_1_TCC2-1 nil 3529874518 ("" (subtype-tcc) nil nil) nil nil)) (F_2_TCC1 0 (F_2_TCC1-1 nil 3529874615 ("" (subtype-tcc) nil nil) nil nil)) (F_o_F12_TCC1 0 (F_o_F12_TCC1-1 nil 3529874749 ("" (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/") (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (Zn const-decl "set[below(n)]" zp_group nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (S const-decl "set[finseq]" cauchy nil) (G!1 skolem-const-decl "finite_group[T, *, one]" cauchy nil) (is_finite const-decl "bool" finite_sets nil) (injective? const-decl "bool" functions nil) (group? const-decl "bool" group_def "algebra/") (inv_exists? const-decl "bool" group_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (associative? const-decl "bool" operator_defs nil) (monad? const-decl "bool" monad_def "algebra/") (identity? const-decl "bool" operator_defs nil) (one_left formula-decl nil group "algebra/") (restrict const-decl "R" restrict nil) (one_right formula-decl nil group "algebra/") (one_member formula-decl nil monad "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (member const-decl "bool" sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (F_o_F12 0 (F_o_F12-1 nil 3529874799 ("" (skosimp*) (("" (typepred "fs!1") (("" (expand "S") (("" (flatten) (("" (hide (-2 -3)) (("" (decompose-equality 1) (("1" (expand* "o" "F" "F_1" "F_2") (("1" (assert) nil nil)) nil) ("2" (decompose-equality 1) (("2" (expand* "o" "F" "F_1" "F_2") (("2" (lift-if) (("2" (assert) (("2" (prop) (("2" (case "x!1 = 0") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (lemma "rem_sum_floor") (("2" (inst?) (("2" (lemma "rem_mod") (("2" (inst -1 "p!1" "k!1") (("2" (replaces -1) (("2" (case-replace "floor((k!1 + x!1) / p!1) = 1" :hide? T) (("1" (assert) nil nil) ("2" (hide (-1 4)) (("2" (lemma "floor_val") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (typepred "k!1" "x!1") (("2" (hide -2) (("2" (expand "F") (("2" (lemma "lt_plus_lt2") (("2" (inst -1 "p!1" "k!1" "p!1" "x!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)) nil)) nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (S const-decl "set[finseq]" cauchy nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types 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_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) (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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (Zn const-decl "set[below(n)]" zp_group nil) (F const-decl "finseq" cauchy nil) (O const-decl "finseq" finite_sequences nil) (F_1 const-decl "finseq" cauchy nil) (F_2 const-decl "finseq" cauchy nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (rem_sum_floor formula-decl nil modulo_arithmetic nil) (rem_mod formula-decl nil modulo_arithmetic nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (lt_plus_lt2 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (floor_val formula-decl nil floor_ceil nil) (int_plus_int_is_int application-judgement "int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (integer nonempty-type-from-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (fs_o_F21 0 (fs_o_F21-1 nil 3529881525 ("" (skosimp*) (("" (typepred "fs!1") (("" (expand "S") (("" (flatten) (("" (hide (-2 -3)) (("" (decompose-equality 1) (("1" (expand* "o" "F" "F_1" "F_2") nil nil) ("2" (decompose-equality 1) (("2" (expand* "o" "F" "F_1" "F_2") (("2" (lift-if) (("2" (prop) (("2" (typepred "x!1") (("2" (replaces -2) (("2" (rewrite "rem_mod") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (S const-decl "set[finseq]" cauchy nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types 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_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) (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) (O const-decl "finseq" finite_sequences nil) (< const-decl "bool" reals nil) (F_2 const-decl "finseq" cauchy nil) (below type-eq-decl nil naturalnumbers nil) (Zn const-decl "set[below(n)]" zp_group nil) (F_1 const-decl "finseq" cauchy nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (int_minus_int_is_int application-judgement "int" integers nil) (rem_mod formula-decl nil modulo_arithmetic nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (F_in_S 0 (F_in_S-1 nil 3529880561 ("" (skosimp*) (("" (expand "member") (("" (expand "S") (("" (prop) (("1" (expand "F") (("1" (propax) nil nil)) nil) ("2" (skosimp) (("2" (expand "member") (("2" (expand "F") (("2" (prop) (("1" (typepred "fs!1") (("1" (expand "S") (("1" (flatten) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (typepred "k!1") (("2" (typepred "fs!1") (("2" (expand "S") (("2" (flatten) (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "F_o_F12") (("3" (inst?) (("3" (replaces -1) (("3" (lemma "fseq_product_o") (("3" (inst -1 "G!1" "F_1(fs!1)(k!1)" "F_2(fs!1)(k!1)") (("3" (prop) (("1" (replaces -1) (("1" (lemma "one_left") (("1" (inst -1 "fseq_product(F_1(fs!1)(k!1))") (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (lemma "inv_left") (("1" (inst -1 "fseq_product(F_2(fs!1)(k!1))") (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (lemma "fseq_product_o") (("1" (inst -1 "G!1" "F_2(fs!1)(k!1)" "F_1(fs!1)(k!1)") (("1" (prop) (("1" (lemma "fs_o_F21") (("1" (inst?) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (rewrite "associative") (("1" (replace -1 1 rl) (("1" (typepred "fs!1") (("1" (expand "S") (("1" (flatten) (("1" (hide (-1 -2 -4)) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "member") (("2" (expand "F_2") (("2" (typepred "fs!1") (("2" (expand "S") (("2" (flatten) (("2" (inst?) (("1" (assert) nil nil) ("2" (hide (-2 2)) (("2" (typepred "i!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (expand "member") (("3" (expand "F_1") (("3" (typepred "fs!1") (("3" (expand "S") (("3" (flatten) (("3" (inst?) (("1" (assert) nil nil) ("2" (hide (-2 2)) (("2" (typepred "j!1") (("2" (typepred "k!1") (("2" (grind) 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" (hide 2) (("2" (skosimp) (("2" (expand "member") (("2" (expand "F_1") (("2" (typepred "fs!1") (("2" (expand "S") (("2" (flatten) (("2" (inst?) (("1" (assert) nil nil) ("2" (hide (-2 2)) (("2" (typepred "i!1") (("2" (typepred "k!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (expand "member") (("3" (expand "F_2") (("3" (typepred "fs!1") (("3" (expand "S") (("3" (flatten) (("3" (inst?) (("1" (assert) nil nil) ("2" (hide (-2 2)) (("2" (typepred "j!1") (("2" (grind) nil nil)) nil)) 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) (F const-decl "finseq" cauchy nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types 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_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) (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) (< const-decl "bool" reals nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}" modulo_arithmetic nil) (below type-eq-decl nil naturalnumbers nil) (Zn const-decl "set[below(n)]" zp_group nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (fseq_product_o formula-decl nil cauchy nil) (one_left formula-decl nil group "algebra/") (inv_left formula-decl nil group "algebra/") (one_right formula-decl nil group "algebra/") (associative formula-decl nil semigroup "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (fs_o_F21 formula-decl nil cauchy nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (G!1 skolem-const-decl "finite_group[T, *, one]" cauchy nil) (p!1 skolem-const-decl "posnat" cauchy nil) (fs!1 skolem-const-decl "(S(G!1)(p!1))" cauchy nil) (k!1 skolem-const-decl "(Zn[p!1])" cauchy nil) (i!1 skolem-const-decl "below[length(F_2(fs!1)(k!1))]" cauchy nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (j!1 skolem-const-decl "below[length(F_1(fs!1)(k!1))]" cauchy nil) (restrict const-decl "R" restrict nil) (int_minus_int_is_int application-judgement "int" integers nil) (fseq_product def-decl "T" cauchy nil) (i!1 skolem-const-decl "below[length(F_1(fs!1)(k!1))]" cauchy nil) (j!1 skolem-const-decl "below[length(F_2(fs!1)(k!1))]" cauchy nil) (F_1 const-decl "finseq" cauchy nil) (F_2 const-decl "finseq" cauchy nil) (F_o_F12 formula-decl nil cauchy nil) (S const-decl "set[finseq]" cauchy nil)) shostak)) (F_is_action_TCC1 0 (F_is_action_TCC1-1 nil 3529848984 ("" (skosimp*) (("" (lemma "F_in_S") (("" (inst -1 "G!1" "p!1" "x1!1`1" "x1!1`2") (("" (expand "member") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((F_in_S formula-decl nil cauchy nil) (member const-decl "bool" sets nil) (S const-decl "set[finseq]" cauchy nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (Zn const-decl "set[below(n)]" zp_group nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cauchy nil)) nil)) (F_is_action_TCC2 0 (F_is_action_TCC2-1 nil 3529848984 ("" (skosimp) (("" (rewrite "Zn_group") nil nil)) nil) ((Zn_group formula-decl nil zp_group nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans 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)) nil)) (F_is_action_TCC3 0 (F_is_action_TCC3-1 nil 3529848984 ("" (subtype-tcc) nil nil) nil nil)) (F_is_action_TCC4 0 (F_is_action_TCC4-1 nil 3530102299 ("" (skosimp*) (("" (case-replace "fullset[below(p!1)] = Zn[p!1]") (("1" (rewrite "Zn_group") nil nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (expand "fullset") (("2" (expand "Zn[p!1]") (("2" (expand "restrict") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (fullset const-decl "set" sets nil) (Zn const-decl "set[below(n)]" zp_group nil) (Zn_group formula-decl nil zp_group nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (restrict const-decl "R" restrict nil)) nil)) (F_is_action 0 (F_is_action-1 nil 3529882859 ("" (skosimp*) (("" (expand "group_action?") (("" (skosimp) (("" (prop) (("1" (decompose-equality 1) (("1" (expand "F") (("1" (typepred "x!1") (("1" (expand "S") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (expand "F") (("2" (typepred "x!2") (("2" (expand "F") (("2" (rewrite "rem_mod") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "++") (("2" (decompose-equality 1) (("1" (expand "F") (("1" (propax) nil nil)) nil) ("2" (decompose-equality 1) (("2" (expand "F") (("2" (assert) (("2" (rewrite "rem_sum1") (("2" (rewrite "rem_sum1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((group_action? const-decl "bool" group_action nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (rem_mod formula-decl nil modulo_arithmetic nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil cauchy nil) (finseq type-eq-decl nil finite_sequences nil) (F const-decl "finseq" cauchy nil) (S const-decl "set[finseq]" cauchy nil) (Zn const-decl "set[below(n)]" zp_group nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (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) (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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}" modulo_arithmetic nil) (rem_sum1 formula-decl nil modulo_arithmetic nil) (++ const-decl "below(n)" zp_group nil)) shostak)) (Fixed_subset_TCC1 0 (Fixed_subset_TCC1-1 nil 3529964584 ("" (skosimp*) (("" (prop) (("1" (skosimp) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (replaces -2) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (replaces -2) (("3" (replaces -2) (("3" (lemma "F_in_S") (("3" (inst -1 "G!1" "p!1" "x1!1`1" "x1!1`2") (("3" (expand "member") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((F_in_S formula-decl nil cauchy nil) (member const-decl "bool" sets nil) (S const-decl "set[finseq]" cauchy nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (Zn const-decl "set[below(n)]" zp_group nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cauchy nil)) nil)) (Fixed_subset_TCC2 0 (Fixed_subset_TCC2-1 nil 3529964584 ("" (skosimp*) (("" (lemma "Zn_group[p!1]") (("" (assert) nil nil)) nil)) nil) ((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) (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) (Zn_group formula-decl nil zp_group nil)) nil)) (Fixed_subset 0 (Fixed_subset-1 nil 3529964774 ("" (skosimp*) (("" (expand "SE") (("" (decompose-equality 1) (("" (iff) (("" (prop) (("1" (expand "Fix") (("1" (expand "extend") (("1" (prop) (("1" (hide -1) (("1" (inst 1 "x!1`seq(0)") (("1" (expand "same_element") (("1" (skosimp) (("1" (inst -2 "i!1") (("1" (expand "F") (("1" (decompose-equality -2) (("1" (decompose-equality -2) (("1" (inst?) (("1" (assert) (("1" (typepred "i!1") (("1" (replace -3 -1 rl) (("1" (rewrite "rem_mod") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "S") (("2" (flatten) (("2" (hide (-2 -3 2)) (("2" (typepred "i!1") (("2" (expand "Zn") (("2" (expand "restrict") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (expand "S") (("2" (flatten) (("2" (hide (-1 -3)) (("2" (inst?) (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -2) (("3" (expand "S") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Fix") (("2" (expand "extend") (("2" (prop) (("2" (skosimp) (("2" (hide -1) (("2" (expand "F") (("2" (decompose-equality 1) (("1" (expand "S") (("1" (propax) nil nil)) nil) ("2" (decompose-equality 1) (("1" (skosimp) (("1" (expand "same_element") (("1" (copy -2) (("1" (inst -1 "rem(p!1)(g!1 + x!2)") (("1" (inst -3 "x!2") (("1" (assert) nil nil) ("2" (hide (-1 2)) (("2" (expand "S") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (skosimp) (("2" (expand "S") (("2" (flatten) (("2" (hide (-2 -3)) (("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -2) (("3" (prop) (("1" (skosimp) (("1" (expand "S") (("1" (flatten) (("1" (hide (-2 -3)) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "S") (("2" (assert) nil nil)) nil)) nil)) nil) ("4" (hide -2) (("4" (skosimp) (("4" (expand "S") (("4" (flatten) (("4" (hide (-2 -3)) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((SE const-decl "set[finseq]" cauchy nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (g!1 skolem-const-decl "(Zn[p!1])" cauchy nil) (x!2 skolem-const-decl "below[p!1]" cauchy nil) (x!1 skolem-const-decl "finseq[T]" cauchy nil) (G!1 skolem-const-decl "finite_group[T, *, one]" cauchy nil) (restrict const-decl "R" restrict nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rem_mod formula-decl nil modulo_arithmetic nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}" modulo_arithmetic nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (p!1 skolem-const-decl "posnat" cauchy nil) (i!1 skolem-const-decl "below[length(x!1)]" cauchy nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil cauchy nil) (finseq type-eq-decl nil finite_sequences nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (same_element const-decl "bool" cauchy nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (F const-decl "finseq" cauchy nil) (S const-decl "set[finseq]" cauchy 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) (Zn const-decl "set[below(n)]" zp_group nil) (Fix const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (subset? const-decl "bool" sets nil) (F type-eq-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (++ const-decl "below(n)" zp_group nil) (below type-eq-decl nil naturalnumbers nil) (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) (>= 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (cauchy 0 (cauchy-1 nil 3530095796 ("" (skosimp*) (("" (expand "order") (("" (lemma "Fix_congruence[below(p!1),++,0,finseq]") (("" (inst -1 "Zn[p!1]" "S(G!1)(p!1)" "1" "p!1" "F(p!1,G!1)") (("1" (prop) (("1" (lemma "S_card") (("1" (inst -1 "G!1" "p!1") (("1" (lemma "Fixed_subset") (("1" (inst -1 "G!1" "p!1") (("1" (assert) (("1" (replaces -1) (("1" (replaces -1) (("1" (lemma "order_gt_1[T,*,one]") (("1" (inst -1 "p!1" "G!1") (("1" (expand "order") (("1" (expand "divides") (("1" (skosimp*) (("1" (case "x!2 > 0") (("1" (case "card(SE(G!1)(p!1)) = (p!1 * x!2) ^ (p!1 - 1) - p!1 * x!1") (("1" (hide -4) (("1" (rewrite "mult_expt") (("1" (lemma "expt_plus") (("1" (inst -1 "1" "p!1 - 2" "p!1") (("1" (assert) (("1" (rewrite "expt_x1") (("1" (replaces -1) (("1" (rewrite "associative_mult" :dir rl) (("1" (lemma "distributive") (("1" (inst -1 "p!1" "(p!1 ^ (p!1 - 2)) * x!2 ^ (p!1 - 1)" "- x!1") (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (case "divides(p!1, card(SE(G!1)(p!1)))") (("1" (hide -2) (("1" (case "card(SE(G!1)(p!1)) > 1") (("1" (hide -2) (("1" (lemma "card_2_has_2[finseq]") (("1" (inst?) (("1" (assert) (("1" (skosimp) (("1" (case "same_element(one, y!1)") (("1" (inst 2 "x!3`seq(0)") (("1" (lemma "order_SE") (("1" (inst -1 "G!1" "x!3" "p!1" "x!3`seq(0)") (("1" (assert) (("1" (hide (-4 -5 -6 -7 -8 3)) (("1" (prop) (("1" (decompose-equality 1) (("1" (hide (-1 -2)) (("1" (expand "SE") (("1" (expand "extend") (("1" (prop) (("1" (hide (-2 -4)) (("1" (expand "S") (("1" (flatten) (("1" (hide (-2 -3 -5 -6)) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (expand "same_element") (("2" (inst -2 "x!4") (("2" (replaces -2) (("2" (hide -3) (("2" (expand "SE") (("2" (expand "extend") (("2" (prop) (("2" (hide -1) (("2" (skosimp) (("2" (expand "same_element") (("2" (inst-cp -1 "x!4") (("2" (inst -1 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -3 2)) (("2" (expand "SE") (("2" (expand "extend") (("2" (prop) (("2" (hide -1) (("2" (skosimp) (("2" (expand "same_element") (("2" (skosimp) (("2" (inst-cp -1 "i!1") (("2" (inst -1 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -3 -4 -5 -6 -7 -8 2)) (("2" (expand "SE") (("2" (expand "extend") (("2" (prop) (("2" (hide -1) (("2" (skosimp) (("2" (expand "same_element") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 -3 -4 -5 -6 -7 -8 2)) (("3" (expand "SE") (("3" (expand "extend") (("3" (prop) (("3" (hide -2) (("3" (expand "S") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-3 -4 -5 -6 -7)) (("2" (inst 3 "y!1`seq(0)") (("1" (lemma "order_SE") (("1" (inst -1 "G!1" "y!1" "p!1" "y!1`seq(0)") (("1" (assert) (("1" (hide (-1 3 4)) (("1" (prop) (("1" (expand* "SE" "same_element" "extend") (("1" (prop) (("1" (skosimp*) (("1" (hide -1) (("1" (inst-cp -1 "i!1") (("1" (inst -1 "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand* "SE" "same_element" "extend") (("2" (prop) (("2" (hide -1) (("2" (skosimp*) (("2" (inst-cp -1 "i!1") (("2" (inst -1 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2 3)) (("2" (expand "SE") (("2" (expand "extend") (("2" (prop) (("2" (hide -1) (("2" (skosimp) (("2" (expand "same_element") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 2 3)) (("3" (expand "SE") (("3" (expand "extend") (("3" (prop) (("3" (hide -2) (("3" (expand "S") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "divides") (("2" (skosimp) (("2" (typepred "card(SE(G!1)(p!1))") (("2" (replaces -1) (("2" (typepred "Card[finseq[T]](SE(G!1)(p!1))") (("2" (case "Card[finseq[T]](SE(G!1)(p!1)) = 0") (("1" (hide (-2 -3 -4 -5 1)) (("1" (lemma "empty_card[finseq]") (("1" (inst?) (("1" (assert) (("1" (hide -2) (("1" (expand "empty?") (("1" (lemma "one_in_SE") (("1" (inst -1 "G!1" "(# length := p!1, seq := (LAMBDA (i: below[p!1]): one) #)" "p!1") (("1" (expand "same_element") (("1" (expand "member") (("1" (inst -2 "(# length := p!1, seq := (LAMBDA (i: below[p!1]): one) #)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "Card[finseq[T]](SE(G!1)(p!1)) = 1") (("1" (replaces -3) (("1" (case "x!3 <= 0") (("1" (expand "<=") (("1" (prop) (("1" (lemma "neg_times_ge") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "<=") (("2" (flatten) (("2" (lemma "prime_gt_1") (("2" (inst -1 "p!1") (("2" (assert) (("2" (lemma "eq1_gt") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "divides") (("2" (inst?) (("2" (hide -1) (("2" (hide -2) (("2" (lemma "prime_gt_1") (("2" (inst?) (("2" (assert) (("2" (hide -3) (("2" (grind) 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" (hide (-1 -2 -4 2)) (("2" (replaces -2) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide (-2 2)) (("2" (lemma "prime_gt_1") (("2" (inst -1 "p!1") (("2" (prop) (("2" (hide -3) (("2" (replaces -3) (("2" (lemma "pos_times_gt") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "fullset_is_group") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-2 2)) (("2" (expand "finite_group?") (("2" (rewrite "Zn_group") (("2" (rewrite "Zn_finite") nil nil)) nil)) nil)) nil) ("3" (hide (-2 2)) (("3" (expand "order") (("3" (rewrite "expt_x1") (("3" (rewrite "Zn_card") nil nil)) nil)) nil)) nil) ("4" (hide (-1 -2 2)) (("4" (rewrite "S_is_finite") nil nil)) nil) ("5" (hide (-1 -2 2)) (("5" (expand "nonempty?") (("5" (expand "empty?") (("5" (inst -1 "(# length := p!1, seq := (LAMBDA (i: below[p!1]): one) #)") (("5" (expand "member") (("5" (expand "S") (("5" (prop) (("1" (skosimp) (("1" (expand "member") (("1" (rewrite "one_in") nil nil)) nil)) nil) ("2" (lemma "fseq_product_power") (("2" (inst -1 "G!1" "(# length := p!1, seq := (LAMBDA (i: below[p!1]): one) #)" "one") (("1" (expand "same_element") (("1" (rewrite "one_expt") nil nil)) nil) ("2" (hide 2) (("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide (-1 -2 2)) (("6" (rewrite "F_is_action") nil nil)) nil)) nil) ("2" (hide (-1 -2 2)) (("2" (skosimp) (("2" (lemma "F_in_S") (("2" (inst -1 "G!1" "p!1" "x1!1`1" "x1!1`2") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 -2 2)) (("3" (rewrite "Zn_group") nil nil)) nil)) nil)) nil)) nil)) nil) ((order const-decl "posnat" monad "algebra/") (p!1 skolem-const-decl "posnat" cauchy nil) (set type-eq-decl nil sets nil) (group? const-decl "bool" group_def "algebra/") (Zn const-decl "set[below(n)]" zp_group nil) (F const-decl "finseq" cauchy nil) (G!1 skolem-const-decl "finite_group[T, *, one]" cauchy nil) (S const-decl "set[finseq]" cauchy 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) (group nonempty-type-eq-decl nil group "algebra/") (F type-eq-decl nil group_action nil) (F_is_action formula-decl nil cauchy nil) (one_in formula-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (monad nonempty-type-eq-decl nil monad "algebra/") (one_expt formula-decl nil group "algebra/") (fseq_product_power formula-decl nil cauchy nil) (nonempty? const-decl "bool" sets nil) (S_is_finite formula-decl nil cauchy nil) (Zn_card formula-decl nil zp_group nil) (Zn_group formula-decl nil zp_group nil) (Zn_finite formula-decl nil zp_group nil) (S_card formula-decl nil cauchy nil) (Fixed_subset formula-decl nil cauchy nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (fullset_is_group formula-decl nil cauchy nil) (divides const-decl "bool" divides nil) (expt_plus formula-decl nil exponentiation nil) (posint_exp application-judgement "posint" exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (int_plus_int_is_int application-judgement "int" integers nil) (posrat_exp application-judgement "posrat" exponentiation nil) (distributive formula-decl nil number_fields nil) (minus_int_is_int application-judgement "int" integers nil) (card_2_has_2 formula-decl nil finite_sets nil) (same_element const-decl "bool" cauchy nil) (order_SE formula-decl nil cauchy nil) (member const-decl "bool" sets nil) (extend const-decl "R" extend nil) (x!3 skolem-const-decl "finseq[T]" cauchy nil) (y!1 skolem-const-decl "finseq[T]" cauchy nil) (NOT const-decl "[bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (neg_times_ge formula-decl nil real_props nil) (eq1_gt formula-decl nil real_props nil) (prime_gt_1 formula-decl nil primes "ints/") (one_in_SE formula-decl nil cauchy nil) (empty? const-decl "bool" sets nil) (empty_card formula-decl nil finite_sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (expt def-decl "real" exponentiation nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (int_expt application-judgement "int" exponentiation nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posnat_expt application-judgement "posnat" exponentiation nil) (x!2 skolem-const-decl "int" cauchy nil) (x!1 skolem-const-decl "int" cauchy nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (associative_mult formula-decl nil number_fields nil) (expt_x1 formula-decl nil exponentiation nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rat_exp application-judgement "rat" exponentiation nil) (mult_expt formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (SE const-decl "set[finseq]" cauchy nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (pos_times_gt formula-decl nil real_props nil) (fullset const-decl "set" sets nil) (order_gt_1 formula-decl nil groups_scaf nil) (F_in_S formula-decl nil cauchy nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Fix_congruence formula-decl nil group_action nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (below type-eq-decl nil naturalnumbers nil) (++ const-decl "below(n)" zp_group nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil cauchy nil) (finseq type-eq-decl nil finite_sequences nil)) shostak)) (cauchy_cor_TCC1 0 (cauchy_cor_TCC1-1 nil 3530980535 ("" (skosimp*) (("" (hide (-1 -2)) (("" (typepred "G!1" "H!1") (("" (expand "group?") (("" (expand "monoid?") (("" (flatten) (("" (lemma "finite_subgroups") (("" (inst?) (("" (assert) (("" (hide (-2 -4 -5 -6)) (("" (expand* "finite_group?" "finite_monad?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_monad? const-decl "bool" monad_def "algebra/") (finite_subgroups formula-decl nil group "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (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/") (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/")) nil)) (cauchy_cor 0 (cauchy_cor-1 nil 3530980803 ("" (skosimp*) (("" (lemma "cauchy") (("" (inst?) (("" (assert) (("" (skosimp) (("" (inst 1 "generated_by(x!1)") (("1" (rewrite "period_is_generated_order") nil nil) ("2" (rewrite "generated_is_subgroup") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy formula-decl nil cauchy nil) (group? const-decl "bool" group_def "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (generated_by const-decl "group" group "algebra/") (G!1 skolem-const-decl "finite_group[T, *, one]" cauchy nil) (x!1 skolem-const-decl "(G!1)" cauchy nil) (subgroup type-eq-decl nil group "algebra/") (period_is_generated_order formula-decl nil finite_groups "algebra/") (member const-decl "bool" sets nil) (generated_is_subgroup formula-decl nil group "algebra/") (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) (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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cauchy nil)) shostak)))
¤ Dauer der Verarbeitung: 0.210 Sekunden (vorverarbeitet am 2026-04-28) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26