Quelle ring_nz_closed.prf
Sprache: Lisp
(ring_nz_closednil 3293963187"" (lemma "fullset_is_ring_nz_closed" )"" (expand "ring_nz_closed?" ) (("" (flatten) nil nil )) nil )) nil )"bool" ring_nz_closed_def nil )nil ring_nz_closed nil ))nil 3293963187"" (lemma "fullset_is_ring_nz_closed" ) (("" (propax) nil nil )) nil )nil ring_nz_closed nil ))nil 3293963211"" (skolem!) (("" (typepred "R!1" ) (("" (propax) nil nil )) nil ))nil )nil ring_nz_closed nil )"bool" ring_nz_closed_def nil )"T" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )set type-eq-decl nil sets nil )nil ring_nz_closed nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3293963187"" (skolem!)"" (typepred "x!1" )"" (expand "ring_nz_closed?" ) (("" (flatten) nil nil )) nil ))nil ))nil )nil ring_nz_closed nil )"bool" ring_nz_closed_def nil )"T" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )set type-eq-decl nil sets nil )nil ring_nz_closed nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3293964256"" (skosimp*)"" (typepred "nzx!1" )"" (typepred "nzy!1" )"" (skosimp*)"" (lemma "fullset_is_ring_nz_closed" )"" (expand "ring_nz_closed?" )"" (flatten)"" (expand "nz_closed?" )"" (hide -1)"" (expand "star_closed?" )"" (inst - "nzx!1" "nzy!1" )"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil ring_nz_closed_def nil )"[T, T -> T]" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )"T" ring_nz_closed nil )"boolean" notequal nil )nil ring_nz_closed nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" ring_nz_closed_def nil )"bool" ring_nz_closed_def nil )"bool" groupoid_def nil )"bool" sets nil )"nz_T[T, +, *, zero]" ring_nz_closed nil )"nz_T[T, +, *, zero]" ring_nz_closed nil )"set" sets nil )"set" sets nil ) (set type-eq-decl nil sets nil )nil ring_nz_closed nil ))nil 3293964256"" (skosimp 1)"" (lemma "negate_negate" ("x" "nzx!1" ))"" (replace -2)"" (rewrite "negate_zero" )"" (typepred "nzx!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"T" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )nil ring_nz_closed nil )nil ring_nz_closed_def nil )"boolean" notequal nil )nil booleans nil )nil ring nil )nil ring nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3293966061"" (skolem!)"" (prop)"1" (lemma "nz_T_times_nz_T_is_nz_T" ("nzx" "x!1" "nzy" "y!1" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil )"2" (replace -1) (("2" (rewrite "zero_times" ) nil nil )) nil )"3" (replace -1) (("3" (rewrite "times_zero" ) nil nil )) nil ))nil ))nil )nil ring_nz_closed nil )nil ring_nz_closed nil )nil booleans nil )"boolean" notequal nil )"T" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )nil ring_nz_closed_def nil )nil ring nil )nil ring nil ))nil 3293967447"" (skosimp)"" (typepred "nzx!1" )"" (skosimp)"" (lemma "times_is_zero" ("x" "nzx!1" "y" "y!1" ))"" (grind) nil nil )) nil ))nil ))nil ))nil )nil ring_nz_closed_def nil )"[T, T -> T]" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )"T" ring_nz_closed nil )"boolean" notequal nil )nil ring_nz_closed nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil ring_nz_closed nil ))nil 3293967527"" (skosimp)"" (lemma "times_is_zero" ("x" "x!1" "y" "nzy!1" ))"" (typepred "nzy!1" ) (("" (grind) nil nil )) nil )) nil ))nil )nil ring_nz_closed_def nil )"[T, T -> T]" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )"T" ring_nz_closed nil )"boolean" notequal nil )nil booleans nil )nil ring_nz_closed nil )nil ring_nz_closed nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3293967555"" (skosimp)"" "nz_T_times_nz_T_is_nz_T" ("nzx" "nzx!1" "nzy" "nzy!1" ))"" (assert ) nil nil )) nil ))nil )nil ring_nz_closed_def nil )"[T, T -> T]" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )"T" ring_nz_closed nil )"boolean" notequal nil )nil booleans nil )nil ring_nz_closed nil )nil ring_nz_closed nil )"nz_T" nil ))nil 3297003228"" (expand "sq" )"" (skosimp)"" "nz_T_times_nz_T_is_not_zero" "nzx" "nzx!1" "nzy" "nzx!1" ))"" (assert ) nil nil )) nil ))nil ))nil )"nz_T" nil )nil ring_nz_closed nil )nil ring_nz_closed nil )nil booleans nil )"boolean" notequal nil )"T" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )nil ring_nz_closed_def nil )"T" ring nil ))nil 3297003276"" (skosimp)"" (expand "sq" )"" (prop)"1" (lemma "times_is_zero" ("x" "x!1" "y" "x!1" ))"1" (assert ) nil nil )) nil )"2" (replace -1) (("2" (rewrite "zero_times" ) nil nil )) nil ))nil ))nil ))nil )"T" ring nil )"T" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )"[T, T -> T]" ring_nz_closed nil )nil ring nil )nil ring_nz_closed nil )nil ring_nz_closed nil ))quality 100%
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
