(commutative_ringnil 3293981068"" (lemma "fullset_is_commutative_ring" )"" (expand "commutative_ring?" ) (("" (flatten) nil nil )) nil ))nil )"bool" ring_def nil )nil commutative_ringnil ))nil 3293981068"" (lemma "fullset_is_commutative_ring" ) (("" (propax) nil nil ))nil )nil commutative_ringnil ))nil 3293981087"" (lemma "fullset_is_commutative_ring" )"" (expand "commutative_ring?" )"" (flatten)"" (expand "commutative?" )"" (expand "restrict" )"" (skosimp)"" (inst - "x!1" "y!1" )"1" (expand "fullset" ) (("1" (propax) nil nil )) nil )"2" (expand "fullset" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" ring_def nil )"bool" operator_defs nil )"T" commutative_ring nil )"T" commutative_ring nil )"set" sets nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil commutative_ring nil )"R" restrict nil )nil commutative_ringnil ))nil 3293981068"" (skosimp)"" (typepred "x!1" )"" (expand "commutative_ring?" ) (("" (flatten) nil nil )) nil ))nil ))nil )nil commutative_ring nil )"bool" ring_def nil )"T" commutative_ring nil )"[T, T -> T]" commutative_ring nil )"[T, T -> T]" commutative_ring nil )set type-eq-decl nil sets nil )nil commutative_ring nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3294090987"" (skosimp)"" (typepred "R!1" )"" (expand "subring?" )"" (expand "commutative_ring?" )"" (flatten)"" (assert )"" (expand "commutative?" )"" (expand "restrict" )"" (expand "subset?" )"" (expand "member" )"" (skosimp)"" (inst-cp - "x!1" )"" (inst - "y!1" )"" (assert )"" (inst - "x!1" "y!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil commutative_ring nil )"bool" ring_def nil )"T" commutative_ring nil )"[T, T -> T]" commutative_ring nil )"[T, T -> T]" commutative_ring nil )set type-eq-decl nil sets nil )nil commutative_ring nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(partial_order?[set[T]])" nil )"R" restrict nil )"bool" sets nil )"bool" sets nil )"bool" operator_defs nil )"bool" ring_def nil ))nil 3297002583"" (skosimp)"" (expand "sq" )"" (lemma "times_associative" )"" (rewrite "times_associative" )"" (rewrite "times_associative" )"" (inst-cp - "y!1" "x!1" "y!1" )"" (inst - "x!1" "y!1" "y!1" )"" (lemma "times_commutative" ("x" "x!1" "y" "y!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" ring nil )nil commutative_ring nil )nil ring nil )nil commutative_ring nil )"[T, T -> T]" commutative_ring nil )"[T, T -> T]" commutative_ring nil )"T" commutative_ring nil ))quality 100%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
