Quelle monotone_subsequence.prf
Sprache: Lisp
(monotone_subsequencenil 3507029426"" (skolem + (_ "u!1" ))"" (induct "n" )"1" (reduce) nil nil )"2" (skosimp*)"2" "IF u!1(i!1) <= u!1(j!1+1) THEN i!1 ELSE j!1+1 ENDIF" )"2" (skosimp)"2" (inst - "j!2" ) (("2" (smash) nil nil )) nil )) nil ))nil ))nil ))nil ))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 )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sequences nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )"posint" nil ))nil ))nil 3507029426"" (grind :if-match nil )"" (use "minimum_prefix" ("n" "n!1" ))"" (skolem!)"" (inst + "IF u!1(i!2) <= u!1(i!1) THEN i!2 ELSE i!1 ENDIF" )"" (skolem!)"" (inst - "j!1" )"" (inst - "j!1" ) (("" (smash) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil monotone_subsequence nil )nil sequences nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" monotone_subsequence nil ))nil ))nil 3507029426"" (skolem!)"" (name-replace "m" "mini(v!1, n!1)" :hide? nil )"" (expand "mini" )"" (use "epsilon_ax[nat]" )"" (replace -2)"" (delete -2)"" (split)"1" (propax) nil nil )"2" (typepred "v!1" )"2" (inst?)"2" (expand "has_minimum" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities 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 )nil sequences nil )"bool" monotone_subsequence nil )"nat" monotone_subsequence nil )nil epsilons nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3507029426"" (skolem!) (("" (use "min_prop" ) (("" (flatten) nil nil )) nil ))nil )nil monotone_subsequence nil )"bool" monotone_subsequence nil )nil sequences 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 )nil booleans nil )nil numbers nil ))nil ))nil 3507029426"" (skosimp) (("" (use "min_prop" ) (("" (reduce) nil nil )) nil ))nil )nil monotone_subsequence nil )"bool" monotone_subsequence nil )nil sequences 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 )nil booleans nil )nil numbers nil )"(total_order?[real])" nil ))nil ))nil 3507029426 ("" (skosimp) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3507029426 ("" (skosimp) (("" (assert ) nil nil )) nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3507029426"" (skolem!)"" (rewrite "strict_incr_condition" )"" (skolem!)"" (expand "h" 1 2)"" (use "min_prop1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil sequence_props 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 )nil sequences nil )"bool" monotone_subsequence nil )"nat" monotone_subsequence nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil monotone_subsequence nil ))nil ))nil 3507029426"" (skolem!)"" (expand * "hseq" "subseq" )"" (inst + "h(v!1)" )"1" (assert ) nil nil ) ("2" (rewrite "h_increasing" ) nil nil ))nil ))nil ))nil )"bool" sequence_props nil )"sequence[real]" monotone_subsequence nil )nil monotone_subsequence nil )nil sequence_props 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" real_fun_preds "reals/" )nil sequences nil )"bool" monotone_subsequence nil )"nat" monotone_subsequence nil )"{u | FORALL n: has_minimum(u, n)}" nil ))nil ))nil 3507029426"" (skolem!)"" (rewrite "incr_condition" )"" (skolem!)"" (expand "hseq" )"" (name-replace "k" "h(v!1)(i!1)" :hide? nil )"" (expand "h" -1)"" (smash)"1" (use "min_prop2" ("i" "h(v!1)(1 + i!1)" ))"1" (assert ) nil nil )) nil )"2" (use "min_prop2" ("i" "h(v!1)(1 + i!1)" ))"2" (assert )"2" (use "h_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "i!1 - 1" "1 + i!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sequence_props 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 )nil sequences nil )"bool" monotone_subsequence nil )"sequence[real]" monotone_subsequence nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil monotone_subsequence nil )"(strict_total_order?[real])" real_props nil )"bool" real_fun_preds "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil monotone_subsequence nil )"int" integers nil )"posint" nil )"(total_order?[real])" nil )"nat" monotone_subsequence nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3507029426"" (skolem-typepred)"" (forward-chain "minimum_suffix" ) nil nil )) nil )nil monotone_subsequence nil )"bool" monotone_subsequence nil )nil sequences nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3507029426"" (skolem!)"" (name-replace "k" "pick(w!1, n!1)" :hide? nil )"" (expand "pick" )"" "epsilon_ax" "p" "LAMBDA (i : nat) : n!1 <= i AND w!1(i) < w!1(n!1)" ))"" (replace -2)"" (assert )"" (split)"1" (propax) nil nil )"2" (delete -1 2)"2" (use "no_minimum" ("n" "n!1" ))"2" (expand "has_minimum" )"2" (inst?)"2" (assert )"2" (skosimp)"2" (inst?) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities 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 )nil sequences nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" monotone_subsequence nil )"nat" monotone_subsequence nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil defined_types nil )nil epsilons nil )"(total_order?[real])" nil )nil monotone_subsequence nil ))nil ))nil 3507029426"" (skolem!) (("" (use "pick_prop" ) (("" (ground) nil nil )) nil ))nil )nil monotone_subsequence nil )"bool" monotone_subsequence nil )NOT const-decl "[bool -> bool]" booleans nil )nil sequences 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 )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3507029426"" (skolem!) (("" (use "pick_prop" ) (("" (flatten) nil nil )) nil ))nil )nil monotone_subsequence nil )"bool" monotone_subsequence nil )NOT const-decl "[bool -> bool]" booleans nil )nil sequences 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 )nil booleans nil )nil numbers nil ))nil ))nil 3507029426 ("" (skosimp) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3507029426 ("" (assert ) nil nil ) nil nil ))nil 3507029426"" (skolem!)"" (rewrite "strict_incr_condition" )"" (skolem!)"" (expand "g" 1 2) (("" (rewrite "pick_prop1" ) nil nil ))nil ))nil ))nil ))nil )nil sequence_props 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 )nil sequences nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" monotone_subsequence nil )"nat" monotone_subsequence nil )nil monotone_subsequence nil ))nil ))nil 3507029426"" (skolem!)"" (expand * "subseq" "gseq" )"" (inst + "g(w!1)" )"1" (assert ) nil nil ) ("2" (rewrite "g_increasing" ) nil nil ))nil ))nil ))nil )"sequence[real]" monotone_subsequence nil )"bool" sequence_props nil )nil monotone_subsequence nil )nil sequence_props 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" real_fun_preds "reals/" )nil sequences nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" monotone_subsequence nil )"nat" monotone_subsequence nil )"{u | NOT has_minimum(u, 0)}" nil ))nil ))nil 3507029426"" (skolem!)"" (rewrite "strict_decr_condition" )"" (skolem!)"" (expand "gseq" )"" (expand "g" 1 1) (("" (rewrite "pick_prop2" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil sequence_props 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 )nil sequences nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" monotone_subsequence nil )"sequence[real]" monotone_subsequence nil )nil monotone_subsequence nil )"nat" monotone_subsequence nil ))nil ))nil 3507029426"" (grind :if-match nil )"" (inst + "LAMBDA i : i+n!1" )"1" (assert ) nil nil )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil ))nil )"nonneg_int" nil )"nat" monotone_subsequence nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )nil sequence_props nil )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" sequence_props nil )"sequence[real]" monotone_subsequence nil ))nil ))nil 3507029426"" (grind :if-match nil )"1" (inst? +)"1" (assert )"1" (skosimp)"1" (inst - "j!1 - n!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (inst + "i!1 - n!1" )"2" (skosimp) (("2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"nonneg_int" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"nat" monotone_subsequence nil )"nat" monotone_subsequence nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" monotone_subsequence nil )"sequence[real]" monotone_subsequence nil ))nil ))nil 3507029426"" (skosimp)"" (auto-rewrite "strict_decr_to_decr[nat]" "gseq_decreasing" )"" (case "FORALL n : has_minimum(u!1, n)" )"1" (assert )"1" (inst + "hseq(u!1)" )"1" (ground)"1" (rewrite "hseq_extraction" ) nil nil )"2" (rewrite "hseq_increasing" ) nil nil ))nil ))nil ))nil )"2" (skolem!)"2" (rewrite "suffix_hasmin" :dir rl)"2" (assert )"2" (inst + "gseq(suffix(u!1, n!1))" )"2" (ground)"2" (use "gseq_extraction" )"2" (use "suffix_subseq" )"2" (forward-chain "transitive_subseq" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil monotone_subsequence nil )nil real_fun_props "reals/" )nil monotone_subsequence nil )nil sequence_props nil )nil monotone_subsequence nil )"sequence[real]" monotone_subsequence nil )"sequence[real]" monotone_subsequence nil )NOT const-decl "[bool -> bool]" booleans nil )nil monotone_subsequence nil )nil monotone_subsequence nil )nil monotone_subsequence nil )"sequence[real]" monotone_subsequence nil )"sequence[real]" monotone_subsequence 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 )nil sequences nil )"bool" monotone_subsequence nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.33 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
