| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 5 kB |
|
Quelle commutative_ring_with_one.prf Sprache: Lisp |
|||||||||
|
(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.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28