| products/sources/formale Sprachen/PVS/algebra/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: field.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(field
(fullset_is_field 0 (fullset_is_field-1 nil 3292792257 ("" (expand "field?") (("" (lemma "fullset_is_division_ring") (("" (lemma "star_commutative") (("" (assert) nil nil)) nil)) nil)) nil) ((fullset_is_division_ring formula-decl nil division_ring nil)) shostak)) (IMP_division_ring_TCC1 0 (IMP_division_ring_TCC1-1 nil 3292792094 ("" (lemma "fullset_is_field") (("" (expand "field?") (("" (flatten) nil nil)) nil)) nil) ((field? const-decl "bool" field_def nil) (fullset_is_field formula-decl nil field nil)) shostak)) (IMP_integral_domain_TCC1 0 (IMP_integral_domain_TCC1-1 nil 3293395171 ("" (lemma "fullset_is_field") (("" (expand "field?") (("" (expand "division_ring?") (("" (expand "ring_with_one?") (("" (expand "integral_domain?") (("" (expand "commutative_ring?") (("" (flatten) (("" (assert) (("" (hide-all-but (-3 1)) (("" (expand "group?") (("" (expand "monoid?") (("" (expand "monad?") (("" (expand "groupoid?") (("" (expand "star_closed?") (("" (expand "nz_closed?") (("" (expand "star_closed?") (("" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((field? const-decl "bool" field_def nil) (ring_with_one? const-decl "bool" ring_with_one_def nil) (commutative_ring? const-decl "bool" ring_def nil) (group? const-decl "bool" group_def nil) (monad? const-decl "bool" monad_def nil) (nz_closed? const-decl "bool" ring_nz_closed_def nil) (star_closed? const-decl "bool" groupoid_def nil) (monoid? const-decl "bool" monoid_def nil) (integral_domain? const-decl "bool" integral_domain_def nil) (division_ring? const-decl "bool" division_ring_def nil) (fullset_is_field formula-decl nil field nil)) shostak)) (field_TCC1 0 (field_TCC1-1 nil 3292792094 ("" (lemma "fullset_is_field") (("" (propax) nil nil)) nil) ((fullset_is_field formula-decl nil field nil)) shostak)) (nz_star_TCC1 0 (nz_star_TCC1-1 nil 3294126539 ("" (grind) (("" (typepred "x1!1`1") (("" (typepred "x1!1`2") (("" (lemma "nz_T_times_nz_T_is_nz_T" ("nzx" "x1!1`1" "nzy" "x1!1`2")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((nz_T type-eq-decl nil ring_nz_closed_def nil) (* formal-const-decl "[T, T -> T]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (zero formal-const-decl "T" field nil) (/= const-decl "boolean" notequal nil) (T formal-nonempty-type-decl nil field 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_nz_T judgement-tcc nil ring_nz_closed nil) (restrict const-decl "R" restrict nil)) shostak)) (field_is_division_ring 0 (field_is_division_ring-1 nil 3292793030 ("" (skolem!) (("" (typepred "x!1") (("" (expand "field?") (("" (flatten) nil nil)) nil)) nil)) nil) ((field nonempty-type-eq-decl nil field nil) (field? const-decl "bool" field_def nil) (one formal-const-decl "T" field nil) (zero formal-const-decl "T" field nil) (* formal-const-decl "[T, T -> T]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil field nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (field_is_integral_domain 0 (field_is_integral_domain-1 nil 3293395171 ("" (skosimp) (("" (typepred "x!1") (("" (expand "field?") (("" (expand "integral_domain?") (("" (expand "commutative_ring?") (("" (expand "nz_closed?") (("" (expand "division_ring?") (("" (expand "ring_with_one?") (("" (flatten) (("" (expand "group?") (("" (hide -2) (("" (assert) (("" (hide -1 -3) (("" (expand "monoid?") (("" (expand "monad?") (("" (expand "groupoid?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((field nonempty-type-eq-decl nil field nil) (field? const-decl "bool" field_def nil) (one formal-const-decl "T" field nil) (zero formal-const-decl "T" field nil) (* formal-const-decl "[T, T -> T]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil field nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (integral_domain? const-decl "bool" integral_domain_def nil) (nz_closed? const-decl "bool" ring_nz_closed_def nil) (ring_with_one? const-decl "bool" ring_with_one_def nil) (group? const-decl "bool" group_def nil) (monoid? const-decl "bool" monoid_def nil) (monad? const-decl "bool" monad_def nil) (division_ring? const-decl "bool" division_ring_def nil) (commutative_ring? const-decl "bool" ring_def nil)) shostak)) (field_is_abelian_group_TCC1 0 (field_is_abelian_group_TCC1-1 nil 3294126540 ("" (lemma "one_ne_zero") (("" (propax) nil nil)) nil) ((one_ne_zero formula-decl nil division_ring nil) (T formal-nonempty-type-decl nil field nil) (+ formal-const-decl "[T, T -> T]" field nil) (* formal-const-decl "[T, T -> T]" field nil) (zero formal-const-decl "T" field nil) (one formal-const-decl "T" field nil)) shostak)) (field_is_abelian_group_TCC2 0 (field_is_abelian_group_TCC2-1 nil 3294126540 ("" (inst + "one") (("" (lemma "one_ne_zero") (("" (propax) nil nil)) nil)) nil) ((one formal-const-decl "T" field nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (* formal-const-decl "[T, T -> T]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (zero formal-const-decl "T" field nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil field nil) (one_ne_zero formula-decl nil division_ring nil)) shostak)) (field_is_abelian_group 0 (field_is_abelian_group-1 nil 3294124716 ("" (skosimp) (("" (typepred "F!1") (("" (expand "field?") (("" (expand "division_ring?") (("" (expand "abelian_group?") (("" (flatten) (("" (split) (("1" (hide -1 -3) (("1" (expand "group?") (("1" (expand "monoid?") (("1" (expand "monad?") (("1" (expand "groupoid?") (("1" (flatten) (("1" (expand "restrict") (("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) (("1" (rewrite "one_times") nil nil) ("2" (rewrite "times_one") nil nil) ("3" (rewrite "one_times") nil nil) ("4" (rewrite "times_one") nil nil) ("5" (typepred "F!1") (("5" (expand "field?") (("5" (expand "division_ring?") (("5" (expand "ring_with_one?") (("5" (expand "monoid?") (("5" (expand "monad?") (("5" (expand "member") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (rewrite "times_one") 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 "remove") (("5" (expand "member") (("5" (inst - "x!1") (("5" (skosimp) (("5" (typepred "y!1") (("5" (inst + "y!1") (("1" (grind) nil nil) ("2" (expand "remove") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((field nonempty-type-eq-decl nil field nil) (field? const-decl "bool" field_def nil) (one formal-const-decl "T" field nil) (zero formal-const-decl "T" field nil) (* formal-const-decl "[T, T -> T]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil field nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (division_ring? const-decl "bool" division_ring_def nil) (commutative? const-decl "bool" operator_defs nil) (monoid? const-decl "bool" monoid_def nil) (member const-decl "bool" sets nil) (remove const-decl "set" sets nil) (nz_star const-decl "[nz_T, nz_T -> nz_T]" field nil) (star_closed? const-decl "bool" groupoid_def nil) (/= const-decl "boolean" notequal nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (times_one formula-decl nil ring_with_one nil) (one_times formula-decl nil ring_with_one nil) (identity? const-decl "bool" operator_defs nil) (associative? const-decl "bool" operator_defs nil) (inv_exists? const-decl "bool" group_def nil) (F!1 skolem-const-decl "field" field nil) (y!1 skolem-const-decl "(remove(zero, F!1))" field nil) (restrict const-decl "R" restrict nil) (monad? const-decl "bool" monad_def nil) (group? const-decl "bool" group_def nil) (abelian_group? const-decl "bool" group_def nil)) shostak)) (mult_div_TCC1 0 (mult_div_TCC1-1 nil 3374415995 ("" (skosimp) (("" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "x1!1`1" "nzy" "x1!1`2")) (("" (assert) nil nil)) nil)) nil) ((zero formal-const-decl "T" field nil) (* formal-const-decl "[T, T -> T]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (T formal-nonempty-type-decl nil field nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil)) nil)) (mult_div 0 (mult_div-1 nil 3294126850 ("" (skosimp) (("" (name "Z" "inv[nz_T[T, +, *, zero], restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0z!1)") (("1" (lemma "div_mult" ("x" "x!1" "n0z" "n0z!1")) (("1" (replace -2) (("1" (lemma "times_commutative" ("x" "n0z!1" "y" "x!1*Z")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "one_ne_zero") (("2" (hide 2) (("2" (skosimp) (("2" (expand "restrict") (("2" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "x1!1`1" "nzy" "x1!1`2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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" field 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]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (zero formal-const-decl "T" field nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil field nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" field nil) (times_commutative formula-decl nil commutative_ring nil) (div_mult formula-decl nil 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)) shostak)) (times_div_right 0 (times_div_right-1 nil 3294127276 ("" (skosimp) (("" (name "Z" "inv[nz_T[T, +, *, zero], restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0z!1)") (("1" (lemma "times_div_left" ("x" "x!1" "y" "y!1" "n0z" "n0z!1")) (("1" (replace -2) (("1" (lemma "times_commutative" ("x" "Z" "y" "y!1")) (("1" (replace -1 -2 rl) (("1" (replace -2 1 rl) (("1" (rewrite "times_associative" 1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "restrict") (("2" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "x1!1`1" "nzy" "x1!1`2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) 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" field 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]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (zero formal-const-decl "T" field nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil field nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" field nil) (times_associative formula-decl nil ring nil) (times_commutative formula-decl nil commutative_ring nil) (times_div_left formula-decl nil division_ring nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil)) shostak)) (div_times_TCC1 0 (div_times_TCC1-1 nil 3294126541 ("" (skosimp) (("" (lemma "nz_T_times_nz_T_is_nz_T" ("nzx" "n0x!1" "nzy" "n0y!1")) (("" (assert) nil nil)) nil)) nil) ((zero formal-const-decl "T" field nil) (* formal-const-decl "[T, T -> T]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (T formal-nonempty-type-decl nil field nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (nz_T_times_nz_T_is_nz_T judgement-tcc nil ring_nz_closed nil)) shostak)) (div_times 0 (div_times-1 nil 3294128022 ("" (skosimp) (("" (rewrite "inv_star") (("" (lemma "times_associative") (("" (lemma "times_commutative") (("" (name "X" "inv[nz_T[T, +, *, zero], restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0x!1)") (("1" (name "Y" "inv[nz_T[T, +, *, zero], restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0y!1)") (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (inst-cp -2 "x!1" "y!1" "Y*X") (("1" (inst-cp - "Y" "X") (("1" (replace -2) (("1" (replace -4) (("1" (inst-cp - "y!1" "X" "Y") (("1" (replace -4 1 rl) (("1" (inst - "y!1" "X") (("1" (replace -1) (("1" (rewrite "times_associative" 1) (("1" (rewrite "times_associative" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "one_ne_zero") (("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "restrict") (("2" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "x1!1`1" "nzy" "x1!1`2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inv_star formula-decl nil group nil) (T formal-nonempty-type-decl nil field nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero formal-const-decl "T" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (* formal-const-decl "[T, T -> T]" field nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (restrict const-decl "R" restrict nil) (one formal-const-decl "T" field nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" field nil) (times_commutative formula-decl nil commutative_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) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (times_associative formula-decl nil ring nil)) shostak)) (cross_mult 0 (cross_mult-1 nil 3294128630 ("" (skosimp) (("" (lemma "div_mult_left" ("x" "x!1" "n0z" "n0x!1" "y" "y!1 * inv[nz_T[T, +, *, zero], restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0y!1)")) (("1" (replace -1 1) (("1" (hide -1) (("1" (rewrite "times_associative" 1) (("1" (lemma "times_commutative" ("x" "inv[nz_T[T, +, *, zero], restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0y!1)" "y" "n0x!1")) (("1" (replace -1 1) (("1" (hide -1) (("1" (rewrite "times_associative" :dir rl) (("1" (lemma "div_mult_right" ("y" "x!1" "x" "y!1*n0x!1" "n0z" "n0y!1")) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "one_ne_zero") (("2" (hide 2) (("2" (skosimp) (("2" (expand "restrict") (("2" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "x1!1`1" "nzy" "x1!1`2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((one formal-const-decl "T" field nil) (zero formal-const-decl "T" field nil) (* formal-const-decl "[T, T -> T]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (T formal-nonempty-type-decl nil field nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (restrict const-decl "R" restrict 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) (div_mult_left formula-decl nil division_ring nil) (times_commutative formula-decl nil commutative_ring nil) (div_mult_right formula-decl nil division_ring nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" field nil) (times_associative formula-decl nil 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)) shostak)) (add_div 0 (add_div-2 nil 3374416802 ("" (skosimp) (("" (rewrite "div_distributes" :dir rl) (("" (rewrite "inv_star") (("" (lemma "div_simplify" ("n0x" "n0x!1")) (("" (lemma "div_simplify" ("n0x" "n0y!1")) (("" (name-replace "X" "inv[nz_T[T, +, *, zero], restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0x!1)") (("1" (name-replace "Y" "inv[nz_T[T, +, *, zero], restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0y!1)") (("1" (lemma "times_commutative") (("1" (inst-cp - "Y" "X") (("1" (lemma "times_associative") (("1" (inst-cp - "x!1*n0y!1" "Y" "X") (("1" (inst-cp - "x!1" "n0y!1" "Y") (("1" (replace -6) (("1" (rewrite "times_one") (("1" (replace -2) (("1" (replace -3 1 rl) (("1" (replace -5) (("1" (inst-cp - "y!1*n0x!1" "X" "Y") (("1" (inst - "y!1" "n0x!1" "X") (("1" (replace -8) (("1" (rewrite "times_one") (("1" (replace -1) (("1" (replace -2 1 rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "x1!1`1" "nzy" "x1!1`2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "x1!1`1" "nzy" "x1!1`2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((div_distributes formula-decl nil division_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) (T formal-nonempty-type-decl nil field nil) (+ formal-const-decl "[T, T -> T]" field nil) (* formal-const-decl "[T, T -> T]" field nil) (zero formal-const-decl "T" field nil) (one formal-const-decl "T" field nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" field nil) (div_simplify formula-decl nil division_ring nil) (one_ne_zero formula-decl nil 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) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil) (times_commutative formula-decl nil commutative_ring nil) (times_associative formula-decl nil ring nil) (times_one formula-decl nil ring_with_one nil) (restrict const-decl "R" restrict nil) (inv_star formula-decl nil group nil)) nil) (add_div-1 nil 3294129287 ("" (skosimp) (("" (rewrite "div_distributes" :dir rl) (("" (rewrite "inv_star") (("" (lemma "div_simplify" ("n0x" "n0x!1")) (("" (lemma "div_simplify" ("n0x" "n0y!1")) (("" (name-replace "X" "inv[nz_T[T, +, *, zero], restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0x!1)") (("1" (name-replace "Y" "inv[nz_T[T, +, *, zero], restrict[[T, T], [nz_T[T, +, *, zero], nz_T[T, +, *, zero]], T] (*), one] (n0y!1)") (("1" (lemma "times_commutative") (("1" (inst-cp - "Y" "X") (("1" (lemma "times_associative") (("1" (inst-cp - "x!1*n0y!1" "Y" "X") (("1" (inst-cp - "x!1" "n0y!1" "Y") (("1" (replace -6) (("1" (rewrite "times_one") (("1" (replace -2) (("1" (replace -3 1 rl) (("1" (replace -5) (("1" (inst-cp - "y!1*n0x!1" "X" "Y") (("1" (inst - "y!1" "n0x!1" "X") (("1" (replace -8) (("1" (rewrite "times_one") (("1" (replace -1) (("1" (replace -2 1 rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "one_ne_zero") (("2" (propax) nil nil)) nil) ("3" (hide-all-but 1) (("3" (grind) (("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) ("2" (lemma "one_ne_zero") (("2" (propax) nil nil)) nil) ("3" (hide-all-but 1) (("3" (grind) (("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)) nil)) nil)) nil) ((div_distributes formula-decl nil division_ring nil) (nz_T type-eq-decl nil ring_nz_closed_def nil) (div_simplify formula-decl nil division_ring nil) (inv const-decl "{y | x * y = one AND y * x = one}" group 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) (times_commutative formula-decl nil commutative_ring nil) (times_associative formula-decl nil ring nil) (times_one formula-decl nil ring_with_one nil) (inv_star formula-decl nil group nil)) shostak)) (minus_div1 0 (minus_div1-1 nil 3294127633 ("" (skosimp) (("" (lemma "add_div" ("x" "x!1" "n0x" "n0x!1" "y" "-y!1" "n0y" "n0y!1")) (("" (rewrite "negative_times") (("1" (rewrite "negative_times") nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "x1!1`1" "nzy" "x1!1`2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) 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) (nz_T type-eq-decl nil ring_nz_closed_def nil) (* formal-const-decl "[T, T -> T]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (zero formal-const-decl "T" field nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil field nil) (add_div formula-decl nil field 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]" field nil) (restrict const-decl "R" restrict nil) (negative_times formula-decl nil ring nil) (one_ne_zero formula-decl nil division_ring nil) (one formal-const-decl "T" field nil)) shostak)) (sq_div 0 (sq_div-1 nil 3297003448 ("" (skosimp*) (("" (rewrite "sq_times") (("1" (expand "sq") (("1" (assert) (("1" (rewrite "inv_star") nil nil)) nil)) nil) ("2" (lemma "one_ne_zero") (("2" (hide 2) (("2" (skosimp) (("2" (typepred "x1!1`1") (("2" (typepred "x1!1`2") (("2" (lemma "nz_T_times_nz_T_is_not_zero" ("nzx" "x1!1`1" "nzy" "x1!1`2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((one formal-const-decl "T" field nil) (zero formal-const-decl "T" field nil) (* formal-const-decl "[T, T -> T]" field nil) (+ formal-const-decl "[T, T -> T]" field nil) (T formal-nonempty-type-decl nil field nil) (one_ne_zero formula-decl nil division_ring nil) (sq_times formula-decl nil commutative_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) (restrict const-decl "R" restrict nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (negate_nz_T_is_nz_T application-judgement "nz_T[T, +, *, zero]" field nil) (sq_nz_is_nz application-judgement "nz_T[T, +, *, zero]" field nil) (inv_star formula-decl nil group nil) (sq const-decl "T" ring nil) (NOT const-decl "[bool -> bool]" booleans nil) (nz_T_times_nz_T_is_not_zero formula-decl nil ring_nz_closed nil)) shostak))) ¤ Dauer der Verarbeitung: 0.23 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 |
