| products/sources/formale sprachen/PVS/complex/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: number_fields_bis.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(number_fields_bis
(number_fields_left_identity_add 0 (number_fields_left_identity_add-1 nil 3294676177 ("" (grind) nil nil) nil shostak)) (number_fields_right_identity_add 0 (number_fields_right_identity_add-1 nil 3294676190 ("" (grind) nil nil) nil shostak)) (number_fields_left_identity_mult 0 (number_fields_left_identity_mult-1 nil 3294676195 ("" (skosimp) (("" (rewrite "identity_mult") nil nil)) nil) ((identity_mult formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil)) shostak)) (number_fields_right_identity_mult 0 (number_fields_right_identity_mult-1 nil 3294676212 ("" (skosimp) (("" (lemma "commutative_mult" ("x" "x!1" "y" "1")) (("" (rewrite "identity_mult") nil nil)) nil)) nil) ((number_field nonempty-type-from-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (commutative_mult formula-decl nil number_fields nil) (identity_mult formula-decl nil number_fields nil)) shostak)) (number_fields_negate_is_left_inverse 0 (number_fields_negate_is_left_inverse-1 nil 3294676243 ("" (skosimp) (("" (lemma "commutative_add" ("x" "-x!1" "y" "x!1")) (("" (rewrite "inverse_add") nil nil)) nil)) nil) ((number_field nonempty-type-from-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (commutative_add formula-decl nil number_fields nil) (inverse_add formula-decl nil number_fields nil)) shostak)) (number_fields_negate_is_right_inverse 0 (number_fields_negate_is_right_inverse-1 nil 3294676289 ("" (skosimp) (("" (rewrite "inverse_add") nil nil)) nil) ((inverse_add formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil)) shostak)) (both_sides_plus1 0 (both_sides_plus1-1 nil 3280126152 ("" (grind) nil nil) nil shostak)) (both_sides_plus2 0 (both_sides_plus2-1 nil 3280126162 ("" (grind) nil nil) nil shostak)) (both_sides_minus1 0 (both_sides_minus1-1 nil 3280126168 ("" (grind) nil nil) nil shostak)) (both_sides_minus2 0 (both_sides_minus2-1 nil 3280126174 ("" (skosimp*) (("" (split) (("1" (flatten) (("1" (rewrite "minus_add") (("1" (rewrite "minus_add") (("1" (lemma "both_sides_plus1" ("x" "-x!1" "y" "-y!1" "z" "z!1")) (("1" (assert) (("1" (hide -1) (("1" (lemma "inverse_add" ("x" "x!1")) (("1" (lemma "both_sides_plus2" ("x" "-x!1" "y" "-y!1" "z" "x!1")) (("1" (replace -2 -1) (("1" (grind) (("1" (lemma "both_sides_plus2" ("z" "y!1" "x" "0" "y" "-y!1+x!1")) (("1" (rewrite "identity_add" -1) (("1" (lemma "associative_add" ("x" "y!1" "y" "-y!1" "z" "x!1")) (("1" (rewrite "inverse_add" -1) (("1" (rewrite "identity_add" -1) (("1" (replace -1 -2) (("1" (hide -1 -4) (("1" (lemma "commutative_add" ("x" "0" "y" "x!1")) (("1" (lemma "identity_add" ("x" "x!1")) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil) ((minus_add formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (both_sides_plus1 formula-decl nil number_fields_bis nil) (both_sides_plus2 formula-decl nil number_fields_bis nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (identity_add formula-decl nil number_fields nil) (commutative_add formula-decl nil number_fields nil) (associative_add formula-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (inverse_add formula-decl nil number_fields nil)) shostak)) (number_fields_negate_negate 0 (number_fields_negate_negate-1 nil 3294676300 ("" (skosimp) (("" (lemma "both_sides_plus1" ("z" "-x!1" "x" "-(-x!1)" "y" "x!1")) (("" (rewrite "inverse_add" -1) (("" (lemma "commutative_add" ("x" "-(-x!1)" "y" "-x!1")) (("" (rewrite "inverse_add" -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (both_sides_plus1 formula-decl nil number_fields_bis nil) (commutative_add formula-decl nil number_fields nil) (inverse_add formula-decl nil number_fields nil)) shostak)) (zero_times1 0 (zero_times1-1 nil 3280124273 ("" (skosimp*) (("" (lemma "inverse_add" ("x" "x!1")) (("" (lemma "distributive" ("x" "0" "y" "x!1" "z" "-x!1")) (("" (grind) nil nil)) nil)) nil)) nil) ((number_field nonempty-type-from-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (inverse_add formula-decl nil number_fields nil) (distributive formula-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil)) shostak)) (zero_times2 0 (zero_times2-1 nil 3280124509 ("" (skosimp*) (("" (rewrite "commutative_mult") (("" (rewrite "zero_times1") nil nil)) nil)) nil) ((commutative_mult formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (zero_times1 formula-decl nil number_fields_bis nil)) shostak)) (nznum_times_nznum_is_nznum 0 (nznum_times_nznum_is_nznum-1 nil 3280139881 ("" (skosimp*) (("" (typepred "nzx!1") (("" (typepred "nzy!1") (("" (hide -1 -3) (("" (case "FORALL (x:nznum, y:numfield): x*y = 0 => y = 0") (("1" (inst - "nzx!1" "nzy!1") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (hide -1) (("2" (lemma "inverse_mult" ("n0x" "x!1")) (("2" (case "FORALL (x,y,z:numfield): x=y => x*z = y*z") (("1" (inst - "x!1 * (1 / x!1)" "1" "y!1") (("1" (split -1) (("1" (rewrite "identity_mult" -1) (("1" (hide -2) (("1" (lemma "associative_mult") (("1" (inst-cp - "x!1" "1/x!1" "y!1") (("1" (lemma "commutative_mult" ("x" "1/x!1" "y" "y!1")) (("1" (replace -1 -3) (("1" (inst - "x!1" "y!1" "1/x!1") (("1" (replace -4) (("1" (replace -3 -2) (("1" (replace -6 -2) (("1" (rewrite "zero_times1" -2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (inverse_mult formula-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (identity_mult formula-decl nil number_fields nil) (associative_mult formula-decl nil number_fields nil) (commutative_mult formula-decl nil number_fields nil) (zero_times1 formula-decl nil number_fields_bis nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (minus_nznum_is_nznum 0 (minus_nznum_is_nznum-1 nil 3280140087 ("" (skosimp*) (("" (typepred "nzx!1") (("" (lemma "inverse_add" ("x" "nzx!1")) (("" (replace -4) (("" (rewrite "identity_add" -1) (("" (replace -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (identity_add formula-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (inverse_add formula-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil)) shostak)) (zero_times3 0 (zero_times3-1 nil 3280133331 ("" (skosimp*) (("" (case-replace "x!1=0") (("1" (rewrite "zero_times1") (("1" (assert) nil nil)) nil) ("2" (case-replace "y!1=0") (("1" (rewrite "zero_times2") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (lemma "nznum_times_nznum_is_nznum" ("nzx" "x!1" "nzy" "y!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (zero_times1 formula-decl nil number_fields_bis nil) (nznum_times_nznum_is_nznum judgement-tcc nil number_fields_bis nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (zero_times2 formula-decl nil number_fields_bis nil)) shostak)) (neg_times_neg 0 (neg_times_neg-1 nil 3280141326 ("" (skosimp*) (("" (lemma "inverse_add" ("x" "y!1")) (("" (lemma "distributive" ("x" "x!1" "y" "y!1" "z" "-y!1")) (("" (replace -2 -1) (("" (rewrite "zero_times2" -1) (("" (lemma "both_sides_minus1" ("x" "0" "y" "(x!1 * y!1) + (x!1 * -y!1)" "z" "x!1 * -y!1")) (("" (assert) (("" (lemma "associative_mult" ("x" "-1" "y" "x!1" "z" "-y!1")) (("" (case-replace "-1*x!1=-x!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (lemma "both_sides_plus2" ("z" "x!1" "x" "-1*x!1" "y" "-x!1")) (("2" (rewrite "inverse_add" -1) (("2" (lemma "inverse_add" ("x" "1")) (("2" (lemma "zero_times1" ("x" "x!1")) (("2" (lemma "distributive" ("x" "x!1" "y" "1" "z" "-1")) (("2" (lemma "commutative_mult") (("2" (inst-cp - "x!1" "1+ -1") (("2" (replace -2 -3) (("2" (replace -5) (("2" (replace -4) (("2" (inst-cp - "x!1" "1") (("2" (rewrite "identity_mult" -2) (("2" (replace -2) (("2" (inst - "x!1" "-1") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number_field nonempty-type-from-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (inverse_add formula-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_minus1 formula-decl nil number_fields_bis nil) (associative_mult formula-decl nil number_fields nil) (both_sides_plus2 formula-decl nil number_fields_bis nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (identity_mult formula-decl nil number_fields nil) (commutative_mult formula-decl nil number_fields nil) (zero_times1 formula-decl nil number_fields_bis nil) (minus_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (= const-decl "[T, T -> boolean]" equalities nil) (zero_times2 formula-decl nil number_fields_bis nil) (distributive formula-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil)) shostak)) (zero_is_neg_zero 0 (zero_is_neg_zero-1 nil 3280127050 ("" (grind) nil nil) ((minus_even_is_even application-judgement "even_int" integers nil)) shostak)) (both_sides_times1 0 (both_sides_times1-1 nil 3280127668 ("" (skosimp*) (("" (split) (("1" (flatten) (("1" (lemma "both_sides_minus1" ("x" "x!1*n0z!1" "y" "y!1*n0z!1" "z" "y!1 * n0z!1")) (("1" (lemma "inverse_add" ("x" "y!1 * n0z!1")) (("1" (lemma "minus_add" ("x" "y!1 * n0z!1" "y" "y!1 * n0z!1")) (("1" (replace -1 -2 rl) (("1" (replace -2 -3) (("1" (hide -1 -2) (("1" (assert) (("1" (hide -2) (("1" (case-replace "x!1 * n0z!1 - y!1 * n0z!1 = n0z!1*(x!1-y!1)") (("1" (lemma "zero_times3" ("x" "n0z!1" "y" "x!1-y!1")) (("1" (replace -3 -1) (("1" (hide -2 -3) (("1" (flatten -1) (("1" (typepred "n0z!1") (("1" (split -3) (("1" (assert) nil nil) ("2" (hide -2 -3) (("2" (lemma "both_sides_plus1" ("x" "x!1-y!1" "y" "0" "z" "y!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (rewrite "minus_add") (("2" (rewrite "minus_add") (("2" (rewrite "distributive" 1) (("2" (lemma "commutative_mult" ("x" "x!1" "y" "n0z!1")) (("2" (replace -1) (("2" (assert) (("2" (hide -1) (("2" (lemma "inverse_add" ("x" "y!1")) (("2" (lemma "distributive" ("x" "n0z!1" "y" "y!1" "z" "-y!1")) (("2" (replace -2) (("2" (rewrite "zero_times2" -1) (("2" (rewrite "commutative_mult" -1) (("2" (lemma "both_sides_plus2" ("z" "-(y!1 * n0z!1)" "x" "0" "y" "y!1 * n0z!1 + (n0z!1 * -y!1)")) (("2" (lemma "identity_add" ("x" "-(y!1*n0z!1)")) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "inverse_add" ("x" "y!1*n0z!1")) (("2" (case-replace "-(y!1 * n0z!1) + (y!1 * n0z!1 + (n0z!1 * -y!1)) = (n0z!1 * -y!1)") (("1" (assert) nil nil) ("2" (hide 2 -2) (("2" (lemma "associative_add" ("x" "-(y!1 * n0z!1)" "y" "y!1 * n0z!1" "z" "n0z!1 * -y!1")) (("2" (lemma "commutative_add" ("x" "y!1 * n0z!1" "y" "-(y!1 * n0z!1)")) (("2" (replace -1 -2 :dir rl) (("2" (replace -2 1) (("2" (replace -3 1) (("2" (rewrite "commutative_add" 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil) ((nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (both_sides_minus1 formula-decl nil number_fields_bis nil) (minus_add formula-decl nil number_fields nil) (minus_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (both_sides_plus1 formula-decl nil number_fields_bis nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (zero_times3 formula-decl nil number_fields_bis nil) (- const-decl "[numfield -> numfield]" number_fields nil) (distributive formula-decl nil number_fields nil) (zero_times2 formula-decl nil number_fields_bis nil) (both_sides_plus2 formula-decl nil number_fields_bis nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (commutative_add formula-decl nil number_fields nil) (associative_add formula-decl nil number_fields nil) (identity_add formula-decl nil number_fields nil) (commutative_mult formula-decl nil number_fields nil) (inverse_add formula-decl nil number_fields nil)) shostak)) (both_sides_times2 0 (both_sides_times2-1 nil 3280128353 ("" (skosimp*) (("" (rewrite "commutative_mult") (("" (lemma "commutative_mult" ("x" "n0z!1" "y" "y!1")) (("" (replace -1) (("" (lemma "both_sides_times1" ("x" "x!1" "y" "y!1" "n0z" "n0z!1")) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((commutative_mult formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (both_sides_times1 formula-decl nil number_fields_bis nil)) shostak)) (inv_ne_0 0 (inv_ne_0-1 nil 3280127243 ("" (skosimp*) (("" (lemma "inverse_mult" ("n0x" "n0x!1")) (("" (typepred "n0x!1") (("" (replace -4) (("" (lemma "zero_times2" ("x" "n0x!1")) (("" (replace -1 -4) (("" (hide-all-but -4) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (inverse_mult formula-decl nil number_fields nil) (zero_times2 formula-decl nil number_fields_bis nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (nznum_div_nznum_is_nznum 0 (nznum_div_nznum_is_nznum-1 nil 3280140171 ("" (skosimp*) (("" (rewrite "div_def") (("" (lemma "inv_ne_0" ("n0x" "nzy!1")) (("" (lemma "nznum_times_nznum_is_nznum" ("nzx" "nzx!1" "nzy" "1/nzy!1")) (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((div_def formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum_times_nznum_is_nznum judgement-tcc nil number_fields_bis nil) (inv_ne_0 formula-decl nil number_fields_bis nil)) shostak)) (both_sides_div1 0 (both_sides_div1-1 nil 3280130887 ("" (skosimp*) (("" (lemma "div_def" ("y" "x!1" "n0x" "n0z!1")) (("" (lemma "div_def" ("y" "y!1" "n0x" "n0z!1")) (("" (replace -1) (("" (replace -2) (("" (lemma "both_sides_times1" ("x" "x!1" "y" "y!1" "n0z" "1/n0z!1")) (("1" (propax) nil nil) ("2" (rewrite "inv_ne_0" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_def formula-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (both_sides_times1 formula-decl nil number_fields_bis nil) (nznum_div_nznum_is_nznum application-judgement "nznum" number_fields_bis nil)) shostak)) (both_sides_div2 0 (both_sides_div2-1 nil 3280142404 ("" (skosimp*) (("" (rewrite "div_def") (("" (lemma "div_def" ("y" "n0z!1" "n0x" "n0y!1")) (("" (replace -1 1) (("" (lemma "both_sides_times2" ("n0z" "n0z!1" "x" "1/n0x!1" "y" "1/n0y!1")) (("" (replace -1 1) (("" (hide -1 -2) (("" (split) (("1" (flatten) (("1" (lemma "both_sides_times2" ("n0z" "n0x!1" "x" "1 / n0x!1" "y" "1 / n0y!1")) (("1" (rewrite "inverse_mult" -1) (("1" (assert) (("1" (hide -2) (("1" (lemma "both_sides_times1" ("n0z" "n0y!1" "x" "1" "y" "n0x!1 * (1 / n0y!1)")) (("1" (rewrite "identity_mult" -1) (("1" (assert) (("1" (replace -1 1) (("1" (hide -1 -2) (("1" (lemma "identity_mult" ("x" "n0x!1")) (("1" (lemma "inverse_mult" ("n0x" "n0y!1")) (("1" (lemma "commutative_mult") (("1" (inst-cp - "1 / n0y!1" "n0x!1") (("1" (replace -2 1) (("1" (lemma "associative_mult" ("x" "n0x!1" "y" "1/n0y!1" "z" "n0y!1")) (("1" (replace -1 1 rl) (("1" (hide -1 -3) (("1" (inst-cp - "1 / n0y!1" "n0y!1") (("1" (replace -3 -2) (("1" (replace -2) (("1" (inst - "1" "n0x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((div_def formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum_div_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (nznum_times_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (both_sides_times1 formula-decl nil number_fields_bis nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (associative_mult formula-decl nil number_fields nil) (commutative_mult formula-decl nil number_fields nil) (identity_mult formula-decl nil number_fields nil) (inverse_mult formula-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (both_sides_times2 formula-decl nil number_fields_bis nil)) shostak)) (times_plus 0 (times_plus-1 nil 3280126622 ("" (skosimp*) (("" (lemma "distributive" ("x" "x!1+y!1" "y" "z!1" "z" "w!1")) (("" (replace -1 1) (("" (rewrite "commutative_mult" 1) (("" (lemma "commutative_mult" ("x" "x!1+y!1" "y" "w!1")) (("" (replace -1 1) (("" (assert) (("" (rewrite "commutative_mult" 1) (("" (assert) (("" (rewrite "commutative_mult" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number_field nonempty-type-from-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (distributive formula-decl nil number_fields nil) (commutative_mult formula-decl nil number_fields nil)) shostak)) (times_div1 0 (times_div1-1 nil 3280129158 ("" (skosimp*) (("" (rewrite "div_def") (("" (lemma "div_def" ("y" "x!1*y!1" "n0x" "n0z!1")) (("" (replace -1) (("" (rewrite "associative_mult" 1) nil nil)) nil)) nil)) nil)) nil) ((div_def formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum_div_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (associative_mult formula-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (times_div2 0 (times_div2-1 nil 3280129233 ("" (skosimp*) (("" (rewrite "commutative_mult") (("" (rewrite "times_div1") (("" (rewrite "commutative_mult") nil nil)) nil)) nil)) nil) ((commutative_mult formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (times_div1 formula-decl nil number_fields_bis nil)) shostak)) (div_eq_zero 0 (div_eq_zero-1 nil 3280134605 ("" (skosimp*) (("" (rewrite "div_def") (("" (lemma "inv_ne_0" ("n0x" "n0z!1")) (("" (lemma "zero_times3" ("x" "x!1" "y" "1/n0z!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((div_def formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum_div_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (zero_times3 formula-decl nil number_fields_bis nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (inv_ne_0 formula-decl nil number_fields_bis nil)) shostak)) (div_simp 0 (div_simp-1 nil 3280126859 ("" (skosimp*) (("" (rewrite "div_def") (("" (rewrite "inverse_mult") nil nil)) nil)) nil) ((div_def formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum_div_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (nznum_times_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (inverse_mult formula-decl nil number_fields nil)) shostak)) (div_cancel1 0 (div_cancel1-1 nil 3280135297 ("" (skosimp*) (("" (rewrite "div_def") (("" (lemma "inverse_mult" ("n0x" "n0z!1")) (("" (case-replace "x!1=0") (("1" (rewrite "zero_times1") (("1" (rewrite "zero_times2") nil nil)) nil) ("2" (lemma "both_sides_times1" ("n0z" "x!1" "x" "n0z!1 * (1 / n0z!1)" "y" "1")) (("1" (rewrite "identity_mult" -1) (("1" (lemma "associative_mult" ("x" "n0z!1" "y" "1/n0z!1" "z" "x!1")) (("1" (lemma "commutative_mult" ("x" "1/n0z!1" "y" "x!1")) (("1" (replace -1 -2) (("1" (replace -2 2) (("1" (replace -3 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((div_def formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum_div_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (= const-decl "[T, T -> boolean]" equalities nil) (zero_times2 formula-decl nil number_fields_bis nil) (zero_times1 formula-decl nil number_fields_bis nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (identity_mult formula-decl nil number_fields nil) (nznum_times_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (commutative_mult formula-decl nil number_fields nil) (associative_mult formula-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times1 formula-decl nil number_fields_bis nil) (inverse_mult formula-decl nil number_fields nil)) shostak)) (div_cancel2 0 (div_cancel2-1 nil 3280134780 ("" (skosimp*) (("" (rewrite "commutative_mult") (("" (rewrite "div_cancel1") nil nil)) nil)) nil) ((commutative_mult formula-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (div_cancel1 formula-decl nil number_fields_bis nil)) shostak)) (div_cancel3 0 (div_cancel3-1 nil 3280142714 ("" (skosimp*) (("" (lemma "div_cancel1" ("n0z" "n0z!1" "x" "x!1")) (("" (lemma "both_sides_times2" ("n0z" "n0z!1" "x" "x!1 / n0z!1" "y" "y!1")) (("" (replace -2 -1) (("" (rewrite "commutative_mult" -1) (("" (replace -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_cancel1 formula-decl nil number_fields_bis nil) (commutative_mult formula-decl nil number_fields nil) (both_sides_times2 formula-decl nil number_fields_bis nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)) shostak)) (div_cancel4 0 (div_cancel4-1 nil 3280134879 ("" (skosimp*) (("" (lemma "div_cancel3" ("x" "x!1" "y" "y!1" "n0z" "n0z!1")) (("" (split) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_cancel3 formula-decl nil number_fields_bis nil)) shostak)) (cross_mult 0 (cross_mult-1 nil 3280134974 ("" (skosimp*) (("" (lemma "div_cancel3" ("x" "x!1" "n0z" "n0x!1" "y" "y!1/n0y!1")) (("" (rewrite "times_div2" -1) (("" (lemma "div_cancel4" ("y" "x!1" "x" "y!1*n0x!1" "n0z" "n0y!1")) (("" (replace -2 1) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_cancel3 formula-decl nil number_fields_bis nil) (div_cancel4 formula-decl nil number_fields_bis nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (times_div2 formula-decl nil number_fields_bis nil)) shostak)) (div_times 0 (div_times-1 nil 3280136949 ("" (skosimp*) (("" (lemma "times_div1" ("x" "x!1/n0x!1" "y" "y!1" "n0z" "n0y!1")) (("" (replace -1 1) (("" (hide -1) (("" (lemma "cross_mult" ("x" "x!1 / n0x!1 * y!1" "n0x" "n0y!1" "y" "x!1 * y!1" "n0y" "n0x!1 * n0y!1")) (("" (replace -1 1) (("" (hide -1) (("" (rewrite "associative_mult") (("" (rewrite "div_cancel2" 1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (times_div1 formula-decl nil number_fields_bis nil) (associative_mult formula-decl nil number_fields nil) (div_cancel2 formula-decl nil number_fields_bis nil) (nznum_times_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (cross_mult formula-decl nil number_fields_bis nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (add_div 0 (add_div-1 nil 3280145209 ("" (skosimp*) (("" (lemma "div_cancel4" ("y" "(x!1 / n0x!1) + (y!1 / n0y!1)" "x" "x!1 * n0y!1 + y!1 * n0x!1" "n0z" "n0x!1 * n0y!1")) (("" (replace -1 1) (("" (hide -1) (("" (lemma "commutative_mult") (("" (inst-cp - "(x!1 / n0x!1) + (y!1 / n0y!1)" "n0x!1 * n0y!1") (("" (replace -2 1) (("" (lemma "distributive" ("x" "n0x!1*n0y!1" "y" "x!1 / n0x!1" "z" "y!1 / n0y!1")) (("" (replace -1 1) (("" (hide -1 -3) (("" (inst-cp - "n0x!1" "n0y!1") (("" (lemma "associative_mult") (("" (inst-cp - "n0y!1" "n0x!1" "x!1 / n0x!1") (("" (replace -4 -2 rl) (("" (lemma "div_cancel1") (("" (inst-cp - "n0x!1" "x!1") (("" (replace -2 -4) (("" (replace -4 1 rl) (("" (hide -2 -4 -6) (("" (inst - "n0y!1" "y!1") (("" (inst - "n0x!1" "n0y!1" "y!1/n0y!1") (("" (replace -1 -2) (("" (replace -2 1 rl) (("" (hide -1 -2) (("" (inst-cp - "n0y!1" "x!1") (("" (inst - "n0x!1" "y!1") (("" (replace -1 1) (("" (replace -2 1) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_cancel4 formula-decl nil number_fields_bis nil) (nznum_times_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (distributive formula-decl nil number_fields nil) (associative_mult formula-decl nil number_fields nil) (div_cancel1 formula-decl nil number_fields_bis nil) (commutative_mult formula-decl nil number_fields nil)) shostak)) (minus_div1 0 (minus_div1-1 nil 3280143033 ("" (skosimp*) (("" (lemma "add_div" ("x" "x!1" "y" "-y!1" "n0x" "n0x!1" "n0y" "n0y!1")) (("" (case "FORALL (x,y:numfield): (-x*y) = -(x*y)") (("1" (inst-cp - "y!1" "n0x!1") (("1" (replace -2 -3) (("1" (lemma "minus_add" ("x" "x!1*n0y!1" "y" "y!1*n0x!1")) (("1" (replace -1 -4 rl) (("1" (replace -4 1 rl) (("1" (hide -4 -1 -3) (("1" (rewrite "minus_add" 1) (("1" (assert) (("1" (rewrite "div_def") (("1" (lemma "div_def" ("y" "-y!1" "n0x" "n0y!1")) (("1" (replace -1 1) (("1" (inst - "y!1" "1/n0y!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "both_sides_plus2" ("z" "x!2*y!2" "x" "(-x!2 * y!2)" "y" "-(x!2 * y!2)")) (("2" (replace -1 1 rl) (("2" (rewrite "inverse_add" 1) (("2" (hide -1) (("2" (lemma "inverse_add" ("x" "x!2")) (("2" (lemma "distributive" ("x" "y!2" "y" "x!2" "z" "-x!2")) (("2" (replace -2) (("2" (rewrite "zero_times2" -1) (("2" (hide -2) (("2" (lemma "commutative_mult") (("2" (inst-cp - "y!2" "x!2") (("2" (replace -2) (("2" (inst - "y!2" "-x!2") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.51 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 |
