|
(ring_nz_closed
(IMP_ring_TCC1 0
(IMP_ring_TCC1-1 nil 3293963187
("" (lemma "fullset_is_ring_nz_closed")
(("" (expand "ring_nz_closed?") (("" (flatten) nil nil)) nil)) nil)
((ring_nz_closed? const-decl "bool" ring_nz_closed_def nil)
(fullset_is_ring_nz_closed formula-decl nil ring_nz_closed nil))
shostak))
(ring_nz_closed_TCC1 0
(ring_nz_closed_TCC1-1 nil 3293963187
("" (lemma "fullset_is_ring_nz_closed") (("" (propax) nil nil)) nil)
((fullset_is_ring_nz_closed formula-decl nil ring_nz_closed nil))
shostak))
(ring_nz_closed_is 0
(ring_nz_closed_is-1 nil 3293963211
("" (skolem!) (("" (typepred "R!1") (("" (propax) nil nil)) nil))
nil)
((ring_nz_closed nonempty-type-eq-decl nil ring_nz_closed nil)
(ring_nz_closed? const-decl "bool" ring_nz_closed_def nil)
(zero formal-const-decl "T" ring_nz_closed nil)
(* formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(+ formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil ring_nz_closed nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(ring_nz_closed_is_ring 0
(ring_nz_closed_is_ring-1 nil 3293963187
("" (skolem!)
(("" (typepred "x!1")
(("" (expand "ring_nz_closed?") (("" (flatten) nil nil)) nil))
nil))
nil)
((ring_nz_closed nonempty-type-eq-decl nil ring_nz_closed nil)
(ring_nz_closed? const-decl "bool" ring_nz_closed_def nil)
(zero formal-const-decl "T" ring_nz_closed nil)
(* formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(+ formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil ring_nz_closed nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(nz_T_times_nz_T_is_nz_T 0
(nz_T_times_nz_T_is_nz_T-1 nil 3293964256
("" (skosimp*)
(("" (typepred "nzx!1")
(("" (typepred "nzy!1")
(("" (skosimp*)
(("" (lemma "fullset_is_ring_nz_closed")
(("" (expand "ring_nz_closed?")
(("" (flatten)
(("" (expand "nz_closed?")
(("" (hide -1)
(("" (expand "star_closed?")
(("" (inst - "nzx!1" "nzy!1")
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nz_T type-eq-decl nil ring_nz_closed_def nil)
(* formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(+ formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(zero formal-const-decl "T" ring_nz_closed nil)
(/= const-decl "boolean" notequal nil)
(T formal-nonempty-type-decl nil ring_nz_closed nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(ring_nz_closed? const-decl "bool" ring_nz_closed_def nil)
(nz_closed? const-decl "bool" ring_nz_closed_def nil)
(star_closed? const-decl "bool" groupoid_def nil)
(member const-decl "bool" sets nil)
(nzy!1 skolem-const-decl "nz_T[T, +, *, zero]" ring_nz_closed nil)
(nzx!1 skolem-const-decl "nz_T[T, +, *, zero]" ring_nz_closed nil)
(fullset const-decl "set" sets nil)
(remove const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(fullset_is_ring_nz_closed formula-decl nil ring_nz_closed nil))
shostak))
(negate_nz_T_is_nz_T 0
(negate_nz_T_is_nz_T-1 nil 3293964256
("" (skosimp 1)
(("" (lemma "negate_negate" ("x" "nzx!1"))
(("" (replace -2)
(("" (rewrite "negate_zero")
(("" (typepred "nzx!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((zero formal-const-decl "T" ring_nz_closed nil)
(* formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(+ formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(T formal-nonempty-type-decl nil ring_nz_closed nil)
(nz_T type-eq-decl nil ring_nz_closed_def nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(negate_negate formula-decl nil ring nil)
(negate_zero formula-decl nil ring nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(times_is_zero 0
(times_is_zero-1 nil 3293966061
("" (skolem!)
(("" (prop)
(("1" (lemma "nz_T_times_nz_T_is_nz_T" ("nzx" "x!1" "nzy" "y!1"))
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (assert) nil nil))
nil)
("2" (replace -1) (("2" (rewrite "zero_times") nil nil)) nil)
("3" (replace -1) (("3" (rewrite "times_zero") nil nil)) nil))
nil))
nil)
((nz_T_times_nz_T_is_nz_T judgement-tcc nil ring_nz_closed nil)
(T formal-nonempty-type-decl nil ring_nz_closed nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero formal-const-decl "T" ring_nz_closed nil)
(+ formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(* formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(nz_T type-eq-decl nil ring_nz_closed_def nil)
(zero_times formula-decl nil ring nil)
(times_zero formula-decl nil ring nil))
shostak))
(nz_T_times 0
(nz_T_times-1 nil 3293967447
("" (skosimp)
(("" (typepred "nzx!1")
(("" (skosimp)
(("" (lemma "times_is_zero" ("x" "nzx!1" "y" "y!1"))
(("" (grind) nil nil)) nil))
nil))
nil))
nil)
((nz_T type-eq-decl nil ring_nz_closed_def nil)
(* formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(+ formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(zero formal-const-decl "T" ring_nz_closed nil)
(/= const-decl "boolean" notequal nil)
(T formal-nonempty-type-decl nil ring_nz_closed nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(times_is_zero formula-decl nil ring_nz_closed nil))
shostak))
(times_nz_T 0
(times_nz_T-1 nil 3293967527
("" (skosimp)
(("" (lemma "times_is_zero" ("x" "x!1" "y" "nzy!1"))
(("" (typepred "nzy!1") (("" (grind) nil nil)) nil)) nil))
nil)
((nz_T type-eq-decl nil ring_nz_closed_def nil)
(* formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(+ formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(zero formal-const-decl "T" ring_nz_closed nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ring_nz_closed nil)
(times_is_zero formula-decl nil ring_nz_closed nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(nz_T_times_nz_T_is_not_zero 0
(nz_T_times_nz_T_is_not_zero-1 nil 3293967555
("" (skosimp)
((""
(lemma "nz_T_times_nz_T_is_nz_T" ("nzx" "nzx!1" "nzy" "nzy!1"))
(("" (assert) nil nil)) nil))
nil)
((nz_T type-eq-decl nil ring_nz_closed_def nil)
(* formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(+ formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(zero formal-const-decl "T" ring_nz_closed nil)
(/= const-decl "boolean" notequal nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ring_nz_closed nil)
(nz_T_times_nz_T_is_nz_T judgement-tcc nil ring_nz_closed nil)
(nz_T_times_nz_T_is_nz_T application-judgement "nz_T"
ring_nz_closed nil))
shostak))
(sq_nz_is_nz 0
(sq_nz_is_nz-1 nil 3297003228
("" (expand "sq")
(("" (skosimp)
((""
(lemma "nz_T_times_nz_T_is_not_zero"
("nzx" "nzx!1" "nzy" "nzx!1"))
(("" (assert) nil nil)) nil))
nil))
nil)
((nz_T_times_nz_T_is_nz_T application-judgement "nz_T"
ring_nz_closed nil)
(nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil)
(T formal-nonempty-type-decl nil ring_nz_closed nil)
(boolean nonempty-type-decl nil booleans nil)
(/= const-decl "boolean" notequal nil)
(zero formal-const-decl "T" ring_nz_closed nil)
(+ formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(* formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(nz_T type-eq-decl nil ring_nz_closed_def nil)
(sq const-decl "T" ring nil))
shostak))
(sq_eq_zero 0
(sq_eq_zero-1 nil 3297003276
("" (skosimp)
(("" (expand "sq")
(("" (prop)
(("1" (lemma "times_is_zero" ("x" "x!1" "y" "x!1"))
(("1" (assert) nil nil)) nil)
("2" (replace -1) (("2" (rewrite "zero_times") nil nil)) nil))
nil))
nil))
nil)
((sq const-decl "T" ring nil)
(zero formal-const-decl "T" ring_nz_closed nil)
(* formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(+ formal-const-decl "[T, T -> T]" ring_nz_closed nil)
(zero_times formula-decl nil ring nil)
(T formal-nonempty-type-decl nil ring_nz_closed nil)
(times_is_zero formula-decl nil ring_nz_closed nil))
shostak)))
¤ Dauer der Verarbeitung: 0.1 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.
|
