SSL product_perm_lems.prf
Sprache: Lisp
(product_perm_lemsnil 3413557357"" (skeep)"" (skeep)"" (lift-if)"" (ground)"" (typepred "fs`seq" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil nil ))nil 3413558127 ("" (grind) nil nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"T" fseqs "structures/" )"fseq[posnat]" product_perm_lems nil ))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 )nil naturalnumbers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil fseqs "structures/" )nil fseqs "structures/" )"fseq[posnat]" product_perm_lems nil )"T" fseqs "structures/" )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil ))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 )nil naturalnumbers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil fseqs "structures/" )nil fseqs "structures/" )"fseq[posnat]" product_perm_lems nil )"T" fseqs "structures/" )"(total_order?[real])" nil ))nil 3413560184 ("" (subtype-tcc) nil nil ) nil nil ))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 )nil product "reals/" )nil integers nil )"bool" reals nil )nil integers nil )nil fseqs "structures/" )nil fseqs "structures/" )"fseq[posnat]" product_perm_lems nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil product "reals/" )nil product "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"posnat" product_fseq_posnat"reals/" )"(total_order?[real])" nil )"[T -> real]" product "reals/" )"(total_order?[real])" nil )"T" fseqs "structures/" )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil ))nil 3413563853 ("" (subtype-tcc) nil nil ) nil nil ))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 )nil product "reals/" )nil integers nil )"bool" reals nil )nil integers nil )nil fseqs "structures/" )nil fseqs "structures/" )"fseq[posnat]" product_perm_lems nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil product "reals/" )nil product "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"posnat" product_fseq_posnat"reals/" )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[T -> real]" product "reals/" )"(total_order?[real])" nil )"T" fseqs "structures/" )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil ))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 ") "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" "2" "product_last" )"2" "2" assert )"2" replace -1 * lr)"2" "2" "2" "product_split_ge" )"2" "2" "j!2" )"2" assert )"2" replace -1)"2" "2" "product_last" )"2" "2" assert )"2" replace "2" "2" "prod_swap_prep" )"2" "fs!1" "i!2" "j!2" "1+j!2" "l(fs!1)-1" )"2" assert )"2" replace "2" "2" "i!2 = 0" )"1" assert )"1" rewrite "prod_swap_prep2" )"1" "1" expand "swap" )"1" "1" "product_first" )"1" "1" assert )"1" replace "1" "1" "1" "product_split_ge" )"1" "1" "j!2" )"1" assert )"1" replace "1" "1" "product_last" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "prod_swap_prep" )"2" "fs!1" "i!2" "j!2" "0" "i!2-1" )"1" assert )"1" replace "1" "1" rewrite "prod_swap_prep2" )"1" "1" "1" expand "swap" )"1" "1" "product_split_ge" )"1" "1" "i!2" )"1" assert )"1" replace "1" "1" "product_last" )"1" "1" assert )"1" replace "1" "1" assert )"1" "1" "product_split_ge" )"1" "1" "j!2" )"1" assert )"1" replace "1" "1" "product_last" )"1" "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 )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil product_perm_lems nil )nil product_nat "reals/" )nil product "reals/" )"(total_order?[real])" nil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )nil product_perm_lems nil )nil product "reals/" )"even_int" integersnil )"[bool, bool -> bool]" booleans nil )nil product_nat "reals/" )"odd_int" integers nil )"fseq[posnat]" product_perm_lems nil )"below(length(fs!1))" product_perm_lems nil )"(strict_total_order?[real])" real_props nil )nil product_perm_lems nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"odd_int" integersnil )"posnat" product_fseq_posnat"reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil product_perm_lems nil )nil product_perm_lems nil )"nnreal" product_nat "reals/" )"nat" product_nat "reals/" )"posreal" product_nat "reals/" )"posnat" product_nat "reals/" )"int" integers nil )"[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil product "reals/" )nil product "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"fseq[posnat]" product_perm_lems nil )"real" product "reals/" )"posnat" product_fseq_posnat "reals/" ))nil 3413654632"" (skosimp*)"" (expand "permutation?" )"" "(LAMBDA (jj: below(length(swap(fs!1)(i!1, j!1)))): IF jj = i!1 THEN j!1") "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 )"bool" permutations_fseq "structures/" )"bool" functions nil )"(strict_total_order?[real])" real_props nil )"below(length(fs!1))" product_perm_lems nil )"T" fseqs "structures/" )"bool" functions nil )"bool" functions nil )"(total_order?[real])" nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil fseqs "structures/" )nil fseqs "structures/" )"fseq[posnat]" product_perm_lems nil )"fseq[posnat]" product_perm_lems nil )nil naturalnumbers nil )"below(length(fs!1))" product_perm_lems nil )"below(length(fs!1))" product_perm_lems nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil ))"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 ") "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" "1" "perm_length" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "perm_length" )"2" "2" assert )"2" case "length(fs1!1) = 1" )"1" expand "product" )"1" replace -1)"1" assert )"1" "length(fs2!1) = 1" )"1" assert )"1" expand "permutation?" )"1" "1" "0" )"1" "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" "2" "IX" "l(fs1!1)-1" )"2" "IX" )"1" "product_last" )"1" "1" assert )"1" replace "1" replace "1" "1" "product_swap" )"1" "1" "fs2!1" "IX" "f!1(IX)" )"1" expand "product" "1" "1" case "length(swap(fs2!1)(IX, f!1(IX))) = 0" )"1" assert )nil nil )"2" assert )"2" "product_last" )"2" "2" "length(fs2!1) = 1" )"2" assert )"2" replace "2" "2" replace "2" "2" "swap(fs2!1)(IX, f!1(IX))`seq(length(fs2!1) - 1) = fs1!1`seq(IX)" )"1" "1" "fs1!1 ^ (0, fs1!1`length-2)" "swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length-2)" )"1" assert )"1" "1" expand "product" "1" assert )"1" case "l(fs1!1 ^ (0, fs1!1`length - 2)) = 0" )"1" assert )"1" "1" 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" "1" nil nil ))nil ))nil )"2" assert )"2" "l(fs1!1 ^ (0, fs1!1`length - 2)) = l(fs1!1)-1" )"1" "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = l(fs2!1) -1" )"1" assert )"1" "1" "product_restrict_eq" )"1" "structures@fseqs[posnat].^(fs1!1, (0, fs1!1`length - 2))`seq" "fs1!1`seq" "fs1!1`length - 2" "0" )"1" "1" replace "1" "1" replace "1" "1" assert )"1" "product_restrict_eq" )"1" "1" "swap(fs2!1)(IX, f!1(IX))`seq" )"1" "1" assert )nil nil )"2" "2" "2" expand "restrict" )"2" "2" assert )"2" "2" expand "swap" )"2" "2" expand "^" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" "2" "2" expand "^" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "(LAMBDA (jj: [below(l(fs1!1 ^ (0, l(fs1!1) - 2)))]): IF f!1(IX) = IX THEN f!1(jj)") "1" "1" "1" expand "bijective?" )"1" "1" "1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" expand "^" )"1" "1" "1" "x1!1" "x2!1" )"1" "1" "IX" "x1!1" )"1" "IX" "x2!1" )"1" assert )nil nil ))nil ))nil )"2" case "f!1(x2!1) = IX" )"1" assert )"1" "x1!1" "x2!1" )"1" replace "1" "IX" "x1!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" expand "swap" )"2" expand "^" )"2" "y!1" )"1" "1" "x!1" )"1" "1" nil nil ))nil )"2" expand "^" )"2" assert )"2" "x!1" )"2" case "x!1 = IX" )"1" expand "injective?" )"1" "1" "1" "IX" )"1" "1" "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" "2" "ii!1" )"2" expand "^" )"2" assert )"2" "2" "2" "ii!1" )"2" expand "swap" )"2" "2" expand "bijective?" )"2" "2" expand "injective?" )"2" "IX" "ii!1" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "^" )"2" expand "swap" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" "jj!1" )"3" nil nil ))nil ))nil )"4" "4" expand "^" )"4" expand "swap" )"4" assert )nil nil ))nil ))nil ))nil )"5" "5" "jj!1" )"5" expand "^" )"5" assert )nil nil ))nil ))nil ))nil )"6" "6" expand "^" )"6" expand "swap" )"6" assert )"6" "jj!1" )"6" expand "^" )"6" assert )"6" expand "bijective?" )"6" "6" expand "injective?" )"6" "IX" "jj!1" )"6" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" "7" "jj!1" )"7" expand "^" )"7" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "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 naturalnumbers nil )nil fsq "structures/" )nil fseqs "structures/" )nil fseqs "structures/" )nil defined_types nil )nil naturalnumbers nil )"int" integers nil )"posnat" product_nat "reals/" )"posreal" product_nat "reals/" )"nat" product_nat "reals/" )"nnreal" product_nat "reals/" )"bool" functions nil )"bool" functions nil )"bool" functions nil )"real" product "reals/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )nil naturalnumbers nil )"fseq[posnat]" product_perm_lems nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"int" product_perm_lems nil )"fseq[posnat]" product_perm_lems nil )nil product "reals/" )nil product "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"fseq[posnat]" product_perm_lems nil )nil product_perm_lems nil )"odd_int" integers nil )"fseq" fseqs "structures/" )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T -> real]" product "reals/" )nil product "reals/" )"T" fseqs "structures/" )"(strict_total_order?[real])" real_props nil )"int" integers nil )"fseq[posnat]" product_perm_lems nil )"[below(length(fs1!1)) -> below(length(fs2!1))]" product_perm_lemsnil )"below(length(fs1!1))" product_perm_lemsnil )"below(length(fs1!1))" product_perm_lemsnil )"below(length(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)))" nil )"below(length(fs1!1 ^ (0, fs1!1`length - 2)))" product_perm_lemsnil )"below(length(fs1!1 ^ (0, fs1!1`length - 2)))" product_perm_lemsnil )nil product_perm_lems nil )nil product "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"odd_int" integersnil )"even_int" integersnil )nil product_nat "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"posnat" product_fseq_posnat "reals/" )"bool" permutations_fseq "structures/" )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )nil permutations_fseq "structures/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"R" restrict nil )"bool" reals nil ))nil )"NEW" 3507373509"" (skeep)"" (auto-rewrite "swap_len" ) (("" (postpone) nil nil )) nil )) nil )nil shostak)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 ") "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" "2" "1" "1" "1" "perm_length" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "perm_length" )"2" "2" assert )"2" case "length(fs1!1) = 1" )"1" expand "product" )"1" replace -1)"1" assert )"1" "length(fs2!1) = 1" )"1" assert )"1" expand "permutation?" )"1" "1" "0" )"1" "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" "2" "IX" "l(fs1!1)-1" )"2" "IX" )"1" "product_last" )"1" "1" assert )"1" replace "1" replace "1" "1" "product_swap" )"1" "1" "fs2!1" "IX" "f!1(IX)" )"1" expand "product" "1" "1" case "length(swap(fs2!1)(IX, f!1(IX))) = 0" )"1" assert )nil nil )"2" assert )"2" "product_last" )"2" "2" "length(fs2!1) = 1" )"2" assert )"2" replace "2" "2" replace "2" "2" "swap(fs2!1)(IX, f!1(IX))`seq(length(fs2!1) - 1) = fs1!1`seq(IX)" )"1" "1" "fs1!1 ^ (0, fs1!1`length-2)" "swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length-2)" )"1" assert )"1" "1" expand "product" "1" assert )"1" case "l(fs1!1 ^ (0, fs1!1`length - 2)) = 0" )"1" assert )"1" "1" 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" "1" nil nil ))nil ))nil )"2" assert )"2" "l(fs1!1 ^ (0, fs1!1`length - 2)) = l(fs1!1)-1" )"1" "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = l(fs2!1) -1" )"1" assert )"1" "1" assert )"1" "product_restrict_eq" )"1" "1" "fs1!1`seq" )"1" "1" replace "1" "1" replace "1" "1" "product_restrict_eq" )"1" "1" "seqn(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2))" )"1" "1" assert )nil nil )"2" "2" "2" expand "restrict" )"2" "2" "2" expand "swap" )"2" "2" expand "^" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" "2" "2" expand "^" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "(LAMBDA (jj: [below(l(fs1!1 ^ (0, l(fs1!1) - 2)))]): IF f!1(IX) = IX THEN f!1(jj)") "1" "1" "1" expand "bijective?" )"1" "1" "1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" expand "^" )"1" "1" "1" "x1!1" "x2!1" )"1" "1" "IX" "x1!1" )"1" "IX" "x2!1" )"1" assert )nil nil ))nil ))nil )"2" "2" "1" "1" "x1!1" "x2!1" )"1" replace "1" "IX" "x1!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" expand "swap" )"2" expand "^" )"2" "y!1" )"1" "1" "x!1" )"1" "1" nil nil ))nil )"2" expand "^" )"2" assert )"2" "x!1" )"2" case "x!1 = IX" )"1" expand "injective?" )"1" "1" "1" "IX" )"1" "1" "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" "2" "ii!1" )"2" expand "^" )"2" assert )"2" "2" "2" "ii!1" )"2" expand "swap" )"2" "2" expand "bijective?" )"2" "2" expand "injective?" )"2" "IX" "ii!1" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "^" )"2" expand "swap" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" "jj!1" )"3" nil nil ))nil ))nil )"4" "4" expand "^" )"4" expand "swap" )"4" assert )nil nil ))nil ))nil ))nil )"5" "5" "jj!1" )"5" expand "^" )"5" assert )nil nil ))nil ))nil ))nil )"6" "6" expand "^" )"6" expand "swap" )"6" assert )"6" "jj!1" )"6" expand "^" )"6" assert )"6" expand "bijective?" )"6" "6" expand "injective?" )"6" "IX" "jj!1" )"6" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" "7" "jj!1" )"7" expand "^" )"7" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "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 )nil permutations_fseq "structures/" )"bool" permutations_fseq "structures/" )"posnat" product_fseq_posnat "reals/" )nil product "reals/" )nil product "reals/" )"fseq" fseqs "structures/" )nil product "reals/" )"[T -> real]" product "reals/" )"T" fseqs "structures/" )nil product "reals/" )nil product_nat "reals/" )"real" product "reals/" )"nnreal" product_nat "reals/" )"nat" product_nat "reals/" )"posreal" product_nat "reals/" )"posnat" product_nat "reals/" )nil fseqs "structures/" )nil fseqs "structures/" ))nil )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 ") "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" "1" "perm_length" )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "perm_length" )"2" "2" assert )"2" case "length(fs1!1) = 1" )"1" expand "product" )"1" replace -1)"1" assert )"1" "length(fs2!1) = 1" )"1" assert )"1" expand "permutation?" )"1" "1" "0" )"1" "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" "2" "IX" "l(fs1!1)-1" )"2" "IX" )"1" "product_last" )"1" "1" assert )"1" replace -2)"1" replace "1" "1" "product_swap" )"1" "1" "fs2!1" "IX" "f!1(IX)" )"1" expand "product" "1" "1" case "length(swap(fs2!1)(IX, f!1(IX))) = 0" )"1" assert )nil nil )"2" assert )"2" "product_last" )"2" "2" "length(fs2!1) = 1" )"2" assert )"2" replace "2" "2" replace "2" "2" "swap(fs2!1)(IX, f!1(IX))`seq(length(fs2!1) - 1) = fs1!1`seq(IX)" )"1" "1" "fs1!1 ^ (0, fs1!1`length-2)" "swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length-2)" )"1" assert )"1" "1" expand "product" "1" assert )"1" case "l(fs1!1 ^ (0, fs1!1`length - 2)) = 0" )"1" assert )"1" "1" 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" "1" nil nil ))nil ))nil )"2" assert )"2" "l(fs1!1 ^ (0, fs1!1`length - 2)) = l(fs1!1)-1" )"1" "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = l(fs2!1) -1" )"1" assert )"1" "1" assert )"1" "product_restrict_eq" )"1" "1" "fs1!1`seq" )"1" "1" replace "1" "1" replace "1" "1" "product_restrict_eq" )"1" "1" "seqn(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2))" )"1" "1" assert )nil nil )"2" "2" "2" expand "restrict" )"2" "2" "2" expand "swap" )"2" "2" expand "^" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" "2" "2" expand "^" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "(LAMBDA (jj: [below(l(fs1!1 ^ (0, l(fs1!1) - 2)))]): IF f!1(IX) = IX THEN f!1(jj)") "1" "1" "1" expand "bijective?" )"1" "1" "1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" expand "^" )"1" "1" "1" "x1!1" "x2!1" )"1" "1" "x1!1" "x2!1" )"1" replace "1" "IX" "x1!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "IX" "x1!1" )"2" "IX" "x2!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" expand "swap" )"2" expand "^" )"2" "y!1" )"1" "1" "x!1" )"1" "1" nil nil ))nil )"2" expand "^" )"2" assert )"2" "x!1" )"2" case "x!1 = IX" )"1" expand "injective?" )"1" "1" "1" "IX" )"1" "1" "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" "2" "2" "ii!1" )"1" assert )"1" "1" "ii!1" )"1" expand "^" )"1" assert )"1" "1" "1" expand "swap" )"1" nil nil ))nil )"2" expand "bijective?" )"2" "2" expand "injective?" )"2" "IX" "ii!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ii!1" )"2" expand "^" )"2" assert )"2" expand "swap" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "ii!1" )"3" expand "^" )"3" assert )"3" expand "swap" )"3" "3" assert )"3" "3" expand "bijective?" )"3" "3" expand "injective?" )"3" "IX" "ii!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "ii!1" )"2" expand "^" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "^" )"2" expand "swap" )"2" assert )nil nil ))nil ))nil ))nil )"3" "3" "jj!1" )"3" nil nil ))nil ))nil )"4" "4" expand "^" )"4" expand "swap" )"4" assert )nil nil ))nil ))nil ))nil )"5" "5" "jj!1" )"5" expand "^" )"5" assert )nil nil ))nil ))nil ))nil )"6" "6" expand "^" )"6" expand "swap" )"6" assert )"6" "jj!1" )"6" expand "^" )"6" assert )"6" expand "bijective?" )"6" "6" expand "injective?" )"6" "IX" "jj!1" )"6" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" "7" "jj!1" )"7" expand "^" )"7" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "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 permutations_fseq "structures/" )"bool" permutations_fseq "structures/" )"posnat" product_fseq_posnat "reals/" )nil product_nat "reals/" )nil product "reals/" )"T" fseqs "structures/" )"[T -> real]" product "reals/" )nil product "reals/" )"fseq" fseqs "structures/" )nil product "reals/" )nil product "reals/" )"real" product "reals/" )"nnreal" product_nat "reals/" )"nat" product_nat "reals/" )"posreal" product_nat "reals/" )"posnat" product_nat "reals/" )nil fseqs "structures/" )nil fseqs "structures/" ))nil )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 ") "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" "1" "perm_length" )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "perm_length" )"2" "2" assert )"2" case "length(fs1!1) = 1" )"1" expand "product" )"1" replace -1)"1" assert )"1" "length(fs2!1) = 1" )"1" assert )"1" expand "permutation?" )"1" "1" "0" )"1" "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" "2" "IX" "l(fs1!1)-1" )"2" "IX" )"1" "product_last" )"1" "1" assert )"1" replace -2)"1" replace "1" "1" "product_swap" )"1" "1" "fs2!1" "IX" "f!1(IX)" )"1" expand "product" "1" "1" case "length(swap(fs2!1)(IX, f!1(IX))) = 0" )"1" assert )nil nil )"2" assert )"2" "product_last" )"2" "2" "length(fs2!1) = 1" )"2" assert )"2" replace "2" "2" replace "2" "2" "swap(fs2!1)(IX, f!1(IX))`seq(length(fs2!1) - 1) = fs1!1`seq(IX)" )"1" "1" "fs1!1 ^ (0, fs1!1`length-2)" "swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length-2)" )"1" assert )"1" "1" expand "product" "1" assert )"1" case "l(fs1!1 ^ (0, fs1!1`length - 2)) = 0" )"1" assert )"1" "1" 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" "1" nil nil ))nil ))nil )"2" assert )"2" "l(fs1!1 ^ (0, fs1!1`length - 2)) = l(fs1!1)-1" )"1" "l(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2)) = l(fs2!1) -1" )"1" assert )"1" "1" assert )"1" "product_restrict_eq" )"1" "1" "fs1!1`seq" )"1" "1" replace "1" "1" replace "1" "1" "product_restrict_eq" )"1" "1" "seqn(swap(fs2!1)(IX, f!1(IX)) ^ (0, fs2!1`length - 2))" )"1" "1" assert )nil nil )"2" "2" "2" expand "restrict" )"2" "2" "2" expand "swap" )"2" "2" expand "^" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "restrict" )"2" "2" "2" expand "^" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "(LAMBDA (jj: [below(l(fs1!1 ^ (0, l(fs1!1) - 2)))]): IF f!1(jj) = IX THEN (f!1(IX))") "1" "1" "1" expand "bijective?" )"1" "1" "1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" expand "^" )"1" "1" "1" "x1!1" "x2!1" )"1" "1" "x1!1" "x2!1" )"1" replace "1" "IX" "x1!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "IX" "x1!1" )"2" "IX" "x2!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" expand "swap" )"2" expand "^" )"2" "y!1" )"1" "1" case "f!1(x!1) = IX" )"1" "x!1" )"1" assert )nil nil )"2" nil nil ))nil )"2" "x!1" )"2" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "^" )"2" expand "swap" )"2" "ii!1" )"2" expand "^" )"2" assert )"2" "2" case " f!1(ii!1) = IX" )"1" assert )"1" "1" "1" "ii!1" )"1" assert )nil nil ))nil )"2" expand "bijective?" )"2" "2" expand "injective?" )"2" "ii!1" "IX" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "1" expand "bijective?" )"1" "1" expand "injective?" )"1" "ii!1" "IX" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "ii!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "^" )"2" expand "swap" )"2" expand "bijective?" )"2" "2" expand "injective?" )"2" "jj!1" "IX" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )"3" "3" "j!1" )"3" "jj!1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" expand "^" )"4" expand "swap" )"4" expand "bijective?" )"4" "4" expand "injective?" )"4" "jj!1" "IX" )"4" assert )"4" "jj!1" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "5" "jj!1" )"5" nil nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "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))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 )"{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" "structures/" )"bool" sort_fseq "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )"bool" permutations_fseq "structures/" )"bool" reals nil )"R" restrict nil )nil fsq "structures/" )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )nil sort_fseq "structures/" )nil permutations_fseq "structures/" ))nil ))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 )nil product_perm_lems nil )NOT const-decl "[bool -> bool]" booleans nil )nil permutations_fseq "structures/" )"{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" "structures/" )"bool" sort_fseq "structures/" )"bool" permutations_fseq "structures/" )"bool" reals nil )"R" restrict nil )nil fsq "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil naturalnumbers nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.462 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
