|
(sqrt_rew
(sqrt_4 0
(sqrt_4-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
((sqrt_4 formula-decl nil sqrt nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq nil)
(nnreal type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(sqrt_9 0
(sqrt_9-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
((sqrt_9 formula-decl nil sqrt nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq nil)
(nnreal type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(sqrt_16 0
(sqrt_16-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
((sqrt_16 formula-decl nil sqrt nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq nil)
(nnreal type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(sqrt_25 0
(sqrt_25-1 nil 3254823310 ("" (both-sides-f 1 "sq") nil nil)
((sqrt_25 formula-decl nil sqrt nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq nil)
(nnreal type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(sqrt_36 0
(sqrt_36-1 nil 3254823310
("" (both-sides-f 1 "sq")
(("1" (assert) (("1" (grind) nil nil)) nil)
("2" (rewrite "sq_eq") nil nil))
nil)
((sq_eq formula-decl nil sq nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_sqrt formula-decl nil sqrt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sq_nz_pos application-judgement "posreal" sq nil))
nil))
(sqrt_49 0
(sqrt_49-2 nil 3563712260
("" (both-sides-f 1 "sq")
(("1" (assert) (("1" (grind) nil))) ("2" (rewrite "sq_eq") nil))
nil)
((sq_eq formula-decl nil sq nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_sqrt formula-decl nil sqrt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sq_nz_pos application-judgement "posreal" sq nil))
nil)
(sqrt_49-1 nil 3254823310
("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(sq const-decl "nonneg_real" sq nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
nil))
(sqrt_64 0
(sqrt_64-2 nil 3563712264
("" (both-sides-f 1 "sq")
(("1" (assert) (("1" (grind) nil))) ("2" (rewrite "sq_eq") nil))
nil)
((sq_eq formula-decl nil sq nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_sqrt formula-decl nil sqrt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sq_nz_pos application-judgement "posreal" sq nil))
nil)
(sqrt_64-1 nil 3254823310
("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(sq const-decl "nonneg_real" sq nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
nil))
(sqrt_81 0
(sqrt_81-2 nil 3563712269
("" (both-sides-f 1 "sq")
(("1" (assert) (("1" (grind) nil))) ("2" (rewrite "sq_eq") nil))
nil)
((sq_eq formula-decl nil sq nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_sqrt formula-decl nil sqrt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sq_nz_pos application-judgement "posreal" sq nil))
nil)
(sqrt_81-1 nil 3254823310
("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(sq const-decl "nonneg_real" sq nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
nil))
(sqrt_100 0
(sqrt_100-2 nil 3563712274
("" (both-sides-f 1 "sq")
(("1" (assert) (("1" (grind) nil nil)) nil)
("2" (rewrite "sq_eq") nil nil))
nil)
((sq_eq formula-decl nil sq nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_sqrt formula-decl nil sqrt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal type-eq-decl nil real_types nil)
(sq const-decl "nonneg_real" sq nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sq_nz_pos application-judgement "posreal" sq nil))
nil)
(sqrt_100-1 nil 3254823310
("" (both-sides-f 1 "sq") (("" (rewrite "sq_eq") nil nil)) nil)
((sq_eq formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
(sqrt_pos application-judgement "posreal" sqrt nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(sq const-decl "nonneg_real" sq nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil))
nil))
(sqrt_factor_left 0
(sqrt_factor_left-1 nil 3254823327
("" (skosimp*)
(("" (case-replace "nna!1 * nnx!1 * nnx!1 = nnx!1 * nnx!1*nna!1")
(("1" (rewrite "sqrt_times") (("1" (assert) nil nil)) nil)
("2" (hide 2) (("2" (assert) nil nil)) nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqrt_square formula-decl nil sqrt nil)
(sqrt_times formula-decl nil sqrt nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
shostak))
(sqrt_factor_middle 0
(sqrt_factor_middle-1 nil 3254823495
("" (skosimp*)
(("" (case-replace "nnx!1 * nna!1 * nnx!1 = nnx!1 * nnx!1*nna!1")
(("1" (rewrite "sqrt_times") (("1" (assert) nil nil)) nil)
("2" (hide 2) (("2" (assert) nil nil)) nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqrt_square formula-decl nil sqrt nil)
(sqrt_times formula-decl nil sqrt nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
nil))
(sqrt_factor_right 0
(sqrt_factor_right-1 nil 3254823514
("" (skosimp*)
(("" (case-replace "nnx!1 * nnx!1 * nna!1 = nnx!1 * nnx!1*nna!1")
(("" (rewrite "sqrt_times") (("" (assert) nil nil)) nil)) nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(sqrt_square formula-decl nil sqrt nil)
(sqrt_times formula-decl nil sqrt nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
nil)))
[ Dauer der Verarbeitung: 0.5 Sekunden
(vorverarbeitet)
]
|
