| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/numbers/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 451 kB |
|
Quelle product_perm_lems.prfSprache: Lisp |
|||||||||||||||
|
(product_perm_lems (swap_TCC1 0 (swap_TCC1-1 nil 3413557357 ("" (skeep) (("" (skeep) (("" (lift-if) (("" (ground) (("" (typepred "fs`seq") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (swap_len 0 (swap_len-1 nil 3413558127 ("" (grind) 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) (default const-decl "T" fseqs "structures/") (swap const-decl "fseq[posnat]" product_perm_lems nil)) shostak)) (swap_eq_arg 0 (swap_eq_arg-1 nil 3413559087 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (apply-extensionality :hide? t) (("2" (case "x!1 < length(fs!1)") (("1" (grind) nil nil) ("2" (typepred "fs!1`seq") (("2" (inst?) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers 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) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (swap const-decl "fseq[posnat]" product_perm_lems nil) (default const-decl "T" fseqs "structures/") (< const-decl "bool" reals nil) (real_lt_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) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (swap_symm 0 (swap_symm-1 nil 3413559177 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("1" (grind) nil nil) ("2" (apply-extensionality 1 :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers 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) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (swap const-decl "fseq[posnat]" product_perm_lems nil) (default const-decl "T" fseqs "structures/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (prod_swap_prep_TCC1 0 (prod_swap_prep_TCC1-1 nil 3413560184 ("" (subtype-tcc) nil nil) nil nil)) (prod_swap_prep 0 (prod_swap_prep-1 nil 3413565100 ("" (skosimp*) (("" (rewrite "product_restrict_eq") (("" (hide 2) (("" (expand "restrict") (("" (apply-extensionality 1 :hide? t) (("" (lift-if) (("" (typepred "fs!1`seq") (("" (inst?) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product_restrict_eq formula-decl nil product "reals/") (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (swap const-decl "fseq[posnat]" product_perm_lems nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (product_nat_nat application-judgement "posnat" product_fseq_posnat "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (restrict const-decl "[T -> real]" product "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (default const-decl "T" fseqs "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil)) shostak)) (prod_swap_prep2_TCC1 0 (prod_swap_prep2_TCC1-1 nil 3413563853 ("" (subtype-tcc) nil nil) nil nil)) (prod_swap_prep2 0 (prod_swap_prep2-1 nil 3413565132 ("" (skosimp*) (("" (rewrite "product_restrict_eq") (("" (hide 2) (("" (expand "restrict") (("" (apply-extensionality 1 :hide? t) (("" (lift-if) (("" (ground) (("" (expand "swap") (("" (typepred "fs!1`seq") (("" (inst?) (("" (assert) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((product_restrict_eq formula-decl nil product "reals/") (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (swap const-decl "fseq[posnat]" product_perm_lems nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (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) (product_nat_nat application-judgement "posnat" product_fseq_posnat "reals/") (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (restrict const-decl "[T -> real]" product "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (default const-decl "T" fseqs "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil)) shostak)) (product_swap 0 (product_swap-1 nil 3413557417 ("" (auto-rewrite "swap_len") (("" (skosimp*) (("" (expand "product") (("" (lift-if) (("" (prop) (("1" (expand "swap") (("1" (expand "product") (("1" (assert) nil nil)) nil)) nil) ("2" (case "i!1 = j!1") (("1" (replace -1) (("1" (rewrite "swap_eq_arg") nil nil)) nil) ("2" (case "(FORALL (i,j: below(length(fs!1))): i < j IMPLIES product(0, length(swap(fs!1)(i, j)) - 1, swap(fs!1)(i, j)`seq) = product(0, length(fs!1) - 1, fs!1`seq))") (("1" (inst-cp -1 "i!1" "j!1") (("1" (inst -1 "j!1" "i!1") (("1" (assert) (("1" (assert) (("1" (assert) (("1" (rewrite "swap_symm") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case-replace "i!2 = j!2") (("1" (rewrite "swap_eq_arg") nil nil) ("2" (lemma "product_split_ge") (("2" (inst?) (("2" (inst - "i!2") (("2" (assert) (("2" (replace -1 * lr) (("2" (hide -1) (("2" (lemma "product_last") (("2" (inst?) (("2" (assert) (("2" (replace -1 * lr) (("2" (hide -1) (("2" (swap! (! 2 l)) (("2" (lemma "product_split_ge") (("2" (inst?) (("2" (inst - "j!2") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "product_last") (("2" (inst?) (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "prod_swap_prep") (("2" (inst - "fs!1" "i!2" "j!2" "1+j!2" "l(fs!1)-1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (case-replace "i!2 = 0") (("1" (assert) (("1" (rewrite "prod_swap_prep2") (("1" (hide 5) (("1" (expand "swap") (("1" (swap-rel 2) (("1" (lemma "product_first") (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (swap! (! 2 l)) (("1" (lemma "product_split_ge") (("1" (inst?) (("1" (inst - "j!2") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_last") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "prod_swap_prep") (("2" (inst - "fs!1" "i!2" "j!2" "0" "i!2-1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "prod_swap_prep2") (("1" (hide 5) (("1" (hide 5) (("1" (expand "swap") (("1" (swap-rel 3) (("1" (lemma "product_split_ge") (("1" (inst?) (("1" (inst - "i!2") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_last") (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (swap! (! 3 l)) (("1" (lemma "product_split_ge") (("1" (inst?) (("1" (inst - "j!2") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_last") (("1" (inst?) (("1" (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) ("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((below type-eq-decl nil naturalnumbers nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (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) (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) (swap_eq_arg formula-decl nil product_perm_lems nil) (product_split_ge formula-decl nil product_nat "reals/") (product_last formula-decl nil product "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (prod_swap_prep2 formula-decl nil product_perm_lems nil) (product_first formula-decl nil product "reals/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (product_0_neg formula-decl nil product_nat "reals/") (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (fs!1 skolem-const-decl "fseq[posnat]" product_perm_lems nil) (i!2 skolem-const-decl "below(length(fs!1))" product_perm_lems nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (prod_swap_prep formula-decl nil product_perm_lems nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (product_nat_nat application-judgement "posnat" product_fseq_posnat "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (swap_len formula-decl nil product_perm_lems nil) (swap_symm formula-decl nil product_perm_lems nil) (prod_nnr application-judgement "nnreal" product_nat "reals/") (prod_nat application-judgement "nat" product_nat "reals/") (prod_pr application-judgement "posreal" product_nat "reals/") (prod_posnat application-judgement "posnat" product_nat "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (swap const-decl "fseq[posnat]" product_perm_lems nil) (product def-decl "real" product "reals/") (product const-decl "posnat" product_fseq_posnat "reals/")) shostak)) (swap_is_permutation 0 (swap_is_permutation-1 nil 3413654632 ("" (skosimp*) (("" (expand "permutation?") (("" (inst + "(LAMBDA (jj: below(length(swap(fs!1)(i!1, j!1)))): IF jj = i!1 THEN j!1 ELSIF jj = j!1 THEN i!1 ELSE jj ENDIF)") (("1" (prop) (("1" (expand "bijective?") (("1" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (case "y!1 = i!1") (("1" (case "y!1 = j!1") (("1" (inst + "y!1") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil) ("2" (inst + "j!1") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil)) nil) ("2" (case "y!1 = j!1") (("1" (inst + "i!1") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil) ("2" (inst + "y!1") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "ii!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "jj!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((permutation? const-decl "bool" permutations_fseq "structures/") (injective? const-decl "bool" functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (y!1 skolem-const-decl "below(length(fs!1))" product_perm_lems nil) (default const-decl "T" fseqs "structures/") (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IF const-decl "[boolean, T, T -> T]" if_def 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) (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (swap const-decl "fseq[posnat]" product_perm_lems nil) (fs!1 skolem-const-decl "fseq[posnat]" product_perm_lems nil) (below type-eq-decl nil naturalnumbers nil) (i!1 skolem-const-decl "below(length(fs!1))" product_perm_lems nil) (j!1 skolem-const-decl "below(length(fs!1))" product_perm_lems nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (product_permutation 0 (product_permutation-4 "NEW" 3507373532 ("" (skeep) (("" (auto-rewrite "swap_len") (("" (lemma "perm_length") (("" (inst - "fs1" "fs2") (("" (assert) (("" (assert) (("" (case "FORALL (n:nat, fs1, fs2: fseq[posnat]): n = length(fs1) IMPLIES (permutation?(fs1, fs2) IMPLIES product(fs1) = product(fs2))") (("1" (inst - "length(fs1)" "fs1" "fs2") (("1" (assert) nil nil)) nil) ("2" (induct "n") (("1" (skosimp*) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "product" +) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("2" (case "length(fs2!1) = 0") (("1" (assert) (("1" (hide -5) (("1" (lemma "perm_length") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -4 -5) (("2" (lemma "perm_length") (("2" (inst?) (("2" (assert) (("2" (case "length(fs1!1) = 1") (("1" (expand "product") (("1" (replace -1) (("1" (assert) (("1" (case-replace "length(fs2!1) = 1") (("1" (assert) (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst -6 "0") (("1" (typepred "f!1(0)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "permutation?") (("2" (skosimp*) (("2" (name "IX" "l(fs1!1)-1") (("2" (inst-cp -6 "IX") (("1" (lemma "product_last") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_swap") (("1" (swap-rel 3) (("1" (inst - "fs2!1" "IX" "f!1(IX)") (("1" (expand "product" -1) (("1" (lift-if) (("1" (case "length(swap(fs2!1)(IX, f!1(IX))) = 0") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "product_last") (("2" (inst?) (("2" (case-replace "length(fs2!1) = 1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (case-replace "swap(fs2!1)(IX, f!1(IX))`seq(length(fs2!1) - 1) = fs1!1`seq(IX)") (("1" (hide -1) (("1" (inst - "fs1!1 ^ (0, fs1!1`length-2)" "swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length-2)") (("1" (assert) (("1" (split -3) (("1" (expand "product" -1) (("1" (assert) (("1" (case "l(fs1!1 ^ (0, fs1!1`length - 2)) = 0") (("1" (assert) (("1" (hide-all-but (-1 3 4)) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) (("2" (case "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = 0") (("1" (assert) (("1" (hide-all-but (-1 2 3)) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) (("2" (case-replace "l(fs1!1 ^ (0, fs1!1`length - 2)) = l(fs1!1)-1") (("1" (case-replace "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = l(fs2!1) -1") (("1" (assert) (("1" (hide -1 -2) (("1" (lemma "product_restrict_eq") (("1" (inst - "structures@fseqs[posnat].^(fs1!1, (0, fs1!1`length - 2))`seq" "fs1!1`seq" "fs1!1`length - 2" "0") (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (lemma "product_restrict_eq") (("1" (inst?) (("1" (inst - "swap(fs2!1)(IX, f!1(IX))`seq") (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 9) (("2" (apply-extensionality :hide? t) (("2" (expand "restrict") (("2" (lift-if) (("2" (assert) (("2" (ground) (("2" (expand "swap") (("2" (lift-if) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 6) (("2" (inst + "(LAMBDA (jj: [below(l(fs1!1 ^ (0, l(fs1!1) - 2)))]): IF f!1(IX) = IX THEN f!1(jj) ELSIF f!1(jj) = IX THEN (f!1(IX)) ELSE f!1(jj) ENDIF)") (("1" (prop) (("1" (hide 6) (("1" (expand "bijective?") (("1" (flatten) (("1" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (typepred "x2!1") (("1" (expand "^") (("1" (lift-if) (("1" (lift-if) (("1" (inst-cp - "x1!1" "x2!1") (("1" (ground) (("1" (inst-cp - "IX" "x1!1") (("1" (inst-cp - "IX" "x2!1") (("1" (assert) nil nil)) nil)) nil) ("2" (case "f!1(x2!1) = IX") (("1" (assert) (("1" (inst-cp - "x1!1" "x2!1") (("1" (replace -1) (("1" (inst-cp - "IX" "x1!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (expand "swap") (("2" (expand "^") (("2" (inst - "y!1") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (expand "^") (("2" (assert) (("2" (typepred "x!1") (("2" (case "x!1 = IX") (("1" (expand "injective?") (("1" (reveal 1) (("1" (reveal -1) (("1" (inst - "IX") (("1" (skosimp*) (("1" (inst + "x!2") (("1" (assert) nil nil) ("2" (expand "^") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "ii!1") (("2" (expand "^") (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (inst - "ii!1") (("2" (expand "swap") (("2" (lift-if) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "injective?") (("2" (inst - "IX" "ii!1") (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "^") (("2" (expand "swap") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "jj!1") (("3" (grind) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "^") (("4" (expand "swap") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (typepred "jj!1") (("5" (expand "^") (("5" (assert) nil nil)) nil)) nil)) nil) ("6" (skosimp*) (("6" (expand "^") (("6" (expand "swap") (("6" (assert) (("6" (typepred "jj!1") (("6" (expand "^") (("6" (assert) (("6" (expand "bijective?") (("6" (flatten) (("6" (expand "injective?") (("6" (inst - "IX" "jj!1") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (skosimp*) (("7" (typepred "jj!1") (("7" (expand "^") (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 6) (("2" (expand "swap") (("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) ("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) ((nat nonempty-type-eq-decl nil naturalnumbers nil) (fsq type-eq-decl nil fsq "structures/") (barray type-eq-decl nil fseqs "structures/") (fseq type-eq-decl nil fseqs "structures/") (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (prod_posnat application-judgement "posnat" product_nat "reals/") (prod_pr application-judgement "posreal" product_nat "reals/") (prod_nat application-judgement "nat" product_nat "reals/") (prod_nnr application-judgement "nnreal" product_nat "reals/") (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (product def-decl "real" product "reals/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (below type-eq-decl nil naturalnumbers nil) (fs2!1 skolem-const-decl "fseq[posnat]" product_perm_lems nil) (< const-decl "bool" reals nil) (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IX skolem-const-decl "int" product_perm_lems nil) (fs1!1 skolem-const-decl "fseq[posnat]" product_perm_lems nil) (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (swap const-decl "fseq[posnat]" product_perm_lems nil) (swap_len formula-decl nil product_perm_lems nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (^ const-decl "fseq" fseqs "structures/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (restrict const-decl "[T -> real]" product "reals/") (product_restrict_eq formula-decl nil product "reals/") (default const-decl "T" fseqs "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (fs2!1 skolem-const-decl "fseq[posnat]" product_perm_lems nil) (f!1 skolem-const-decl "[below(length(fs1!1)) -> below(length(fs2!1))]" product_perm_lems nil) (x!2 skolem-const-decl "below(length(fs1!1))" product_perm_lems nil) (x!1 skolem-const-decl "below(length(fs1!1))" product_perm_lems nil) (y!1 skolem-const-decl "below(length(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)))" product_perm_lems nil) (x2!1 skolem-const-decl "below(length(fs1!1 ^ (0, fs1!1`length - 2)))" product_perm_lems nil) (x1!1 skolem-const-decl "below(length(fs1!1 ^ (0, fs1!1`length - 2)))" product_perm_lems nil) (product_swap formula-decl nil product_perm_lems nil) (product_last formula-decl nil product "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (product_0_neg formula-decl nil product_nat "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (product const-decl "posnat" product_fseq_posnat "reals/") (permutation? const-decl "bool" permutations_fseq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (perm_length formula-decl nil permutations_fseq "structures/") (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) (restrict const-decl "R" restrict nil) (<= const-decl "bool" reals nil)) nil) (NEW "NEW" 3507373509 ("" (skeep) (("" (auto-rewrite "swap_len") (("" (postpone) nil nil)) nil)) nil) nil shostak) (product_permutation-3 nil 3413654613 ("" (skeep) (("" (auto-rewrite "swap_len") (("" (lemma "perm_length") (("" (inst - "fs1" "fs2") (("" (assert) (("" (assert) (("" (case "FORALL (n:nat, fs1, fs2: fseq[posnat]): n = length(fs1) IMPLIES (permutation?(fs1, fs2) IMPLIES product(fs1) = product(fs2))") (("1" (inst - "length(fs1)" "fs1" "fs2") (("1" (assert) nil nil)) nil) ("2" (induct "n") (("1" (skosimp*) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "product" +) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("2" (lift-if) (("2" (split +) (("1" (flatten) (("1" (hide -5) (("1" (lemma "perm_length") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide -4 -5) (("2" (lemma "perm_length") (("2" (inst?) (("2" (assert) (("2" (case "length(fs1!1) = 1") (("1" (expand "product") (("1" (replace -1) (("1" (assert) (("1" (case-replace "length(fs2!1) = 1") (("1" (assert) (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst -6 "0") (("1" (typepred "f!1(0)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "permutation?") (("2" (skosimp*) (("2" (name "IX" "l(fs1!1)-1") (("2" (inst-cp -6 "IX") (("1" (lemma "product_last") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_swap") (("1" (swap-rel 3) (("1" (inst - "fs2!1" "IX" "f!1(IX)") (("1" (expand "product" -1) (("1" (lift-if) (("1" (case "length(swap(fs2!1)(IX, f!1(IX))) = 0") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "product_last") (("2" (inst?) (("2" (case-replace "length(fs2!1) = 1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (case-replace "swap(fs2!1)(IX, f!1(IX))`seq(length(fs2!1) - 1) = fs1!1`seq(IX)") (("1" (hide -1) (("1" (inst - "fs1!1 ^ (0, fs1!1`length-2)" "swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length-2)") (("1" (assert) (("1" (split -3) (("1" (expand "product" -1) (("1" (assert) (("1" (case "l(fs1!1 ^ (0, fs1!1`length - 2)) = 0") (("1" (assert) (("1" (hide-all-but (-1 3 4)) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) (("2" (case "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = 0") (("1" (assert) (("1" (hide-all-but (-1 2 3)) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) (("2" (case-replace "l(fs1!1 ^ (0, fs1!1`length - 2)) = l(fs1!1)-1") (("1" (case-replace "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = l(fs2!1) -1") (("1" (assert) (("1" (hide -1 -2) (("1" (assert) (("1" (lemma "product_restrict_eq") (("1" (inst?) (("1" (inst - "fs1!1`seq") (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_restrict_eq") (("1" (inst?) (("1" (inst - "seqn(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2))") (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 8) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "restrict") (("2" (lift-if) (("2" (ground) (("2" (expand "swap") (("2" (lift-if) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 6) (("2" (inst + "(LAMBDA (jj: [below(l(fs1!1 ^ (0, l(fs1!1) - 2)))]): IF f!1(IX) = IX THEN f!1(jj) ELSIF f!1(jj) = IX THEN (f!1(IX)) ELSE f!1(jj) ENDIF)") (("1" (prop) (("1" (hide 6) (("1" (expand "bijective?") (("1" (flatten) (("1" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (typepred "x2!1") (("1" (expand "^") (("1" (lift-if) (("1" (lift-if) (("1" (inst-cp - "x1!1" "x2!1") (("1" (ground) (("1" (inst-cp - "IX" "x1!1") (("1" (inst-cp - "IX" "x2!1") (("1" (assert) nil nil)) nil)) nil) ("2" (lift-if) (("2" (split -1) (("1" (flatten) (("1" (inst-cp - "x1!1" "x2!1") (("1" (replace -1) (("1" (inst-cp - "IX" "x1!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (expand "swap") (("2" (expand "^") (("2" (inst - "y!1") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (expand "^") (("2" (assert) (("2" (typepred "x!1") (("2" (case "x!1 = IX") (("1" (expand "injective?") (("1" (reveal 1) (("1" (reveal -1) (("1" (inst - "IX") (("1" (skosimp*) (("1" (inst + "x!2") (("1" (assert) nil nil) ("2" (expand "^") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "ii!1") (("2" (expand "^") (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (inst - "ii!1") (("2" (expand "swap") (("2" (lift-if) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "injective?") (("2" (inst - "IX" "ii!1") (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "^") (("2" (expand "swap") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "jj!1") (("3" (grind) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "^") (("4" (expand "swap") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (typepred "jj!1") (("5" (expand "^") (("5" (assert) nil nil)) nil)) nil)) nil) ("6" (skosimp*) (("6" (expand "^") (("6" (expand "swap") (("6" (assert) (("6" (typepred "jj!1") (("6" (expand "^") (("6" (assert) (("6" (expand "bijective?") (("6" (flatten) (("6" (expand "injective?") (("6" (inst - "IX" "jj!1") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (skosimp*) (("7" (typepred "jj!1") (("7" (expand "^") (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 6) (("2" (expand "swap") (("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) ("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) ((perm_length formula-decl nil permutations_fseq "structures/") (permutation? const-decl "bool" permutations_fseq "structures/") (product const-decl "posnat" product_fseq_posnat "reals/") (T_low type-eq-decl nil product "reals/") (T_high type-eq-decl nil product "reals/") (^ const-decl "fseq" fseqs "structures/") (product_restrict_eq formula-decl nil product "reals/") (restrict const-decl "[T -> real]" product "reals/") (default const-decl "T" fseqs "structures/") (product_last formula-decl nil product "reals/") (product_0_neg formula-decl nil product_nat "reals/") (product def-decl "real" product "reals/") (prod_nnr application-judgement "nnreal" product_nat "reals/") (prod_nat application-judgement "nat" product_nat "reals/") (prod_pr application-judgement "posreal" product_nat "reals/") (prod_posnat application-judgement "posnat" product_nat "reals/") (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/")) nil) (product_permutation-2 nil 3413654380 ("" (skeep) (("" (auto-rewrite "swap_len") (("" (lemma "perm_length") (("" (inst - "fs1" "fs2") (("" (assert) (("" (assert) (("" (case "FORALL (n:nat, fs1, fs2: fseq[posnat]): n = length(fs1) IMPLIES (permutation?(fs1, fs2) IMPLIES product(fs1) = product(fs2))") (("1" (inst - "length(fs1)" "fs1" "fs2") (("1" (assert) nil nil)) nil) ("2" (induct "n") (("1" (skosimp*) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "product" +) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (hide -5) (("1" (lemma "perm_length") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -4 -5) (("2" (lemma "perm_length") (("2" (inst?) (("2" (assert) (("2" (case "length(fs1!1) = 1") (("1" (expand "product") (("1" (replace -1) (("1" (assert) (("1" (case-replace "length(fs2!1) = 1") (("1" (assert) (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst -6 "0") (("1" (typepred "f!1(0)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "permutation?") (("2" (skosimp*) (("2" (name "IX" "l(fs1!1)-1") (("2" (inst-cp -6 "IX") (("1" (lemma "product_last") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_swap") (("1" (swap-rel 3) (("1" (inst - "fs2!1" "IX" "f!1(IX)") (("1" (expand "product" -1) (("1" (lift-if) (("1" (case "length(swap(fs2!1)(IX, f!1(IX))) = 0") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "product_last") (("2" (inst?) (("2" (case-replace "length(fs2!1) = 1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (case-replace "swap(fs2!1)(IX, f!1(IX))`seq(length(fs2!1) - 1) = fs1!1`seq(IX)") (("1" (hide -1) (("1" (inst - "fs1!1 ^ (0, fs1!1`length-2)" "swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length-2)") (("1" (assert) (("1" (split -3) (("1" (expand "product" -1) (("1" (assert) (("1" (case "l(fs1!1 ^ (0, fs1!1`length - 2)) = 0") (("1" (assert) (("1" (hide-all-but (-1 3 4)) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) (("2" (case "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = 0") (("1" (assert) (("1" (hide-all-but (-1 2 3)) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) (("2" (case-replace "l(fs1!1 ^ (0, fs1!1`length - 2)) = l(fs1!1)-1") (("1" (case-replace "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = l(fs2!1) -1") (("1" (assert) (("1" (hide -1 -2) (("1" (assert) (("1" (lemma "product_restrict_eq") (("1" (inst?) (("1" (inst - "fs1!1`seq") (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_restrict_eq") (("1" (inst?) (("1" (inst - "seqn(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2))") (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 8) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "restrict") (("2" (lift-if) (("2" (ground) (("2" (expand "swap") (("2" (lift-if) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 6) (("2" (inst + "(LAMBDA (jj: [below(l(fs1!1 ^ (0, l(fs1!1) - 2)))]): IF f!1(IX) = IX THEN f!1(jj) ELSIF f!1(jj) = IX THEN (f!1(IX)) ELSE f!1(jj) ENDIF)") (("1" (prop) (("1" (hide 6) (("1" (expand "bijective?") (("1" (flatten) (("1" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (typepred "x2!1") (("1" (expand "^") (("1" (lift-if) (("1" (lift-if) (("1" (inst-cp - "x1!1" "x2!1") (("1" (ground) (("1" (inst-cp - "x1!1" "x2!1") (("1" (replace -1) (("1" (inst-cp - "IX" "x1!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst-cp - "IX" "x1!1") (("2" (inst-cp - "IX" "x2!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (expand "swap") (("2" (expand "^") (("2" (inst - "y!1") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (expand "^") (("2" (assert) (("2" (typepred "x!1") (("2" (case "x!1 = IX") (("1" (expand "injective?") (("1" (reveal 1) (("1" (reveal -1) (("1" (inst - "IX") (("1" (skosimp*) (("1" (inst + "x!2") (("1" (assert) nil nil) ("2" (expand "^") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lift-if) (("2" (inst - "ii!1") (("1" (assert) (("1" (prop) (("1" (typepred "ii!1") (("1" (expand "^") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (expand "swap") (("1" (propax) nil nil)) nil) ("2" (expand "bijective?") (("2" (flatten) (("2" (expand "injective?") (("2" (inst-cp - "IX" "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "ii!1") (("2" (expand "^") (("2" (assert) (("2" (expand "swap") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (typepred "ii!1") (("3" (expand "^") (("3" (assert) (("3" (expand "swap") (("3" (lift-if) (("3" (assert) (("3" (ground) (("3" (expand "bijective?") (("3" (flatten) (("3" (expand "injective?") (("3" (inst-cp - "IX" "ii!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "ii!1") (("2" (expand "^") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "^") (("2" (expand "swap") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "jj!1") (("3" (grind) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "^") (("4" (expand "swap") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (typepred "jj!1") (("5" (expand "^") (("5" (assert) nil nil)) nil)) nil)) nil) ("6" (skosimp*) (("6" (expand "^") (("6" (expand "swap") (("6" (assert) (("6" (typepred "jj!1") (("6" (expand "^") (("6" (assert) (("6" (expand "bijective?") (("6" (flatten) (("6" (expand "injective?") (("6" (inst - "IX" "jj!1") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (skosimp*) (("7" (typepred "jj!1") (("7" (expand "^") (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 6) (("2" (expand "swap") (("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) ("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) ((perm_length formula-decl nil permutations_fseq "structures/") (permutation? const-decl "bool" permutations_fseq "structures/") (product const-decl "posnat" product_fseq_posnat "reals/") (product_0_neg formula-decl nil product_nat "reals/") (product_last formula-decl nil product "reals/") (default const-decl "T" fseqs "structures/") (restrict const-decl "[T -> real]" product "reals/") (product_restrict_eq formula-decl nil product "reals/") (^ const-decl "fseq" fseqs "structures/") (T_high type-eq-decl nil product "reals/") (T_low type-eq-decl nil product "reals/") (product def-decl "real" product "reals/") (prod_nnr application-judgement "nnreal" product_nat "reals/") (prod_nat application-judgement "nat" product_nat "reals/") (prod_pr application-judgement "posreal" product_nat "reals/") (prod_posnat application-judgement "posnat" product_nat "reals/") (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/")) nil) (product_permutation-1 nil 3410089666 ("" (skeep) (("" (auto-rewrite "swap_len") (("" (lemma "perm_length") (("" (inst - "fs1" "fs2") (("" (assert) (("" (assert) (("" (case "FORALL (n:nat, fs1, fs2: fseq[posnat]): n = length(fs1) IMPLIES (permutation?(fs1, fs2) IMPLIES product(fs1) = product(fs2))") (("1" (inst - "length(fs1)" "fs1" "fs2") (("1" (assert) nil nil)) nil) ("2" (induct "n") (("1" (skosimp*) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "product" +) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (hide -5) (("1" (lemma "perm_length") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -4 -5) (("2" (lemma "perm_length") (("2" (inst?) (("2" (assert) (("2" (case "length(fs1!1) = 1") (("1" (expand "product") (("1" (replace -1) (("1" (assert) (("1" (case-replace "length(fs2!1) = 1") (("1" (assert) (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst -6 "0") (("1" (typepred "f!1(0)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "permutation?") (("2" (skosimp*) (("2" (name "IX" "l(fs1!1)-1") (("2" (inst-cp -6 "IX") (("1" (lemma "product_last") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_swap") (("1" (swap-rel 3) (("1" (inst - "fs2!1" "IX" "f!1(IX)") (("1" (expand "product" -1) (("1" (lift-if) (("1" (case "length(swap(fs2!1)(IX, f!1(IX))) = 0") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "product_last") (("2" (inst?) (("2" (case-replace "length(fs2!1) = 1") (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (case-replace "swap(fs2!1)(IX, f!1(IX))`seq(length(fs2!1) - 1) = fs1!1`seq(IX)") (("1" (hide -1) (("1" (inst - "fs1!1 ^ (0, fs1!1`length-2)" "swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length-2)") (("1" (assert) (("1" (split -3) (("1" (expand "product" -1) (("1" (assert) (("1" (case "l(fs1!1 ^ (0, fs1!1`length - 2)) = 0") (("1" (assert) (("1" (hide-all-but (-1 3 4)) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) (("2" (case "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = 0") (("1" (assert) (("1" (hide-all-but (-1 2 3)) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) (("2" (case-replace "l(fs1!1 ^ (0, fs1!1`length - 2)) = l(fs1!1)-1") (("1" (case-replace "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = l(fs2!1) -1") (("1" (assert) (("1" (hide -1 -2) (("1" (assert) (("1" (lemma "product_restrict_eq") (("1" (inst?) (("1" (inst - "fs1!1`seq") (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "product_restrict_eq") (("1" (inst?) (("1" (inst - "seqn(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2))") (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 8) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "restrict") (("2" (lift-if) (("2" (ground) (("2" (expand "swap") (("2" (lift-if) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "(LAMBDA (jj: [below(l(fs1!1 ^ (0, l(fs1!1) - 2)))]): IF f!1(jj) = IX THEN (f!1(IX)) ELSE f!1(jj) ENDIF)") (("1" (prop) (("1" (hide 6) (("1" (expand "bijective?") (("1" (flatten) (("1" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (typepred "x1!1") (("1" (typepred "x2!1") (("1" (expand "^") (("1" (lift-if) (("1" (lift-if) (("1" (inst-cp - "x1!1" "x2!1") (("1" (ground) (("1" (inst-cp - "x1!1" "x2!1") (("1" (replace -1) (("1" (inst-cp - "IX" "x1!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst-cp - "IX" "x1!1") (("2" (inst-cp - "IX" "x2!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (expand "swap") (("2" (expand "^") (("2" (inst - "y!1") (("1" (skosimp*) (("1" (case "f!1(x!1) = IX") (("1" (inst + "x!1") (("1" (assert) nil nil) ("2" (ground) nil nil)) nil) ("2" (typepred "x!1") (("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 6) (("2" (expand "^") (("2" (expand "swap") (("2" (typepred "ii!1") (("2" (expand "^") (("2" (assert) (("2" (lift-if) (("2" (case " f!1(ii!1) = IX") (("1" (assert) (("1" (lift-if) (("1" (prop) (("1" (inst -8 "ii!1") (("1" (assert) nil nil)) nil) ("2" (expand "bijective?") (("2" (flatten) (("2" (expand "injective?") (("2" (inst - "ii!1" "IX") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (expand "bijective?") (("1" (flatten) (("1" (expand "injective?") (("1" (inst - "ii!1" "IX") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "ii!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 7) (("2" (expand "^") (("2" (expand "swap") (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "injective?") (("2" (inst - "jj!1" "IX") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (hide 7) (("3" (typepred "j!1") (("3" (typepred "jj!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (hide 6) (("4" (expand "^") (("4" (expand "swap") (("4" (expand "bijective?") (("4" (flatten) (("4" (expand "injective?") (("4" (inst - "jj!1" "IX") (("4" (assert) (("4" (typepred "jj!1") (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (typepred "jj!1") (("5" (grind) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 6) (("2" (expand "swap") (("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) ("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 shostak)) (length_sort 0 (length_sort-1 nil 3410089654 ("" (skosimp*) (("" (typepred "sort(fs!1)") (("1" (lemma "perm_length") (("1" (inst?) (("1" (assert) (("1" (hide -2 2) (("1" (lemma "perm_symmetric") (("1" (inst?) (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ((sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq "structures/") (increasing? const-decl "bool" sort_fseq "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (permutation? const-decl "bool" permutations_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (fsq type-eq-decl nil fsq "structures/") (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (sort_length formula-decl nil sort_fseq "structures/") (perm_length formula-decl nil permutations_fseq "structures/")) nil)) (product_sort 0 (product_sort-1 nil 3410089654 ("" (skosimp*) (("" (lemma "product_permutation") (("" (inst?) (("1" (assert) (("1" (expand "permutation_of?") (("1" (assert) (("1" (hide 2) (("1" (typepred "sort(fs!1)") (("1" (hide -2) (("1" (lemma "perm_symmetric") (("1" (inst -1 "fs!1" "sort(fs!1)") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ((product_permutation formula-decl nil product_perm_lems nil) (NOT const-decl "[bool -> bool]" booleans nil) (perm_symmetric formula-decl nil permutations_fseq "structures/") (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq "structures/") (increasing? const-decl "bool" sort_fseq "structures/") (permutation? const-decl "bool" permutations_fseq "structures/") (<= const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (fsq type-eq-decl nil fsq "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs "structures/") (barray type-eq-decl nil fseqs "structures/") (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (total_order_restrict application-judgement "(total_order?[S])" restrict_order_props nil) (dichotomous_restrict application-judgement "(dichotomous?[S])" restrict_order_props nil) (partial_order_restrict application-judgement "(partial_order?[S])" restrict_order_props nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil)) nil)))
¤ 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.0.537Bemerkung: (vorverarbeitet am 2026-04-27) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26