|
(commutative_ring_with_one
(fullset_is_commutative_ring_with_one 0
(fullset_is_commutative_ring_with_one-1 nil 3292785972
("" (expand "commutative_ring_with_one?")
(("" (lemma "star_commutative")
(("" (lemma "fullset_is_ring_with_one") (("" (assert) nil nil))
nil))
nil))
nil)
((fullset_is_ring_with_one formula-decl nil ring_with_one nil))
shostak))
(IMP_ring_with_one_TCC1 0
(IMP_ring_with_one_TCC1-1 nil 3292786148
("" (lemma "fullset_is_commutative_ring_with_one")
(("" (expand "commutative_ring_with_one?") (("" (flatten) nil nil))
nil))
nil)
((commutative_ring_with_one? const-decl "bool" ring_with_one_def
nil)
(fullset_is_commutative_ring_with_one formula-decl nil
commutative_ring_with_one nil))
shostak))
(IMP_commutative_ring_TCC1 0
(IMP_commutative_ring_TCC1-1 nil 3292786148
("" (lemma "fullset_is_commutative_ring_with_one")
(("" (expand "commutative_ring_with_one?")
(("" (expand "commutative_ring?")
(("" (expand "ring_with_one?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((commutative_ring_with_one? const-decl "bool" ring_with_one_def
nil)
(ring_with_one? const-decl "bool" ring_with_one_def nil)
(commutative_ring? const-decl "bool" ring_def nil)
(fullset_is_commutative_ring_with_one formula-decl nil
commutative_ring_with_one nil))
shostak))
(commutative_ring_with_one_TCC1 0
(commutative_ring_with_one_TCC1-1 nil 3292786148
("" (lemma "fullset_is_commutative_ring_with_one")
(("" (propax) nil nil)) nil)
((fullset_is_commutative_ring_with_one formula-decl nil
commutative_ring_with_one nil))
shostak))
(commutative_ring_with_one_is 0
(commutative_ring_with_one_is-1 nil 3292786031
("" (skolem!) (("" (typepred "R!1") (("" (propax) nil nil)) nil))
nil)
((commutative_ring_with_one nonempty-type-eq-decl nil
commutative_ring_with_one nil)
(commutative_ring_with_one? const-decl "bool" ring_with_one_def
nil)
(one formal-const-decl "T" commutative_ring_with_one nil)
(zero formal-const-decl "T" commutative_ring_with_one nil)
(* formal-const-decl "[T, T -> T]" commutative_ring_with_one nil)
(+ formal-const-decl "[T, T -> T]" commutative_ring_with_one nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil commutative_ring_with_one nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(commutative_ring_with_one_is_commutative_ring 0
(commutative_ring_with_one_is_commutative_ring-1 nil 3292786051
("" (skosimp*)
(("" (typepred "x!1")
(("" (expand "commutative_ring_with_one?")
(("" (expand "commutative_ring?")
(("" (expand "ring_with_one?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((commutative_ring_with_one nonempty-type-eq-decl nil
commutative_ring_with_one nil)
(commutative_ring_with_one? const-decl "bool" ring_with_one_def
nil)
(one formal-const-decl "T" commutative_ring_with_one nil)
(zero formal-const-decl "T" commutative_ring_with_one nil)
(* formal-const-decl "[T, T -> T]" commutative_ring_with_one nil)
(+ formal-const-decl "[T, T -> T]" commutative_ring_with_one nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil commutative_ring_with_one nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(commutative_ring? const-decl "bool" ring_def nil)
(ring_with_one? const-decl "bool" ring_with_one_def nil))
shostak))
(commutative_ring_with_one_is_ring_with_one 0
(commutative_ring_with_one_is_ring_with_one-1 nil 3292786121
("" (skosimp*)
(("" (typepred "x!1")
(("" (expand "commutative_ring_with_one?")
(("" (flatten) nil nil)) nil))
nil))
nil)
((commutative_ring_with_one nonempty-type-eq-decl nil
commutative_ring_with_one nil)
(commutative_ring_with_one? const-decl "bool" ring_with_one_def
nil)
(one formal-const-decl "T" commutative_ring_with_one nil)
(zero formal-const-decl "T" commutative_ring_with_one nil)
(* formal-const-decl "[T, T -> T]" commutative_ring_with_one nil)
(+ formal-const-decl "[T, T -> T]" commutative_ring_with_one nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil commutative_ring_with_one nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(commutative_ring_with_one_is_commutative_monoid 0
(commutative_ring_with_one_is_commutative_monoid-1 nil 3294094805
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "commutative_ring_with_one?")
(("" (expand "commutative_monoid?")
(("" (expand "ring_with_one?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((commutative_ring_with_one nonempty-type-eq-decl nil
commutative_ring_with_one nil)
(commutative_ring_with_one? const-decl "bool" ring_with_one_def
nil)
(one formal-const-decl "T" commutative_ring_with_one nil)
(zero formal-const-decl "T" commutative_ring_with_one nil)
(* formal-const-decl "[T, T -> T]" commutative_ring_with_one nil)
(+ formal-const-decl "[T, T -> T]" commutative_ring_with_one nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil commutative_ring_with_one nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(commutative_monoid? const-decl "bool" monoid_def nil)
(ring_with_one? const-decl "bool" ring_with_one_def nil))
shostak)))
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
