(complex_fun_opsnil 3509263489"" (skosimp) (("" (expand "Re" 1 1) (("" (propax) nil nil )) nil ))nil )"[T -> real]" complex_fun_ops nil )) shostak))nil 3509263506"" (skosimp) (("" (expand "Im" 1 1) (("" (propax) nil nil )) nil ))nil )"[T -> real]" complex_fun_ops nil )) shostak))nil 3456290470"" (skosimp)"" (apply-extensionality :hide? t) (("" (grind) nil nil )) nil ))nil )nil complex_fun_ops nil )nil complex_types nil )"[T -> complex]" complex_fun_ops nil )"[T -> complex]" complex_fun_ops nil )"[T -> complex]" complex_fun_ops nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"complex" complex_types nil )"complex" complex_types nil )"complex" complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3456290487"" (skosimp)"" (apply-extensionality :hide? t) (("" (grind) nil nil )) nil ))nil )nil complex_fun_ops nil )nil complex_types nil )"[T -> complex]" complex_fun_ops nil )"[T -> complex]" complex_fun_ops nil )"[T -> complex]" complex_fun_ops nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil complex_types nil )"nonneg_real" sq "reals/" )"nnreal" complex_types nil )"complex" complex_types nil )"complex" complex_types nil )"complex" complex_types nil )"nzcomplex" complex_typesnil )"real" reals nil )"nnreal" nil )"posreal" complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3456290495"" (skosimp)"" (apply-extensionality :hide? t) (("" (grind) nil nil )) nil ))nil )nil complex_fun_ops nil )nil complex_types nil )"[S -> T]" const_fun_def "structures/" )"[T -> complex]" complex_fun_ops nil )"[T -> complex]" complex_fun_ops nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"complex" complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3456290504"" (skosimp)"" (apply-extensionality :hide? t) (("" (grind) nil nil )) nil ))nil )nil complex_fun_ops nil )nil complex_types nil )"[S -> T]" const_fun_def "structures/" )"[T -> complex]" complex_fun_ops nil )"[T -> complex]" complex_fun_ops nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil complex_types nil )"nonneg_real" sq "reals/" )"nnreal" complex_types nil )"complex" complex_types nil )"real" reals nil )"nnreal" nil )"posreal" complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3456290512"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "-" )"" (assert )"" (expand "-" )"" (assert )"" (decompose-equality)"1" (expand "Re" ) (("1" (assert ) nil nil )) nil )"2" (expand "Im" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil complex_fun_ops nil )nil complex_types nil )"[T -> complex]" complex_fun_ops nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"real" reals nil ))nil 3456290621"" (skosimp)"" (apply-extensionality :hide? t) (("" (grind) nil nil )) nil ))nil )nil complex_fun_ops nil )nil complex_types nil )"[T -> complex]" complex_fun_ops nil )"[T -> complex]" complex_fun_ops nil )"[T -> complex]" complex_fun_ops nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[T -> complex]" complex_fun_ops nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"[T -> complex]" complex_fun_ops nil )"posrat" nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"complex" complex_types nil )"complex" complex_types nil )"complex" complex_types nil )"complex" complex_types nil )"complex" complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3509263537"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "conjugate" )"" (expand "conjugate" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )"complex" complex_types nil )"real" reals nil )nil complex_types nil ))nil 3509263568"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "-" )"" (assert )"" (expand "conjugate" )"" (expand "conjugate" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )"real" reals nil )"complex" complex_types nil )nil complex_types nil ))nil 3509263212 ("" (subtype-tcc) nil nil )"real" complex_types nil )"[T -> real]" complex_fun_ops nil )"nonneg_real" sq "reals/" )nil complex_fun_ops nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"real" complex_types nil )"[T -> real]" complex_fun_ops nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil ))nil ))nil 3509263212"" (skolem + ("f!1" "x!1" ))"" (expand "sq_abs" )"" (expand "+ " )"" (expand "sq" )"" (assert )"" (typepred "f!1(x!1)" )"" (expand "/=" )"" (split)"1" (lemma "sq_nz_pos" ("nz" "Re(f!1(x!1))" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil )"2" (lemma "sq_nz_pos" ("nz" "Im(f!1(x!1))" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T -> nnreal]" complex_fun_ops nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil complex_types nil )"real" complex_types nil )nil complex_fun_ops nil )"real" complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil complex_types nil )"boolean" notequal nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil reals nil )nil sq "reals/" )nil complex_fun_ops nil )nil complex_fun_ops nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3509263212"" (skolem + ("f!1" "x!1" ))"" (expand "abs" )"" (expand "abs" )"" (lemma "nz_fun_sq_abs_pos" )"" (inst - "f!1" "x!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"[T -> nonneg_real]" complex_fun_ops nil )nil complex_fun_ops nil )"posreal" complex_types nil )"posreal" sqrt "reals/" )"[T -> posreal]" nil )"(strict_total_order?[real])" real_props nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil complex_types nil )nil complex_fun_ops nil )"nnreal" polar nil ))nil ))nil 3509263892"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "abs" )"" (expand "-" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil complex_fun_ops 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 )"bool" reals nil )nil real_types nil )"[T -> complex]" complex_fun_ops nil )"[T -> nonneg_real]" complex_fun_ops nil )nil complex_types nil )nil polar nil ))nil 3509263918"" (skosimp)"" (apply-extensionality :hide? t)"1" (expand "*" )"1" (expand "abs" ) (("1" (assert ) nil nil )) nil )) nil )"2" (skosimp)"2" (expand "*" )"2" (expand "abs" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil complex_fun_ops 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 )"bool" reals nil )nil real_types nil )"[T -> complex]" complex_fun_ops nil )"[T -> real]" real_fun_ops "reals/" )nil complex_types nil )"[T -> nonneg_real]" complex_fun_ops nil )"[T -> complex]" complex_fun_ops nil )"[T -> complex]" complex_fun_ops nil )"nnreal" nil )nil polar nil )"(total_order?[real])" nil ))nil 3509263965"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "+ " ) (("" (assert ) nil nil )) nil )) nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )nil complex_types nil )"real" reals nil ))nil 3509263983"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "-" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )nil complex_types nil )"real" reals nil ))nil 3509263996"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "-" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )nil complex_types nil )"real" reals nil ))nil 3509264010"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "*" ) (("" (expand "-" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" complex_fun_ops nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )"real" reals nil )"real" reals nil )nil complex_fun_ops nil )nil complex_types nil ))nil 3509264034"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "*" ) (("" (expand "-" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" complex_fun_ops nil )"real" complex_types nil )"real" complex_types nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )"real" reals nil )"real" reals nil )nil complex_fun_ops nil )nil complex_types nil ))nil 3509264053"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "/" )"" (expand "+ " )"" (expand "*" )"" (assert )"" (assert )"" (expand "sq_abs" )"" (expand "sq" 1 3)"" (expand "sq" 1 4)"" (expand "+" 1 4) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> nnreal]" complex_fun_ops nil )nil real_types nil )"bool" reals nil )"[T -> real]" complex_fun_ops nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil reals nil )"[T -> complex]" complex_fun_ops nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )"[T -> posreal]" nil )nil complex_fun_ops nil )"posreal" complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_fun_ops nil )"nnreal" complex_types nil )"nnreal" nil )"[T -> nnreal]" real_fun_ops_aux "reals/" ))nil 3509264266"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "/" )"" (expand "sq_abs" )"" (expand "sq" )"" (expand "+ " )"" (expand "*" )"" (assert )"" (expand "sq_abs" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> nnreal]" complex_fun_ops nil )nil real_types nil )"bool" reals nil )"[T -> real]" complex_fun_ops nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil reals nil )"[T -> complex]" complex_fun_ops nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )"[T -> posreal]" nil )nil complex_fun_ops nil )"nnreal" nil )"posreal" complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_fun_ops nil )"nnreal" complex_types nil )"[T -> nnreal]" real_fun_ops_aux "reals/" ))nil 3509264357"" (skosimp)"" (apply-extensionality :hide? t)"" expand "+ ") "" (expand "*" )"" (assert )"" (assert )"" (expand "/" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" complex_fun_ops nil )"nnreal" complex_types nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )"posreal" complex_types nil )"real" reals nil )nil complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )"real" reals nil )"real" reals nil ))nil 3509264435"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "+ " ) (("" (assert ) nil nil )) nil )) nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )nil complex_types nil )"real" reals nil ))nil 3509264449"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "-" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )nil complex_types nil )"real" reals nil ))nil 3509264474"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "-" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )nil complex_types nil )"real" reals nil ))nil 3509264606"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "+ " )"" (expand "*" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" complex_fun_ops nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )"real" reals nil )"real" reals nil )nil complex_fun_ops nil )nil complex_types nil ))nil 3509264632"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "*" )"" expand "+ ") "" (assert ) nil nil )) nil ))nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" complex_types nil )"[T -> real]" complex_fun_ops nil )"real" complex_types nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )"real" reals nil )"real" reals nil )nil complex_fun_ops nil )nil complex_types nil ))nil 3509264650"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "/" )"" (expand "-" )"" (expand "*" )"" (assert )"" (expand "sq_abs" )"" (assert )"" (expand "+" 1 2)"" (expand "sq" 1 3)"" (expand "sq" 1 3) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> nnreal]" complex_fun_ops nil )nil real_types nil )"bool" reals nil )"[T -> real]" complex_fun_ops nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil reals nil )"[T -> complex]" complex_fun_ops nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )"[T -> posreal]" nil )nil complex_fun_ops nil )"posreal" complex_types nil )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_fun_ops nil )"nnreal" nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"[T -> real]" real_fun_ops "reals/" )"nnreal" complex_types nil )"real" reals nil ))nil 3509264770"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "/" )"" (expand "sq_abs" )"" (expand "+ " )"" (expand "sq" )"" (expand "-" )"" (expand "*" )"" (assert )"" (expand "sq_abs" ) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> nnreal]" complex_fun_ops nil )nil real_types nil )"bool" reals nil )"[T -> real]" complex_fun_ops nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil reals nil )"[T -> complex]" complex_fun_ops nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )"[T -> posreal]" nil )nil complex_fun_ops nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"real" reals nil )"nnreal" complex_types nil )nil complex_fun_ops nil )nil complex_types nil )"real" reals nil )"real" reals nil )"posreal" complex_types nil )"nnreal" nil )"[T -> real]" real_fun_ops "reals/" ))nil 3509264846"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "/" )"" (expand "-" )"" (expand "*" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil complex_fun_ops nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T -> real]" complex_fun_ops nil )"nnreal" complex_types nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> complex]" complex_fun_ops nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"[T -> real]" complex_fun_ops nil )nil complex_types nil )"posreal" complex_types nil )"real" reals nil )nil complex_fun_ops nil )nil complex_types nil )nil complex_fun_ops nil )"real" reals nil )"real" reals nil ))nil 3509264900"" (skosimp) (("" (expand "=" 1 1) (("" (propax) nil nil )) nil ))nil )"bool" complex_fun_ops nil )) shostak))nil 3509264963"" (skosimp) (("" (expand "/=" ) (("" (propax) nil nil )) nil )) nil )"bool" complex_fun_ops nil )) shostak)))quality 100%
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
