|
(number_fields_sq
(sq_nz_pos 0
(sq_nz_pos-1 nil 3280147667
("" (expand "sq")
(("" (skosimp*)
((""
(lemma "nznum_times_nznum_is_nznum"
("nzx" "nz!1" "nzy" "nz!1"))
(("" (assert) nil nil)) nil))
nil))
nil)
((nznum_times_nznum_is_nznum application-judgement "nznum"
number_fields_bis nil)
(nznum_times_nznum_is_nznum judgement-tcc nil number_fields_bis
nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(sq const-decl "numfield" number_fields_sq nil))
shostak))
(sq_rew 0
(sq_rew-1 nil 3280147747
("" (expand "sq") (("" (propax) nil nil)) nil)
((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_neg 0
(sq_neg-1 nil 3280147757
("" (expand "sq")
(("" (skosimp*) (("" (rewrite "neg_times_neg") nil nil)) nil)) nil)
((numfield nonempty-type-eq-decl nil number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(neg_times_neg formula-decl nil number_fields_bis nil)
(sq const-decl "numfield" number_fields_sq nil))
shostak))
(sq_times 0
(sq_times-1 nil 3280147791
("" (expand "sq") (("" (propax) nil nil)) nil)
((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_plus 0
(sq_plus-1 nil 3280147801
("" (expand "sq") (("" (grind) nil nil)) nil)
((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_minus 0
(sq_minus-1 nil 3280147819 ("" (grind) nil nil)
((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_neg_minus 0
(sq_neg_minus-1 nil 3280147827
("" (expand "sq") (("" (propax) nil nil)) nil)
((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_0 0
(sq_0-1 nil 3280147836 ("" (expand "sq") (("" (propax) nil nil)) nil)
((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_1 0
(sq_1-1 nil 3280147845 ("" (expand "sq") (("" (propax) nil nil)) nil)
((sq const-decl "numfield" number_fields_sq nil)) shostak))
(sq_eq_0 0
(sq_eq_0-1 nil 3280147908
("" (skosimp*)
(("" (expand "sq")
(("" (split)
(("1" (flatten)
(("1" (lemma "zero_times3" ("x" "a!1" "y" "a!1"))
(("1" (assert) nil nil)) nil))
nil)
("2" (flatten)
(("2" (assert)
(("2" (replace -1) (("2" (rewrite "zero_times1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sq const-decl "numfield" number_fields_sq nil)
(zero_times1 formula-decl nil number_fields_bis nil)
(zero_times3 formula-decl nil number_fields_bis nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil))
shostak))
(sq_div 0
(sq_div-1 nil 3280147989
("" (expand "sq")
(("" (skosimp*) (("" (rewrite "div_times") nil nil)) nil)) nil)
((numfield nonempty-type-eq-decl nil number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(div_times formula-decl nil number_fields_bis nil)
(sq const-decl "numfield" number_fields_sq nil))
shostak)))
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
