|
(ring
(IMP_abelian_group_TCC1 0
(IMP_abelian_group_TCC1-1 nil 3293388039
("" (lemma "fullset_is_ring")
(("" (expand "ring?") (("" (flatten) nil nil)) nil)) nil)
((ring? const-decl "bool" ring_def nil)
(fullset_is_ring formula-decl nil ring nil))
shostak))
(ring_TCC1 0
(ring_TCC1-1 nil 3293388021
("" (lemma "fullset_is_ring") (("" (propax) nil nil)) nil)
((fullset_is_ring formula-decl nil ring nil)) shostak))
(plus_associative 0
(plus_associative-1 nil 3293388105
("" (grind) (("" (rewrite "associative") nil nil)) nil)
((associative formula-decl nil semigroup nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil))
shostak))
(plus_commutative 0
(plus_commutative-1 nil 3293388201
("" (lemma "fullset_is_ring")
(("" (expand "ring?")
(("" (expand "abelian_group?")
(("" (flatten)
(("" (hide-all-but (-2 1)) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((ring? const-decl "bool" ring_def nil)
(fullset const-decl "set" sets nil)
(restrict const-decl "R" restrict nil)
(commutative? const-decl "bool" operator_defs nil)
(T formal-nonempty-type-decl nil ring nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(abelian_group? const-decl "bool" group_def nil)
(fullset_is_ring formula-decl nil ring nil))
shostak))
(times_associative 0
(times_associative-1 nil 3293904870
("" (lemma "fullset_is_ring")
(("" (expand "ring?")
(("" (flatten)
(("" (expand "semigroup?")
(("" (flatten)
(("" (expand "associative?")
(("" (expand "restrict")
(("" (skosimp)
(("" (inst - "x!1" "y!1" "z!1")
(("1" (expand "fullset") (("1" (propax) nil nil))
nil)
("2" (expand "fullset") (("2" (propax) nil nil))
nil)
("3" (expand "fullset") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ring? const-decl "bool" ring_def nil)
(associative? const-decl "bool" operator_defs nil)
(z!1 skolem-const-decl "T" ring nil)
(y!1 skolem-const-decl "T" ring nil)
(x!1 skolem-const-decl "T" ring nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ring nil)
(restrict const-decl "R" restrict nil)
(fullset_is_ring formula-decl nil ring nil))
shostak))
(right_distributive 0
(right_distributive-1 nil 3293390370
("" (lemma "fullset_is_ring")
(("" (expand "ring?")
(("" (flatten)
(("" (expand "restrict")
(("" (expand "right_distributive?")
(("" (skosimp)
(("" (inst - "x!1" "y!1" "z!1")
(("1" (expand "fullset") (("1" (propax) nil nil)) nil)
("2" (expand "fullset") (("2" (propax) nil nil)) nil)
("3" (expand "fullset") (("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ring? const-decl "bool" ring_def nil)
(restrict const-decl "R" restrict nil)
(z!1 skolem-const-decl "T" ring nil)
(y!1 skolem-const-decl "T" ring nil)
(x!1 skolem-const-decl "T" ring nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ring nil)
(right_distributive? const-decl "bool" operator_defs_more nil)
(fullset_is_ring formula-decl nil ring nil))
shostak))
(left_distributive 0
(left_distributive-1 nil 3293390386
("" (lemma "fullset_is_ring")
(("" (expand "ring?")
(("" (expand "left_distributive?")
(("" (expand "restrict")
(("" (flatten)
(("" (skosimp)
(("" (inst - "x!1" "y!1" "z!1")
(("1" (expand "fullset") (("1" (propax) nil nil)) nil)
("2" (expand "fullset") (("2" (propax) nil nil)) nil)
("3" (expand "fullset") (("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ring? const-decl "bool" ring_def nil)
(restrict const-decl "R" restrict nil)
(z!1 skolem-const-decl "T" ring nil)
(y!1 skolem-const-decl "T" ring nil)
(x!1 skolem-const-decl "T" ring nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ring nil)
(left_distributive? const-decl "bool" operator_defs_more nil)
(fullset_is_ring formula-decl nil ring nil))
shostak))
(zero_plus 0
(zero_plus-1 nil 3293640798
("" (lemma "left_identity") (("" (propax) nil nil)) nil)
((left_identity formula-decl nil monad nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(zero formal-const-decl "T" ring nil))
shostak))
(plus_zero 0
(plus_zero-1 nil 3293640811
("" (lemma "right_identity") (("" (propax) nil nil)) nil)
((right_identity formula-decl nil monad nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(zero formal-const-decl "T" ring nil))
shostak))
(negate_is_left_inv 0
(negate_is_left_inv-1 nil 3293640820
("" (lemma "inv_left") (("" (propax) nil nil)) nil)
((inv_left formula-decl nil group nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(zero formal-const-decl "T" ring nil))
shostak))
(negate_is_right_inv 0
(negate_is_right_inv-1 nil 3293640855
("" (lemma "inv_right") (("" (propax) nil nil)) nil)
((inv_right formula-decl nil group nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(zero formal-const-decl "T" ring nil))
shostak))
(cancel_right_plus 0
(cancel_right_plus-1 nil 3293904329
("" (lemma "cancel_right[T,+,zero]") (("" (propax) nil nil)) nil)
((cancel_right formula-decl nil group nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(zero formal-const-decl "T" ring nil))
shostak))
(cancel_left_plus 0
(cancel_left_plus-1 nil 3293904361
("" (lemma "cancel_left[T,+,zero]") (("" (propax) nil nil)) nil)
((cancel_left formula-decl nil group nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(zero formal-const-decl "T" ring nil))
shostak))
(negate_negate 0
(negate_negate-1 nil 3293641012
("" (lemma "inv_inv") (("" (propax) nil nil)) nil)
((inv_inv formula-decl nil group nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(zero formal-const-decl "T" ring nil))
shostak))
(cancel_right_minus 0
(cancel_right_minus-1 nil 3293904370
("" (lemma "cancel_right_inv[T,+,zero]") (("" (propax) nil nil))
nil)
((cancel_right_inv formula-decl nil group nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(zero formal-const-decl "T" ring nil))
shostak))
(cancel_left_minus 0
(cancel_left_minus-1 nil 3293904389
("" (lemma "cancel_left_inv[T,+,zero]") (("" (propax) nil nil)) nil)
((cancel_left_inv formula-decl nil group nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(zero formal-const-decl "T" ring nil))
shostak))
(negate_zero 0
(negate_zero-1 nil 3293641054
("" (lemma "inv_one") (("" (propax) nil nil)) nil)
((inv_one formula-decl nil group nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(zero formal-const-decl "T" ring nil))
shostak))
(negate_plus 0
(negate_plus-1 nil 3293641070
("" (lemma "inv_star") (("" (propax) nil nil)) nil)
((inv_star formula-decl nil group nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(zero formal-const-decl "T" ring nil))
shostak))
(times_plus 0
(times_plus-1 nil 3293905399
("" (skosimp*)
(("" (rewrite "left_distributive")
(("" (rewrite "right_distributive")
(("" (rewrite "right_distributive")
(("" (assert)
(("" (rewrite "plus_associative")
(("" (rewrite "plus_associative")
(("" (rewrite "plus_associative")
(("" (rewrite "plus_associative") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((left_distributive formula-decl nil ring nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(plus_associative formula-decl nil ring nil)
(* formal-const-decl "[T, T -> T]" ring nil)
(right_distributive formula-decl nil ring nil))
shostak))
(idempotent_add_is_zero 0
(idempotent_add_is_zero-1 nil 3293905643
("" (skosimp*)
((""
(lemma "cancel_right_minus"
("z" "x!1" "x" "x!1 + x!1" "y" "x!1"))
(("" (replace -1 -2 rl)
(("" (hide -1)
(("" (rewrite "plus_associative" -1)
(("" (rewrite "negate_is_right_inv")
(("" (rewrite "plus_zero") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((+ formal-const-decl "[T, T -> T]" ring nil)
(T formal-nonempty-type-decl nil ring nil)
(cancel_right_minus formula-decl nil ring nil)
(negate_is_right_inv formula-decl nil ring nil)
(one_right formula-decl nil group nil)
(inv_right formula-decl nil group nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(zero formal-const-decl "T" ring nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(plus_associative formula-decl nil ring nil))
shostak))
(zero_times 0
(zero_times-1 nil 3293948425
("" (skolem!)
(("" (lemma "left_distributive" ("x" "zero" "y" "zero" "z" "x!1"))
(("" (rewrite "zero_plus")
(("" (lemma "idempotent_add_is_zero" ("x" "zero*x!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((zero formal-const-decl "T" ring nil)
(T formal-nonempty-type-decl nil ring nil)
(left_distributive formula-decl nil ring nil)
(* formal-const-decl "[T, T -> T]" ring nil)
(idempotent_add_is_zero formula-decl nil ring nil)
(zero_plus formula-decl nil ring nil))
shostak))
(times_zero 0
(times_zero-1 nil 3293951117
("" (skosimp*)
(("" (lemma "right_distributive" ("x" "x!1" "y" "zero" "z" "zero"))
(("" (rewrite "zero_plus")
(("" (lemma "idempotent_add_is_zero" ("x" "x!1*zero"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((zero formal-const-decl "T" ring nil)
(T formal-nonempty-type-decl nil ring nil)
(right_distributive formula-decl nil ring nil)
(* formal-const-decl "[T, T -> T]" ring nil)
(idempotent_add_is_zero formula-decl nil ring nil)
(zero_plus formula-decl nil ring nil))
shostak))
(negative_times 0
(negative_times-1 nil 3293952735
("" (skolem!)
((""
(lemma "cancel_right_plus"
("x" "inv(x!1) * y!1" "y" "inv((x!1 * y!1))" "z" "x!1*y!1"))
((""
(lemma "left_distributive"
("x" "inv(x!1)" "y" "x!1" "z" "y!1"))
(("" (replace -2 1 rl)
(("" (hide -2)
(("" (replace -1 1 rl)
(("" (hide -1)
(("" (rewrite "negate_is_left_inv")
(("" (rewrite "zero_times")
(("" (rewrite "negate_is_left_inv") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(zero formal-const-decl "T" ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(* formal-const-decl "[T, T -> T]" ring nil)
(T formal-nonempty-type-decl nil ring nil)
(cancel_right_plus formula-decl nil ring nil)
(negate_is_left_inv formula-decl nil ring nil)
(zero_times formula-decl nil ring nil)
(left_distributive formula-decl nil ring nil))
shostak))
(times_negative 0
(times_negative-1 nil 3293953135
("" (skolem!)
((""
(lemma "right_distributive" ("x" "x!1" "y" "y!1" "z" "inv(y!1)"))
(("" (rewrite "negate_is_right_inv")
(("" (rewrite "times_zero")
((""
(lemma "cancel_left_plus"
("z" "inv((x!1 * y!1))" "x" "zero" "y"
"(x!1 * y!1) + (x!1 * inv(y!1))"))
(("" (replace -1 -2 rl)
(("" (hide -1)
(("" (rewrite "plus_zero")
(("" (rewrite "plus_associative" :dir rl)
(("" (rewrite "negate_is_left_inv")
(("" (rewrite "zero_plus")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(zero formal-const-decl "T" ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ring nil)
(right_distributive formula-decl nil ring nil)
(times_zero formula-decl nil ring nil)
(plus_zero formula-decl nil ring nil)
(one_left formula-decl nil group nil)
(inv_left formula-decl nil group nil)
(plus_associative formula-decl nil ring nil)
(* formal-const-decl "[T, T -> T]" ring nil)
(cancel_left_plus formula-decl nil ring nil)
(negate_is_right_inv formula-decl nil ring nil))
shostak))
(negative_times_negative 0
(negative_times_negative-1 nil 3293951536
("" (skosimp*)
(("" (lemma "negative_times" ("x" "x!1" "y" "inv(y!1)"))
(("" (lemma "times_negative" ("x" "x!1" "y" "y!1"))
(("" (replace -1 -2) (("" (rewrite "inv_inv") nil nil)) nil))
nil))
nil))
nil)
((inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(zero formal-const-decl "T" ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ring nil)
(negative_times formula-decl nil ring nil)
(inv_inv formula-decl nil group nil)
(* formal-const-decl "[T, T -> T]" ring nil)
(times_negative formula-decl nil ring nil))
shostak))
(ring_is_abelian_group 0
(ring_is_abelian_group-1 nil 3293388058
("" (skosimp*)
(("" (typepred "x!1")
(("" (expand "ring?") (("" (flatten) nil nil)) nil)) nil))
nil)
((ring nonempty-type-eq-decl nil ring nil)
(ring? const-decl "bool" ring_def nil)
(zero formal-const-decl "T" ring nil)
(* formal-const-decl "[T, T -> T]" ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil ring nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(subring_is_ring 0
(subring_is_ring-1 nil 3294091203
("" (skosimp)
(("" (typepred "R!1")
(("" (expand "subring?")
(("" (expand "ring?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((ring nonempty-type-eq-decl nil ring nil)
(ring? const-decl "bool" ring_def nil)
(zero formal-const-decl "T" ring nil)
(* formal-const-decl "[T, T -> T]" ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil ring nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subring? const-decl "bool" ring_def nil))
shostak))
(sq_rew 0
(sq_rew-1 nil 3297001249
("" (expand "sq") (("" (propax) nil nil)) nil)
((sq const-decl "T" ring nil)) shostak))
(sq_neg 0
(sq_neg-1 nil 3297001257
("" (expand "sq")
(("" (skosimp) (("" (rewrite "negative_times_negative") nil nil))
nil))
nil)
((T formal-nonempty-type-decl nil ring nil)
(negative_times_negative formula-decl nil ring nil)
(sq const-decl "T" ring nil))
shostak))
(sq_plus 0
(sq_plus-1 nil 3297001295
("" (expand "sq")
(("" (skosimp*)
(("" (rewrite "right_distributive")
(("" (rewrite "left_distributive")
(("" (rewrite "left_distributive")
(("" (assert)
(("" (rewrite "plus_associative")
(("" (rewrite "plus_associative")
(("" (rewrite "plus_associative")
(("" (rewrite "plus_associative")
(("" (lemma "plus_commutative")
(("" (lemma "plus_associative")
((""
(inst-cp - "y!1 * x!1" "x!1 * y!1"
"y!1 * y!1")
(("" (replace -2 1 rl)
((""
(inst
-
"x!1 * y!1"
"y!1 * x!1"
"y!1 * y!1")
((""
(replace -1 1 rl)
((""
(inst - "x!1 * y!1" "y!1 * x!1")
((""
(replace -3)
(("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((left_distributive formula-decl nil ring nil)
(plus_commutative formula-decl nil ring nil)
(plus_associative formula-decl nil ring nil)
(* formal-const-decl "[T, T -> T]" ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(T formal-nonempty-type-decl nil ring nil)
(right_distributive formula-decl nil ring nil)
(sq const-decl "T" ring nil))
shostak))
(sq_minus 0
(sq_minus-1 nil 3297002277
("" (skosimp*)
(("" (lemma "sq_plus" ("x" "x!1" "y" "inv[T, +, zero](y!1)"))
(("" (replace -1 1)
(("" (hide -1)
(("" (rewrite "sq_neg")
(("" (rewrite "times_negative")
(("" (rewrite "negative_times") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(zero formal-const-decl "T" ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil ring nil)
(sq_plus formula-decl nil ring nil)
(times_negative formula-decl nil ring nil)
(negative_times formula-decl nil ring nil)
(sq_neg formula-decl nil ring nil))
shostak))
(sq_neg_minus 0
(sq_neg_minus-1 nil 3297002149
("" (skosimp)
(("" (rewrite "sq_neg" 1 :dir rl)
(("" (rewrite "negate_plus")
(("" (rewrite "negate_negate") nil nil)) nil))
nil))
nil)
((sq_neg formula-decl nil ring nil)
(T formal-nonempty-type-decl nil ring nil)
(+ formal-const-decl "[T, T -> T]" ring nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(zero formal-const-decl "T" ring nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(negate_plus formula-decl nil ring nil)
(inv_inv formula-decl nil group nil))
shostak))
(sq_zero 0
(sq_zero-1 nil 3297002231
("" (expand "sq") (("" (rewrite "zero_times") nil nil)) nil)
((zero_times formula-decl nil ring nil)
(T formal-nonempty-type-decl nil ring nil)
(zero formal-const-decl "T" ring nil) (sq const-decl "T" ring nil))
shostak)))
¤ Dauer der Verarbeitung: 0.43 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
