| products/sources/formale Sprachen/PVS/numbers/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: const_fun_def.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
(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") --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.853 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
