(sequence_propsnil 3406888867"" (skolem!)"" (expand "increasing?" )"" (prop)"1" (skolem!) (("1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" (induct "y" )"1" (skosimp) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst -1 "x!1" )"2" (inst -3 "j!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds "reals/" )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sequences nil )nil naturalnumbers nil )"posint" nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"posint" nil ))nil ))nil 3406888867"" (skolem!)"" (expand "decreasing?" )"" (prop)"1" (skolem!) (("1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" (induct "y" )"1" (skosimp) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst -1 "x!1" )"2" (inst -3 "j!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds "reals/" )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sequences nil )nil naturalnumbers nil )"posint" nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"posint" nil ))nil ))nil 3406888867"" (skolem!)"" (expand "strict_increasing?" )"" (prop)"1" (skolem!) (("1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" (induct "y" )"1" (skosimp) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst -1 "x!1" )"2" (inst -3 "j!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds "reals/" )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sequences nil )nil naturalnumbers nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"posint" nil ))nil ))nil 3406888867"" (skolem!)"" (expand "strict_decreasing?" )"" (prop)"1" (skolem!) (("1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" (induct "y" )"1" (skosimp) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (inst -1 "x!1" )"2" (inst -3 "j!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds "reals/" )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sequences nil )nil naturalnumbers nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"posint" nil ))nil ))nil 3406888867"" (grind :if-match nil )"1" (inst -1 "j!1" "i!1" ) (("1" (assert ) nil nil )) nil )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil )"(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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" real_fun_preds "reals/" )nil sequence_props nil ))nil ))nil 3406888867"" (skosimp)"" (use "extract_incr1" ("i" "j!1" "j" "i!1" ))"" (assert ) 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 sequence_props nil )"bool" real_fun_preds "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3406888867"" (skolem 1 ("f!1" _))"" (induct "i" )"1" (assert ) nil nil )"2" (skosimp)"2" (use "extract_incr1" ("i" "j!1" "j" "j!1+1" ))"2" (assert ) 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" reals nil )"bool" real_fun_preds "reals/" )nil sequence_props nil )nil naturalnumbers nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sequence_props nil )"posint" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3406888867"" (skolem!)"" (inst?) (("" (rewrite "extract_incr3" ) 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 sequence_props nil )"bool" real_fun_preds "reals/" )nil sequence_props nil ))nil ))nil 3406888867"" (skosimp)"" (use "unbounded_extract1" ("f" "f!1" ))"" (skolem!)"" (inst 1 "j!1+1" )"" (use "extract_incr1" ("i" "j!1" "j" "j!1+1" ))"" (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 )"bool" real_fun_preds "reals/" )nil sequence_props nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )nil sequence_props nil ))nil ))nil 3406888867"" (auto-rewrite "strict_increasing?" "o" ) (("" (grind) nil nil ))nil )"bool" real_fun_preds "reals/" )"T3" function_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sequence_props nil )nil naturalnumbers 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 )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3406888900"" (skosimp*) (("" (expand "subseq" ) (("" (propax) nil nil )) nil ))nil )"bool" sequence_props nil )) shostak))nil 3406888867"" (skolem!)"" (expand "subseq" )"" (inst 1 "I" )"1" (expand "I" ) (("1" (propax) nil nil )) nil )"2" (grind) nil nil ))nil ))nil ))nil )"bool" sequence_props nil )NOT const-decl "[bool -> bool]" booleans 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/" )"bool" functions nil )"(bijective?[T, T])" identity nil ))nil ))nil 3406888867"" (expand "subseq" )"" (skosimp*)"" (inst 1 "f!2 o f!1" )"1" (grind) nil nil )"2" (rewrite "extract_composition" ) nil nil ))nil ))nil ))nil )nil sequence_props nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans 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/" )"T3" function_props nil )nil sequence_props nil )"extraction" sequence_props nil )"extraction" sequence_props nil )"bool" sequence_props nil ))nil ))nil 3406889120 ("" (subtype-tcc) nil 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" real_fun_preds "reals/" )nil sequence_props nil )set type-eq-decl nil sets nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"set[R]" function_image nil )"set" sets nil ))nil ))nil 3406889143"" (skosimp)"" (expand "bijective?" )"" (typepred "f!1" )"" (expand "strict_increasing?" )"" (split)"1" (expand "injective?" )"1" (skosimp)"1" (lemma "trich_lt" ("x" "x1!1" "y" "x2!1" ))"1" (split -1)"1" (inst - "x1!1" "x2!1" )"1" (assert ) nil nil )) nil )"2" (propax) nil nil )"3" (inst - "x2!1" "x1!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp*)"2" (typepred "y!1" )"2" (expand "fullset" )"2" (expand "image" )"2" (skosimp)"2" (inst + "x!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" functions nil )"bool" functions nil )"set" sets nil )"set[R]" function_image nil )set type-eq-decl nil sets nil )"bool" booleans nil )"bool" functions nil )nil real_props nil )"(strict_total_order?[real])" real_props 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" real_fun_preds "reals/" )nil sequence_props nil ))nil ))nil 3406888867"" (grind :if-match nil )"" (inst-cp -5 "x!1" )"" (inst -5 "y!1" )"" (replace *)"" (inst? -4)"" (assert )"" (inst -3 "x!1" "y!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" real_fun_preds "reals/" )nil sequence_props nil )"bool" sequence_props nil )"bool" real_fun_preds "reals/" ))nil ))nil 3406888867"" (grind :if-match nil )"" (inst-cp -5 "x!1" )"" (inst -5 "y!1" )"" (inst -3 "x!1" "y!1" )"" (inst -4 "f!1(x!1)" "f!1(y!1)" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" real_fun_preds "reals/" )nil sequence_props nil )"bool" sequence_props nil )"bool" real_fun_preds "reals/" ))nil ))nil 3406888867"" (grind :if-match nil )"" (inst-cp -5 "x!1" )"" (inst -5 "y!1" )"" (inst -3 "x!1" "y!1" )"" (inst -4 "f!1(x!1)" "f!1(y!1)" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"(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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil sequence_props nil )"bool" sequence_props nil )"bool" real_fun_preds "reals/" ))nil ))nil 3406888867"" (grind :if-match nil )"" (inst-cp -5 "x!1" )"" (inst -5 "y!1" )"" (inst -3 "x!1" "y!1" )"" (inst -4 "f!1(x!1)" "f!1(y!1)" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"(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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil sequence_props nil )"bool" sequence_props nil )"bool" real_fun_preds "reals/" ))nil ))nil 3406888867"" (grind :if-match nil )"" (inst? +)"" (skolem!)"" (inst? -4) (("" (inst? -3) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" real_fun_preds "reals/" )nil sequence_props 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" sequence_props nil )"bool" real_fun_preds "reals/" ))nil ))nil 3406888867"" (grind :if-match nil )"" (inst? +)"" (skolem!)"" (inst? -4) (("" (inst? -3) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" real_fun_preds "reals/" )nil sequence_props 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" sequence_props nil )"bool" real_fun_preds "reals/" ))nil ))nil 3406888867"" (expand "bounded?" )"" (skosimp)"" (forward-chain "bounded_above_subseq" )"" (forward-chain "bounded_below_subseq" )"" (assert ) nil nil )) nil ))nil ))nil ))nil )nil sequence_props 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 sequence_props nil )"bool" real_fun_preds "reals/" ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
