| products/Sources/formale Sprachen/PVS/algebra/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: complex_field.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(division_ring
(fullset_is_division_ring 0 (fullset_is_division_ring-1 nil 3292788503 ("" (expand "division_ring?") (("" (lemma "fullset_is_ring") (("" (assert) (("" (hide -1) (("" (expand "group?") (("" (expand "monoid?") (("" (lemma "star_associative") (("" (lemma "star_closed") (("" (lemma "zero_is_not_one") (("" (lemma "star_inv_exists") (("" (expand "semigroup?") (("" (expand "star_closed?") (("" (expand "associative?") (("" (expand "left_identity?") (("" (expand "right_identity?") (("" (expand "inv_exists?") (("" (expand "fullset") (("" (expand "remove") (("" (expand "restrict") (("" (expand "member") (("" (split 1) (("1" (skolem!) (("1" (inst -4 "x!1" "y!1" "z!1") nil nil)) nil) ("2" (lemma "one_left_identity") (("2" (propax) nil nil)) nil) ("3" (lemma "one_right_identity") (("3" (propax) nil nil)) nil) ("4" (skolem!) (("4" (inst -1 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset_is_ring formula-decl nil ring nil)) shostak)) (IMP_ring_with_one_TCC1 0 (IMP_ring_with_one_TCC1-1 nil 3293394587 ("" (lemma "fullset_is_division_ring") (("" (expand "division_ring?") (("" (flatten) nil nil)) nil)) nil) ((division_ring? const-decl "bool" division_ring_def nil) (fullset_is_division_ring formula-decl nil division_ring nil)) shostak)) (IMP_ring_nz_closed_TCC1 0 (IMP_ring_nz_closed_TCC1-1 nil 3293984282 ("" (lemma "fullset_is_division_ring") (("" (expand "division_ring?") (("" (expand "ring_nz_closed?") (("" (expand "group?") (("" (expand "monoid?") (("" (expand "monad?") (("" (expand "groupoid?") (("" (expand "nz_closed?") (("" (expand "ring_with_one?") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((division_ring? const-decl "bool" division_ring_def nil) (group? const-decl "bool" group_def nil) (monad? const-decl "bool" monad_def nil) (ring_with_one? const-decl "bool" ring_with_one_def nil) (member const-decl "bool" sets nil) (nz_closed? const-decl "bool" ring_nz_closed_def nil) (monoid? const-decl "bool" monoid_def nil) (ring_nz_closed? const-decl "bool" ring_nz_closed_def nil) (fullset_is_division_ring formula-decl nil division_ring nil)) shostak)) (IMP_group_TCC1 0 (IMP_group_TCC1-1 nil 3293999365 ("" (skosimp) (("" (lemma "fullset_is_division_ring") (("" (typepred "x1!1`1") (("" (typepred "x1!1`2") (("" (expand "division_ring?") (("" (flatten) (("" (hide -1) (("" (expand "group?") (("" (expand "monoid?") (("" (expand "monad?") (("" (expand "groupoid?") (("" (expand "star_closed?") (("" (flatten) (("" (inst - "x1!1`1" "x1!1`2") (("1" (expand "member") (("1" (expand "remove") (("1" (expand "member") (("1" (expand "fullset") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (expand "fullset") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset_is_division_ring formula-decl nil division_ring nil) (group? const-decl "bool" group_def nil) (monad? const-decl "bool" monad_def nil) (member const-decl "bool" sets nil) (nz_T_times_nz_T_is_nz_T application-judgement "nz_T" division_ring nil) (x1!1 skolem-const-decl "[nz_T[T, +, *, zero], nz_T[T, +, *, zero]]" division_ring nil) (fullset const-decl "set" sets nil) (remove const-decl "set" sets nil) (set type-eq-decl nil sets nil) (star_closed? const-decl "bool" groupoid_def nil) (monoid? const-decl "bool" monoid_def nil) (division_ring? const-decl "bool" division_ring_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-nonempty-type-decl nil division_ring nil) (/= const-decl "boolean" notequal nil) (zero formal-const-decl "T" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil)) shostak)) (IMP_group_TCC2 0 (IMP_group_TCC2-1 nil 3293999365 ("" (lemma "fullset_is_division_ring") (("" (expand "division_ring?") (("" (expand "group?") (("" (expand "monoid?") (("" (expand "monad?") (("" (flatten) (("" (hide-all-but (-3 -7)) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((division_ring? const-decl "bool" division_ring_def nil) (monoid? const-decl "bool" monoid_def nil) (/= const-decl "boolean" notequal nil) (fullset const-decl "set" sets nil) (member const-decl "bool" sets nil) (remove const-decl "set" sets nil) (monad? const-decl "bool" monad_def nil) (group? const-decl "bool" group_def nil) (fullset_is_division_ring formula-decl nil division_ring nil)) shostak)) (IMP_group_TCC3 0 (IMP_group_TCC3-1 nil 3293999366 ("" (lemma "fullset_is_division_ring") (("" (expand "division_ring?") (("" (flatten) (("" (hide -1) (("" (expand "group?") (("" (flatten) (("" (split) (("1" (hide -2) (("1" (expand "monoid?") (("1" (expand "semigroup?") (("1" (flatten) (("1" (split) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil) ("3" (hide-all-but (-3 1)) (("3" (grind) nil nil)) nil) ("4" (hide-all-but (-4 1)) (("4" (expand "identity?") (("4" (skosimp) (("4" (expand "restrict") (("4" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "inv_exists?") (("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "fullset") (("2" (inst - "x!1") (("1" (skosimp) (("1" (typepred "y!1") (("1" (expand "remove") (("1" (flatten) (("1" (inst + "y!1") (("1" (assert) nil nil) ("2" (expand "member") (("2" (expand "fullset") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((division_ring? const-decl "bool" division_ring_def nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (y!1 skolem-const-decl "(remove(zero, fullset[T]))" division_ring nil) (x!1 skolem-const-decl "(fullset[nz_T[T, +, *, zero]])" division_ring nil) (inv_exists? const-decl "bool" group_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (zero formal-const-decl "T" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (set type-eq-decl nil sets nil) (associative? const-decl "bool" operator_defs nil) (remove const-decl "set" sets nil) (fullset const-decl "set" sets nil) (member const-decl "bool" sets nil) (star_closed? const-decl "bool" groupoid_def nil) (one formal-const-decl "T" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (T formal-nonempty-type-decl nil division_ring nil) (right_identity formula-decl nil monad nil) (restrict const-decl "R" restrict nil) (left_identity formula-decl nil monad nil) (identity? const-decl "bool" operator_defs nil) (monad? const-decl "bool" monad_def nil) (nz_T_times_nz_T_is_nz_T application-judgement "nz_T" division_ring nil) (monoid? const-decl "bool" monoid_def nil) (group? const-decl "bool" group_def nil) (fullset_is_division_ring formula-decl nil division_ring nil)) shostak)) (IMP_group_TCC4 0 (IMP_group_TCC4-1 nil 3293999366 ("" (inst + "one") (("" (lemma "fullset_is_division_ring") (("" (expand "division_ring?") (("" (expand "group?") (("" (expand "monoid?") (("" (expand "monad?") (("" (flatten) (("" (hide-all-but (-3 -7)) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset_is_division_ring formula-decl nil division_ring nil) (group? const-decl "bool" group_def nil) (monad? const-decl "bool" monad_def nil) (remove const-decl "set" sets nil) (member const-decl "bool" sets nil) (fullset const-decl "set" sets nil) (monoid? const-decl "bool" monoid_def nil) (division_ring? const-decl "bool" division_ring_def nil) (one formal-const-decl "T" division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (zero formal-const-decl "T" division_ring nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil division_ring nil)) shostak)) (division_ring_TCC1 0 (division_ring_TCC1-1 nil 3292788692 ("" (lemma "fullset_is_division_ring") (("" (propax) nil nil)) nil) ((fullset_is_division_ring formula-decl nil division_ring nil)) shostak)) (division_ring_is 0 (division_ring_is-1 nil 3292788467 ("" (skolem!) (("" (typepred "R!1") (("" (expand "division_ring?") (("" (flatten) nil nil)) nil)) nil)) nil) ((division_ring nonempty-type-eq-decl nil division_ring nil) (division_ring? const-decl "bool" division_ring_def nil) (one formal-const-decl "T" division_ring nil) (zero formal-const-decl "T" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil division_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)) (division_ring_is_ring_with_one 0 (division_ring_is_ring_with_one-1 nil 3293989482 ("" (skosimp*) (("" (typepred "x!1") (("" (expand "division_ring?") (("" (flatten) nil nil)) nil)) nil)) nil) ((division_ring nonempty-type-eq-decl nil division_ring nil) (division_ring? const-decl "bool" division_ring_def nil) (one formal-const-decl "T" division_ring nil) (zero formal-const-decl "T" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil division_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)) (division_ring_is_ring_nz_closed 0 (division_ring_is_ring_nz_closed-1 nil 3293984400 ("" (skosimp) (("" (typepred "x!1") (("" (expand "division_ring?") (("" (expand "ring_nz_closed?") (("" (expand "ring_with_one?") (("" (expand "group?") (("" (expand "monoid?") (("" (expand "monad?") (("" (expand "groupoid?") (("" (flatten) (("" (expand "star_closed?") (("" (expand "nz_closed?") (("" (split) (("1" (propax) nil nil) ("2" (hide-all-but (-6 1)) (("2" (expand "star_closed?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((division_ring nonempty-type-eq-decl nil division_ring nil) (division_ring? const-decl "bool" division_ring_def nil) (one formal-const-decl "T" division_ring nil) (zero formal-const-decl "T" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil division_ring nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (ring_nz_closed? const-decl "bool" ring_nz_closed_def nil) (group? const-decl "bool" group_def nil) (monad? const-decl "bool" monad_def nil) (star_closed? const-decl "bool" groupoid_def nil) (nz_closed? const-decl "bool" ring_nz_closed_def nil) (monoid? const-decl "bool" monoid_def nil) (ring_with_one? const-decl "bool" ring_with_one_def nil)) shostak)) (division_ring_is_group 0 (division_ring_is_group-1 nil 3293984538 ("" (skosimp) (("" (typepred "R!1") (("" (expand "division_ring?") (("" (flatten) (("" (hide -1) (("" (expand "group?") (("" (expand "monoid?") (("" (expand "monad?") (("" (expand "groupoid?") (("" (flatten) (("" (split) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil) ("3" (hide-all-but (-3 1)) (("3" (expand "identity?") (("3" (skosimp) (("3" (expand "restrict") (("3" (inst - "x!1") (("3" (expand "remove") (("3" (expand "member") (("3" (typepred "x!1") (("3" (expand "restrict") (("3" (expand "remove") (("3" (expand "member") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-4 1)) (("4" (grind) nil nil)) nil) ("5" (hide-all-but (-5 1)) (("5" (expand "inv_exists?") (("5" (skosimp) (("5" (typepred "x!1") (("5" (expand "restrict") (("5" (expand "remove") (("5" (expand "member") (("5" (inst - "x!1") (("1" (skosimp) (("1" (typepred "y!1") (("1" (expand "remove") (("1" (flatten) (("1" (expand "member") (("1" (inst + "y!1") (("1" (assert) nil nil) ("2" (expand "restrict") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((division_ring nonempty-type-eq-decl nil division_ring nil) (division_ring? const-decl "bool" division_ring_def nil) (one formal-const-decl "T" division_ring nil) (zero formal-const-decl "T" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil division_ring nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (group? const-decl "bool" group_def nil) (monad? const-decl "bool" monad_def nil) (member const-decl "bool" sets nil) (remove const-decl "set" sets nil) (/= const-decl "boolean" notequal nil) (restrict const-decl "R" restrict nil) (star_closed? const-decl "bool" groupoid_def nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (identity? const-decl "bool" operator_defs nil) (R!1 skolem-const-decl "division_ring" division_ring nil) (x!1 skolem-const-decl "(restrict[T, nz_T[T, +, *, zero], boolean](remove(zero, R!1)))" division_ring nil) (associative? const-decl "bool" operator_defs nil) (inv_exists? const-decl "bool" group_def nil) (x!1 skolem-const-decl "(restrict[T, nz_T[T, +, *, zero], boolean](remove(zero, R!1)))" division_ring nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (y!1 skolem-const-decl "(remove(zero, R!1))" division_ring nil) (monoid? const-decl "bool" monoid_def nil)) shostak)) (one_ne_zero 0 (one_ne_zero-1 nil 3294002114 ("" (lemma "fullset_is_division_ring") (("" (expand "division_ring?") (("" (expand "group?") (("" (expand "monoid?") (("" (expand "monad?") (("" (flatten) (("" (hide-all-but (-3 -7)) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((division_ring? const-decl "bool" division_ring_def nil) (monoid? const-decl "bool" monoid_def nil) (/= const-decl "boolean" notequal nil) (fullset const-decl "set" sets nil) (member const-decl "bool" sets nil) (remove const-decl "set" sets nil) (monad? const-decl "bool" monad_def nil) (group? const-decl "bool" group_def nil) (fullset_is_division_ring formula-decl nil division_ring nil)) shostak)) (cancel_times_right 0 (cancel_times_right-1 nil 3293990272 ("" (skosimp) (("" (prop) (("1" (case-replace "x!1=zero") (("1" (rewrite "zero_times") (("1" (lemma "times_is_zero" ("x" "y!1" "y" "n0z!1")) (("1" (typepred "n0z!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case-replace "y!1=zero") (("1" (rewrite "zero_times") (("1" (lemma "times_is_zero" ("x" "x!1" "y" "n0z!1")) (("1" (typepred "n0z!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "cancel_right[nz_T,*,one]" ("x" "x!1" "y" "y!1" "z" "n0z!1")) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((cancel_right formula-decl nil group nil) (restrict const-decl "R" restrict nil) (one formal-const-decl "T" division_ring nil) (zero_times formula-decl nil ring nil) (/= const-decl "boolean" notequal nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (times_is_zero formula-decl nil ring_nz_closed nil) (zero formal-const-decl "T" division_ring nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil division_ring nil)) shostak)) (cancel_times_left 0 (cancel_times_left-1 nil 3294000455 ("" (skosimp) (("" (prop) (("1" (case-replace "x!1=zero") (("1" (rewrite "times_zero") (("1" (lemma "times_is_zero" ("x" "n0z!1" "y" "y!1")) (("1" (typepred "n0z!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case-replace "y!1=zero") (("1" (rewrite "times_zero") (("1" (lemma "times_is_zero" ("x" "n0z!1" "y" "x!1")) (("1" (typepred "n0z!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "cancel_left[nz_T,*,one]" ("x" "x!1" "y" "y!1" "z" "n0z!1")) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((cancel_left formula-decl nil group nil) (restrict const-decl "R" restrict nil) (one formal-const-decl "T" division_ring nil) (times_zero formula-decl nil ring nil) (/= const-decl "boolean" notequal nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (times_is_zero formula-decl nil ring_nz_closed nil) (zero formal-const-decl "T" division_ring nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil division_ring nil)) shostak)) (idempotent_times 0 (idempotent_times-1 nil 3293989688 ("" (skosimp) (("" (prop) (("1" (lemma "cancel_times_right" ("n0z" "x!1" "x" "x!1" "y" "one")) (("1" (rewrite "one_times") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1 * lr) (("2" (rewrite "zero_times") nil nil)) nil) ("3" (replace -1 * lr) (("3" (rewrite "one_times") nil nil)) nil)) nil)) nil) ((one_times formula-decl nil ring_with_one nil) (cancel_times_right formula-decl nil division_ring nil) (T formal-nonempty-type-decl nil division_ring nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero formal-const-decl "T" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (one formal-const-decl "T" division_ring nil) (zero_times formula-decl nil ring nil)) shostak)) (recip_ne_zero 0 (recip_ne_zero-1 nil 3294000909 ("" (skosimp) (("" (typepred "n0x!1") (("" (skosimp) (("" (lemma "cancel_times_right" ("x" "inv[nz_T, restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0x!1)" "y" "zero" "n0z" "n0x!1")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (rewrite "zero_times") (("1" (rewrite "inv_left") (("1" (lemma "one_ne_zero") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "one_ne_zero") (("2" (propax) nil nil)) nil) ("3" (lemma "nz_T_times_nz_T_is_not_zero") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((nz_T type-eq-decl nil ring_nz_closed_def nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (zero formal-const-decl "T" division_ring nil) (/= const-decl "boolean" notequal nil) (T formal-nonempty-type-decl nil division_ring nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (restrict const-decl "R" restrict nil) (one formal-const-decl "T" division_ring nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (cancel_times_right formula-decl nil division_ring nil) (inv_left formula-decl nil group nil) (one_ne_zero formula-decl nil division_ring nil) (zero_times formula-decl nil ring nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil)) shostak)) (nz_T_div_nz_T_is_nz_T 0 (nz_T_div_nz_T_is_nz_T-1 nil 3294001939 ("" (skosimp) (("" (typepred "n0x!1") (("" (lemma "recip_ne_zero" ("n0x" "n0y!1")) (("" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "n0x!1" "nzy" "inv[nz_T, restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0y!1)")) (("1" (assert) nil nil) ("2" (rewrite "one_ne_zero") nil nil) ("3" (hide-all-but 1) (("3" (skosimp) (("3" (typepred "x1!1`1") (("3" (typepred "x1!1`2") (("3" (lemma "times_is_zero" ("x" "x1!1`1" "y" "x1!1`2")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nz_T type-eq-decl nil ring_nz_closed_def nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (zero formal-const-decl "T" division_ring nil) (/= const-decl "boolean" notequal nil) (T formal-nonempty-type-decl nil division_ring nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (restrict const-decl "R" restrict nil) (one formal-const-decl "T" division_ring nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil) (one_ne_zero formula-decl nil division_ring nil) (times_is_zero formula-decl nil ring_nz_closed nil) (recip_ne_zero formula-decl nil division_ring nil)) shostak)) (div_simplify 0 (div_simplify-1 nil 3294003584 ("" (skosimp) (("" (rewrite "inv_right[nz_T,*,one]") nil nil)) nil) ((inv_right formula-decl nil group nil) (T formal-nonempty-type-decl nil division_ring nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero formal-const-decl "T" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (restrict const-decl "R" restrict nil) (one formal-const-decl "T" division_ring nil)) shostak)) (cancel_div_right 0 (cancel_div_right-1 nil 3294002510 ("" (skosimp) (("" (prop) (("1" (lemma "cancel_times_right" ("x" "x!1 * inv[nz_T, restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0z!1)" "y" "y!1 * inv[nz_T, restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0z!1)" "n0z" "n0z!1")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (rewrite "associative" -1) (("1" (rewrite "associative" -1) (("1" (rewrite "inv_left" -1) (("1" (rewrite "times_one") (("1" (rewrite "times_one") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "one_ne_zero") (("2" (propax) nil nil)) nil) ("3" (hide -1 2) (("3" (skosimp) (("3" (lemma "times_is_zero" ("x" "x1!1`1" "y" "x1!1`2")) (("3" (typepred "x1!1`1") (("3" (typepred "x1!1`2") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((times_is_zero formula-decl nil ring_nz_closed nil) (NOT const-decl "[bool -> bool]" booleans nil) (one_ne_zero formula-decl nil division_ring nil) (associative formula-decl nil semigroup nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil) (inv_left formula-decl nil group nil) (right_identity formula-decl nil monad nil) (cancel_times_right formula-decl nil division_ring nil) (T formal-nonempty-type-decl nil division_ring nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero formal-const-decl "T" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (one formal-const-decl "T" division_ring nil) (restrict const-decl "R" restrict nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil)) shostak)) (cancel_div_left 0 (cancel_div_left-1 nil 3294004279 ("" (skosimp) (("" (prop) (("1" (lemma "cancel_times_left" ("n0z" "recip(n0z!1)" "x" "n0z!1 * inv[nz_T, restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0x!1)" "y" "n0z!1 * inv[nz_T, restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0y!1)")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (rewrite "associative" -1 :dir rl) (("1" (rewrite "associative" -1 :dir rl) (("1" (rewrite "inv_left") (("1" (rewrite "one_times") (("1" (rewrite "one_times") (("1" (lemma "cancel_left_inv[nz_T,restrict[[T, T],[nz_T[T, +, *, zero], nz_T[T, +, *, zero]] ("z" "one" "x" "n0x!1" "y" "n0y!1")) (("1" (replace -1 1 rl) (("1" (rewrite "one_times" 1) (("1" (rewrite "one_times" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "one_ne_zero") (("2" (propax) nil nil)) nil) ("3" (hide 2 -1) (("3" (skosimp) (("3" (typepred "x1!1`1") (("3" (typepred "x1!1`2") (("3" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "x1!1`1" "nzy" "x1!1`2")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil) (one_ne_zero formula-decl nil division_ring nil) (associative formula-decl nil semigroup nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil) (inv_left formula-decl nil group nil) (one_left formula-decl nil group nil) (cancel_left_inv formula-decl nil group nil) (one_times formula-decl nil ring_with_one nil) (cancel_times_left formula-decl nil division_ring nil) (T formal-nonempty-type-decl nil division_ring nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero formal-const-decl "T" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (one formal-const-decl "T" division_ring nil) (restrict const-decl "R" restrict nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil)) shostak)) (times_div_left 0 (times_div_left-1 nil 3294003161 ("" (skosimp) (("" (rewrite "associative") (("1" (lemma "one_ne_zero") (("1" (propax) nil nil)) nil) ("2" (lemma "nz_T_times_nz_T_is_not_zero") (("2" (propax) nil nil)) nil)) nil)) nil) ((associative formula-decl nil semigroup nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero formal-const-decl "T" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (one formal-const-decl "T" division_ring nil) (restrict const-decl "R" restrict nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (T formal-nonempty-type-decl nil division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil) (one_ne_zero formula-decl nil division_ring nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil)) shostak)) (div_eq_zero 0 (div_eq_zero-1 nil 3294005078 ("" (skosimp) (("" (prop) (("1" (lemma "recip_ne_zero" ("n0x" "n0z!1")) (("1" (name-replace "Z" "inv[nz_T, restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0z!1)") (("1" (lemma "times_is_zero" ("x" "x!1" "y" "Z")) (("1" (assert) nil nil)) nil) ("2" (rewrite "one_ne_zero") nil nil) ("3" (lemma "nz_T_times_nz_T_is_not_zero") (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "zero_times") (("1" (rewrite "one_ne_zero") nil nil) ("2" (lemma "nz_T_times_nz_T_is_not_zero") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (one formal-const-decl "T" division_ring nil) (restrict const-decl "R" restrict nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (times_is_zero formula-decl nil ring_nz_closed nil) (one_ne_zero formula-decl nil division_ring nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil) (recip_ne_zero formula-decl nil division_ring nil) (T formal-nonempty-type-decl nil division_ring nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero formal-const-decl "T" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (zero_times formula-decl nil ring nil)) shostak)) (div_mult 0 (div_mult-1 nil 3294007614 ("" (skosimp) (("" (rewrite "associative" 1) (("1" (lemma "one_ne_zero") (("1" (propax) nil nil)) nil) ("2" (lemma "nz_T_times_nz_T_is_not_zero") (("2" (propax) nil nil)) nil)) nil)) nil) ((associative formula-decl nil semigroup nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero formal-const-decl "T" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (one formal-const-decl "T" division_ring nil) (restrict const-decl "R" restrict nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (T formal-nonempty-type-decl nil division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (right_identity formula-decl nil monad nil) (inv_left formula-decl nil group nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil) (one_ne_zero formula-decl nil division_ring nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil)) shostak)) (div_mult_left 0 (div_mult_left-1 nil 3294006361 ("" (skosimp) (("" (prop) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (rewrite "associative") (("1" (lemma "one_ne_zero") (("1" (propax) nil nil)) nil) ("2" (lemma "nz_T_times_nz_T_is_not_zero") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (rewrite "associative") (("1" (lemma "one_ne_zero") (("1" (propax) nil nil)) nil) ("2" (lemma "nz_T_times_nz_T_is_not_zero") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil) (one_ne_zero formula-decl nil division_ring nil) (right_identity formula-decl nil monad nil) (inv_left formula-decl nil group nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (T formal-nonempty-type-decl nil division_ring nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (restrict const-decl "R" restrict nil) (one formal-const-decl "T" division_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) (nz_T type-eq-decl nil ring_nz_closed_def nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (zero formal-const-decl "T" division_ring nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (associative formula-decl nil semigroup nil) (inv_right formula-decl nil group nil)) shostak)) (div_mult_right 0 (div_mult_right-1 nil 3294006233 ("" (skosimp) (("" (lemma "div_mult_left" ("x" "x!1" "n0z" "n0z!1" "y" "y!1")) (("" (flatten) (("" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil) ((nz_T type-eq-decl nil ring_nz_closed_def nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (zero formal-const-decl "T" division_ring nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil division_ring nil) (div_mult_left formula-decl nil division_ring nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil)) shostak)) (div_distributes 0 (div_distributes-1 nil 3294006930 ("" (skosimp) (("" (lemma "left_distributive" ("x" "x!1" "y" "y!1" "z" "inv[nz_T, restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0z!1)")) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (lemma "one_ne_zero") (("2" (propax) nil nil)) nil)) nil) ("3" (lemma "nz_T_times_nz_T_is_not_zero") (("3" (propax) nil nil)) nil)) nil)) nil) ((zero formal-const-decl "T" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (T formal-nonempty-type-decl nil division_ring nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (restrict const-decl "R" restrict nil) (one formal-const-decl "T" division_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) (nz_T type-eq-decl nil ring_nz_closed_def nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (left_distributive formula-decl nil ring nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil) (one_ne_zero formula-decl nil division_ring nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil)) shostak)) (div_distributes_minus 0 (div_distributes_minus-1 nil 3294007129 ("" (skosimp) (("" (rewrite "negative_times" 1 :dir rl) (("1" (rewrite "left_distributive" 1) (("1" (lemma "one_ne_zero") (("1" (propax) nil nil)) nil) ("2" (lemma "nz_T_times_nz_T_is_not_zero") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "one_ne_zero") (("2" (propax) nil nil)) nil) ("3" (lemma "nz_T_times_nz_T_is_not_zero") (("3" (propax) nil nil)) nil)) nil)) nil) ((negative_times formula-decl nil ring nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (one formal-const-decl "T" division_ring nil) (restrict const-decl "R" restrict nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (T formal-nonempty-type-decl nil division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (zero formal-const-decl "T" division_ring nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil) (one_ne_zero formula-decl nil division_ring nil) (left_distributive formula-decl nil ring nil)) shostak)) (div_div1 0 (div_div1-1 nil 3294007942 ("" (skosimp) (("" (lemma "one_ne_zero") (("" (lemma "nz_T_times_nz_T_is_not_zero") (("" (rewrite "inv_star") (("" (rewrite "associative") (("" (rewrite "inv_inv") nil nil)) nil)) nil)) nil)) nil)) nil) ((one_ne_zero formula-decl nil division_ring nil) (inv_star formula-decl nil group nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (restrict const-decl "R" restrict nil) (one formal-const-decl "T" division_ring nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil) (inv_inv formula-decl nil group nil) (associative formula-decl nil semigroup nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil) (T formal-nonempty-type-decl nil division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (zero formal-const-decl "T" division_ring nil)) shostak)) (div_div2_TCC1 0 (div_div2_TCC1-1 nil 3294008240 ("" (skosimp) (("" (typepred "n0z!1") (("" (typepred "n0y!1") (("" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "n0z!1" "nzy" "n0y!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((nz_T type-eq-decl nil ring_nz_closed_def nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (zero formal-const-decl "T" division_ring nil) (/= const-decl "boolean" notequal nil) (T formal-nonempty-type-decl nil division_ring nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil)) shostak)) (div_div2 0 (div_div2-1 nil 3294007984 ("" (skosimp) (("" (rewrite "inv_star[nz_T, restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one]") (("" (rewrite "associative") (("1" (lemma "one_ne_zero") (("1" (propax) nil nil)) nil) ("2" (lemma "nz_T_times_nz_T_is_not_zero") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((inv_star formula-decl nil group nil) (T formal-nonempty-type-decl nil division_ring nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero formal-const-decl "T" division_ring nil) (+ formal-const-decl "[T, T -> T]" division_ring nil) (* formal-const-decl "[T, T -> T]" division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (restrict const-decl "R" restrict nil) (one formal-const-decl "T" division_ring nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" division_ring nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil) (one_ne_zero formula-decl nil division_ring nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (associative formula-decl nil semigroup nil)) shostak))) ¤ Dauer der Verarbeitung: 0.73 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
