(integral_domainnil 3292787563"" (expand "integral_domain?" )"" (lemma "fullset_is_commutative_ring" )"" (lemma "no_zero_divisors" )"" (replace -2)"" (expand "no_zero_divisors?" )"" (skosimp*)"" (inst - "x!1" "y!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil commutative_ringnil ))nil 3292787346"" (lemma "fullset_is_integral_domain" )"" (expand "integral_domain?" ) (("" (flatten) nil nil )) nil ))nil )"bool" integral_domain_def nil )nil integral_domain nil ))nil 3292787453"" (lemma "fullset_is_integral_domain" ) (("" (propax) nil nil ))nil )nil integral_domain nil ))nil 3292787653"" (skolem!) (("" (typepred "I!1" ) (("" (propax) nil nil )) nil ))nil )nil integral_domain nil )"bool" integral_domain_def nil )"T" integral_domain nil )"[T, T -> T]" integral_domain nil )"[T, T -> T]" integral_domain nil )set type-eq-decl nil sets nil )nil integral_domain nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3292787671"" (skosimp*)"" (typepred "x!1" )"" (expand "integral_domain?" ) (("" (flatten) nil nil )) nil ))nil ))nil )nil integral_domain nil )"bool" integral_domain_def nil )"T" integral_domain nil )"[T, T -> T]" integral_domain nil )"[T, T -> T]" integral_domain nil )set type-eq-decl nil sets nil )nil integral_domain nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))quality 100%
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
