Quelle real_facts.prf
Sprache: Lisp
(real_factsnil 3280072578"" (skosimp*)"" (prop)"1" (expand "bounded?" )"1" (flatten)"1" (expand "bounded_above?" )"1" (expand "bounded_below?" )"1" (skosimp*)"1" (expand "lower_bound?" )"1" (expand "upper_bound?" )"1" (inst + "max(abs(x!1),abs(x!2))" )"1" (skosimp*)"1" (inst - "x!3" )"1" (inst - "x!3" )"1" (expand "max" )"1" "1" "1" (grind) nil nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "bounded?" )"2" (prop)"1" (expand "bounded_above?" )"1" (expand "upper_bound?" )"1" (inst + "B!1" )"1" (skosimp*)"1" (inst?) (("1" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (expand "bounded_below?" )"2" (expand "lower_bound?" )"2" (inst + "-B!1" )"2" (skosimp*)"2" (inst - "s!1" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil real_types nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"bool" sets nil )set type-eq-decl nil sets nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil ))nil 3258973007"" (skolem!)"" (lemma "axiom_of_archimedes" ("x" "1/x!1" ))"" (skolem!)"" (assert )"" (inst 1 "i!1" )"" (rewrite "div_mult_pos_lt1" )"" (rewrite "div_mult_pos_lt1" )"" (assert ) nil ))))))))))))))nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"real" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3258973007"" (skosimp)"" (case "x!1 > 0" )"1" (lemma "archimedean2" ("x" "x!1" ))"1" (skolem!) (("1" (inst?) (("1" (assert ) nil )))))"2" (propax) nil )))"2" (assert ) nil ))))nil )nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil booleans 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 )"posrat" nil )"(strict_total_order?[real])" real_props nil )nil integers nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(strict_total_order?[real])" real_props nil )nil real_facts nil )nil real_types nil ))nil ))nil 3258973007"" (skolem!)"" (lemma "wf_nat" )"" (expand "well_founded?" )"" (inst -1 "lambda (b : nat) : x!1 < b" )"" (beta)"" (split)"1" (skolem!)"1" (typepred "y!1" )"1" (inst -2 "y!1 - 1" )"1" (assert ) nil )"2" (inst 2 "y!1 - 1" )"2" (assert ) nil )))))))))"2" (lemma "axiom_of_archimedes" ("x" "x!1" ))"2" (skolem!)"2" (inst?) (("2" (assert ) 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 naturalnumbers nil )nil defined_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )"int" real_facts nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"nonneg_real" real_facts nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(LAMBDA (b: nat): x!1 < b)" real_facts nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" orders nil ))nil ))nil 3258973007"" (skolem!)"" (case "x!1 >= 0" )"1" (lemma "nat_interval" ("x" "x!1" ))"1" (skosimp) (("1" (inst 1 "a!1" ) (("1" (assert ) nil )))))"2" (propax) nil )))"2" (lemma "nat_interval" ("x" "- x!1" ))"1" (skosimp)"1" (case "a!1 = -x!1" )"1" (inst 2 "- a!1" ) (("1" (assert ) nil )))"2" (inst 3 "-a!1 - 1" ) (("2" (assert ) nil )))))))"2" (assert ) nil ))))))nil )"bool" reals nil )nil booleans 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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil naturalnumbers nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )nil real_facts nil )nil real_types nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"[T, T -> boolean]" equalities nil )"real" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil ))nil ))nil 3258973007"" (skolem!)"" (typepred "lub(U!1)" ) (("" (grind) nil nil )) nil )) nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets 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 )"bool" bounded_real_defs nil )"(total_order?[real])" nil ))nil ))nil 3258973007"" (skolem!)"" (typepred "lub(U!1)" )"" (grind :if-match nil )"1" (inst? -3)"1" (inst? -2) (("1" (assert ) nil nil )) nil )) nil )"2" (inst? -2) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets 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 )"(total_order?[real])" nil )"bool" bounded_real_defs nil ))nil ))nil 3258973165"" (skosimp*)"" (prop)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" (inst -1 "a!1" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (expand "bounded_above?" )"2" (expand "upper_bound?" )"2" (inst 1 "b!1" )"2" (skosimp*) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" sets nil )"bool" sets nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil ))nil 3258974830"" (skosimp*)"" (typepred "lub({x | a!1 <= x AND x <= b!1})" )"1" (expand "least_upper_bound?" )"1" (flatten)"1" (expand "upper_bound?" )"1" (inst -1 "b!1" )"1" (inst -2 "b!1" ) (("1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (prop)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" (inst -1 "a!1" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (expand "bounded_above?" )"2" (inst + "b!1" )"2" (expand "upper_bound?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets 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 )"(total_order?[real])" nil )"real" real_facts nil )"real" real_facts nil )"(strict_total_order?[real])" real_props nil )"bool" bounded_real_defs nil )"bool" sets nil )"bool" sets nil ))nil 3258973007"" (skolem!)"" (use "lub_is_lub" ("y" "lub(U!1) - epsilon!1" ))"" (assert )"" (skolem!)"" (inst + "x!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"real" reals nil )nil real_facts nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3258973007"" (skolem!)"" (typepred "glb(V!1)" ) (("" (grind) nil nil )) nil )) nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets 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 )"bool" bounded_real_defs nil )"(total_order?[real])" nil ))nil ))nil 3258973007"" (skolem!)"" (typepred "glb(V!1)" )"" (grind :if-match nil )"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (inst? -2) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets 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 )"(total_order?[real])" nil )"bool" bounded_real_defs nil ))nil ))nil 3258974981 ("" (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 )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"(total_order?[real])" nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil ))nil 3258975012"" (skosimp*)"" (typepred "glb({x | a!1 <= x AND x <= b!1})" )"1" (expand "greatest_lower_bound?" )"1" (flatten)"1" (inst - "a!1" )"1" (expand "lower_bound?" )"1" (inst - "a!1" )"1" (grind) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets 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 )"bool" bounded_real_defs nil )"(strict_total_order?[real])" real_props nil )"real" real_facts nil )"real" real_facts nil )"(total_order?[real])" nil )"bool" sets nil )"bool" sets nil ))nil 3258973007"" (skolem!)"" (use "glb_is_glb" ("y" "glb(V!1) + epsilon!1" ))"" (assert )"" (skolem!)"" (inst + "x!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"real" reals nil )nil real_facts nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
