(ring_with_onenil 3293390922"" (lemma "fullset_is_ring_with_one" )"" (expand "ring_with_one?" )"" (flatten)"" (expand "ring?" ) (("" (postpone) nil nil )) nil )) nil ))nil ))nil )"bool" ring_with_one_def nil )nil ring_with_one nil ))nil 3293390922"" (lemma "fullset_is_ring_with_one" )"" (expand "ring_with_one?" ) (("" (flatten) nil nil )) nil )) nil )"bool" ring_with_one_def nil )nil ring_with_one nil ))nil 3293390922"" (lemma "fullset_is_ring_with_one" ) (("" (propax) nil nil )) nil )nil ring_with_one nil ))nil 3293907997"" (lemma "left_identity[T,*,one]" ) (("" (propax) nil nil )) nil )nil monad nil )nil ring_with_one nil )"[T, T -> T]" ring_with_one nil )"T" ring_with_one nil ))nil 3293908022"" (lemma "right_identity[T,*,one]" ) (("" (propax) nil nil )) nil )nil monad nil )nil ring_with_one nil )"[T, T -> T]" ring_with_one nil )"T" ring_with_one nil ))nil 3293908031"" (skosimp)"" "unique_left_identity[T,*,one]" "y" "y!1" "M" "fullset[T]" ))"1" (prop)"1" (skosimp)"1" (inst - "x!1" ) (("1" (grind) nil nil )) nil )) nil )"2" (skosimp) (("2" (inst - "x!1" ) nil nil )) nil ))nil )"2" (hide 2)"2" (lemma "fullset_is_ring_with_one" )"2" (expand "ring_with_one?" )"2" (expand "monoid?" ) (("2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"T" ring_with_one nil )"[T, T -> T]" ring_with_one nil )nil ring_with_one nil )"set" sets nil )nil monad nil )"bool" monad_def nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil monad nil )"T" ring_with_one nil )nil ring_with_one nil )"bool" monoid_def nil )"bool" ring_with_one_def nil ))nil 3293908156"" (skosimp)"" "unique_right_identity[T,*,one]" "M" "fullset[T]" "y" "y!1" ))"1" (prop)"1" (skosimp)"1" (inst - "x!1" ) (("1" (grind) nil nil )) nil )) nil )"2" (skosimp) (("2" (inst - "x!1" ) nil nil )) nil ))nil )"2" (lemma "fullset_is_ring_with_one" )"2" (expand "ring_with_one?" )"2" (flatten)"2" (expand "monoid?" ) (("2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"T" ring_with_one nil )"[T, T -> T]" ring_with_one nil )nil ring_with_one nil )"set" sets nil )nil monad nil )"bool" monad_def nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil monad nil )"T" ring_with_one nil )"bool" ring_with_one_def nil )"bool" monoid_def nil )nil ring_with_one nil ))nil 3293956723"" (skolem!)"" (rewrite "negative_times" )"" (rewrite "one_times" ) nil nil )) nil ))nil )nil monad nil )nil ring nil )"T" ring_with_one nil )nil ring_with_one nil )"[T, T -> T]" ring_with_one nil )"[T, T -> T]" ring_with_one nil )"T" ring_with_one nil ))nil 3293956819"" (skolem!)"" (rewrite "times_negative" )"" (rewrite "times_one" ) nil nil )) nil ))nil )nil monad nil )nil ring nil )"T" ring_with_one nil )nil ring_with_one nil )"[T, T -> T]" ring_with_one nil )"[T, T -> T]" ring_with_one nil )"T" ring_with_one nil ))nil 3293956844"" (assert )"" (rewrite "minus_one_times" )"" (rewrite "negate_negate" ) nil nil )) nil ))nil )nil group nil )nil ring_with_one nil )nil ring_with_one nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[T, T -> T]" ring_with_one nil )"T" ring_with_one nil )"{y | x * y = one AND y * x = one}" group nil )"T" ring_with_one nil ))nil 3293390922"" (skosimp)"" (typepred "x!1" )"" (expand "ring_with_one?" ) (("" (flatten) nil nil )) nil ))nil ))nil )nil ring_with_one nil )"bool" ring_with_one_def nil )"T" ring_with_one nil )"T" ring_with_one nil )"[T, T -> T]" ring_with_one nil )"[T, T -> T]" ring_with_one nil )set type-eq-decl nil sets nil )nil ring_with_one nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3293390922"" (skosimp*)"" (typepred "x!1" )"" (expand "ring_with_one?" ) (("" (flatten) nil nil )) nil ))nil ))nil )nil ring_with_one nil )"bool" ring_with_one_def nil )"T" ring_with_one nil )"T" ring_with_one nil )"[T, T -> T]" ring_with_one nil )"[T, T -> T]" ring_with_one nil )set type-eq-decl nil sets nil )nil ring_with_one nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))quality 100%
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
