|
(ring_with_one
(IMP_ring_TCC1 0
(IMP_ring_TCC1-1 nil 3293390922
("" (lemma "fullset_is_ring_with_one")
(("" (expand "ring_with_one?")
(("" (flatten)
(("" (expand "ring?") (("" (postpone) nil nil)) nil)) nil))
nil))
nil)
((ring_with_one? const-decl "bool" ring_with_one_def nil)
(fullset_is_ring_with_one formula-decl nil ring_with_one nil))
shostak))
(IMP_monoid_TCC1 0
(IMP_monoid_TCC1-1 nil 3293390922
("" (lemma "fullset_is_ring_with_one")
(("" (expand "ring_with_one?") (("" (flatten) nil nil)) nil)) nil)
((ring_with_one? const-decl "bool" ring_with_one_def nil)
(fullset_is_ring_with_one formula-decl nil ring_with_one nil))
shostak))
(ring_with_one_TCC1 0
(ring_with_one_TCC1-1 nil 3293390922
("" (lemma "fullset_is_ring_with_one") (("" (propax) nil nil)) nil)
((fullset_is_ring_with_one formula-decl nil ring_with_one nil))
shostak))
(one_times 0
(one_times-1 nil 3293907997
("" (lemma "left_identity[T,*,one]") (("" (propax) nil nil)) nil)
((left_identity formula-decl nil monad nil)
(T formal-nonempty-type-decl nil ring_with_one nil)
(* formal-const-decl "[T, T -> T]" ring_with_one nil)
(one formal-const-decl "T" ring_with_one nil))
shostak))
(times_one 0
(times_one-1 nil 3293908022
("" (lemma "right_identity[T,*,one]") (("" (propax) nil nil)) nil)
((right_identity formula-decl nil monad nil)
(T formal-nonempty-type-decl nil ring_with_one nil)
(* formal-const-decl "[T, T -> T]" ring_with_one nil)
(one formal-const-decl "T" ring_with_one nil))
shostak))
(unique_left_identity 0
(unique_left_identity-1 nil 3293908031
("" (skosimp)
((""
(lemma "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)
((one formal-const-decl "T" ring_with_one nil)
(* formal-const-decl "[T, T -> T]" ring_with_one nil)
(T formal-nonempty-type-decl nil ring_with_one nil)
(fullset const-decl "set" sets nil)
(monad nonempty-type-eq-decl nil monad nil)
(monad? const-decl "bool" monad_def nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(unique_left_identity formula-decl nil monad nil)
(x!1 skolem-const-decl "T" ring_with_one nil)
(fullset_is_ring_with_one formula-decl nil ring_with_one nil)
(monoid? const-decl "bool" monoid_def nil)
(ring_with_one? const-decl "bool" ring_with_one_def nil))
shostak))
(unique_right_identity 0
(unique_right_identity-1 nil 3293908156
("" (skosimp)
((""
(lemma "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)
((one formal-const-decl "T" ring_with_one nil)
(* formal-const-decl "[T, T -> T]" ring_with_one nil)
(T formal-nonempty-type-decl nil ring_with_one nil)
(fullset const-decl "set" sets nil)
(monad nonempty-type-eq-decl nil monad nil)
(monad? const-decl "bool" monad_def nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(unique_right_identity formula-decl nil monad nil)
(x!1 skolem-const-decl "T" ring_with_one nil)
(ring_with_one? const-decl "bool" ring_with_one_def nil)
(monoid? const-decl "bool" monoid_def nil)
(fullset_is_ring_with_one formula-decl nil ring_with_one nil))
shostak))
(minus_one_times 0
(minus_one_times-1 nil 3293956723
("" (skolem!)
(("" (rewrite "negative_times")
(("" (rewrite "one_times") nil nil)) nil))
nil)
((left_identity formula-decl nil monad nil)
(negative_times formula-decl nil ring nil)
(one formal-const-decl "T" ring_with_one nil)
(T formal-nonempty-type-decl nil ring_with_one nil)
(+ formal-const-decl "[T, T -> T]" ring_with_one nil)
(* formal-const-decl "[T, T -> T]" ring_with_one nil)
(zero formal-const-decl "T" ring_with_one nil))
shostak))
(times_minus_one 0
(times_minus_one-1 nil 3293956819
("" (skolem!)
(("" (rewrite "times_negative")
(("" (rewrite "times_one") nil nil)) nil))
nil)
((right_identity formula-decl nil monad nil)
(times_negative formula-decl nil ring nil)
(one formal-const-decl "T" ring_with_one nil)
(T formal-nonempty-type-decl nil ring_with_one nil)
(+ formal-const-decl "[T, T -> T]" ring_with_one nil)
(* formal-const-decl "[T, T -> T]" ring_with_one nil)
(zero formal-const-decl "T" ring_with_one nil))
shostak))
(minus_one_sq_is_one 0
(minus_one_sq_is_one-1 nil 3293956844
("" (assert)
(("" (rewrite "minus_one_times")
(("" (rewrite "negate_negate") nil nil)) nil))
nil)
((inv_inv formula-decl nil group nil)
(minus_one_times formula-decl nil ring_with_one nil)
(T formal-nonempty-type-decl nil ring_with_one 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)
(+ formal-const-decl "[T, T -> T]" ring_with_one nil)
(zero formal-const-decl "T" ring_with_one nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(one formal-const-decl "T" ring_with_one nil))
shostak))
(ring_with_one_is_ring 0
(ring_with_one_is_ring-1 nil 3293390922
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "ring_with_one?") (("" (flatten) nil nil)) nil))
nil))
nil)
((ring_with_one nonempty-type-eq-decl nil ring_with_one nil)
(ring_with_one? const-decl "bool" ring_with_one_def nil)
(one formal-const-decl "T" ring_with_one nil)
(zero formal-const-decl "T" ring_with_one nil)
(* formal-const-decl "[T, T -> T]" ring_with_one nil)
(+ formal-const-decl "[T, T -> T]" ring_with_one nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil ring_with_one nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(ring_with_one_is_monoid 0
(ring_with_one_is_monoid-1 nil 3293390922
("" (skosimp*)
(("" (typepred "x!1")
(("" (expand "ring_with_one?") (("" (flatten) nil nil)) nil))
nil))
nil)
((ring_with_one nonempty-type-eq-decl nil ring_with_one nil)
(ring_with_one? const-decl "bool" ring_with_one_def nil)
(one formal-const-decl "T" ring_with_one nil)
(zero formal-const-decl "T" ring_with_one nil)
(* formal-const-decl "[T, T -> T]" ring_with_one nil)
(+ formal-const-decl "[T, T -> T]" ring_with_one nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil ring_with_one nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
