Quelle number_fields_bis.prf
Sprache: Lisp
(number_fields_bisnil 3294676177"" (grind) nil nil ) nil shostak))nil 3294676190"" (grind) nil nil ) nil shostak))nil 3294676195"" (skosimp) (("" (rewrite "identity_mult" ) nil nil )) nil )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )nil number_fields nil ))nil 3294676212"" (skosimp)"" (lemma "commutative_mult" ("x" "x!1" "y" "1" ))"" (rewrite "identity_mult" ) nil nil )) nil ))nil )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields nil )nil number_fields nil ))nil 3294676243"" (skosimp)"" (lemma "commutative_add" ("x" "-x!1" "y" "x!1" ))"" (rewrite "inverse_add" ) nil nil )) nil ))nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields nil )nil number_fields nil ))nil 3294676289"" (skosimp) (("" (rewrite "inverse_add" ) nil nil )) nil )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )nil number_fields nil ))nil 3280126152 ("" (grind) nil nil ) nil shostak))nil 3280126162 ("" (grind) nil nil ) nil shostak))nil 3280126168 ("" (grind) nil nil ) nil nil 3280126174"" (skosimp*)"" (split)"1" (flatten)"1" (rewrite "minus_add" )"1" (rewrite "minus_add" )"1" "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" "both_sides_plus2" "x" "-x!1" "y" "-y!1" "z" "x!1" ))"1" (replace -2 -1)"1" (grind)"1" "both_sides_plus2" "z" "y!1" "x" "0" "y" "-y!1+x!1" ))"1" (rewrite "identity_add" -1)"1" "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" "1" "commutative_add" "x" "0" "y" "x!1" ))"1" "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 )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )nil number_fields nil )"odd_int" integers nil )"[numfield -> numfield]" number_fields nil )nil number_fields_bis nil )nil number_fields_bis nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil ))nil 3294676300"" (skosimp)"" "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 )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil )nil number_fields nil )nil number_fields nil ))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 )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil ))nil 3280124509"" (skosimp*)"" (rewrite "commutative_mult" )"" (rewrite "zero_times1" ) nil nil )) nil ))nil )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )nil number_fields nil )nil number_fields_bis nil ))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" "1" "associative_mult" )"1" "x!1" "1/x!1" "y!1" )"1" "commutative_mult" "x" "1/x!1" "y" "y!1" ))"1" replace -1 -3)"1" "x!1" "y!1" "1/x!1" )"1" replace -4)"1" replace -3 -2)"1" replace -6 -2)"1" rewrite "zero_times1" 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 )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil number_fields nil )nil number_fields_bis nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fieldsnil ))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 )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil ))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" "nznum_times_nznum_is_nznum" "nzx" "x!1" "nzy" "y!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )nil number_fields_bis nil )nil number_fields_bisnil )"boolean" notequal nil )nil number_fields nil )nil number_fields_bis nil ))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)"" "both_sides_minus1" "x" "0" "y" "(x!1 * y!1) + (x!1 * -y!1)" "z" "x!1 * -y!1" ))"" (assert )"" "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" "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" "zero_times1" ("x" "x!1" ))"2" "distributive" "x" "x!1" "y" "1" "z" "-1" ))"2" "commutative_mult" )"2" "x!1" "1+ -1" )"2" replace -2 -3)"2" replace -5)"2" replace -4)"2" "x!1" "1" )"2" rewrite "identity_mult" "2" replace -2)"2" "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 )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields_bis nil )nil number_fields nil )nil number_fields_bis nil )"even_int" integersnil )nil number_fields nil )nil number_fields nil )nil number_fields_bis nil )"nznum" nil )"[T, T -> boolean]" equalities nil )nil number_fields_bis nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil ))nil 3280127050 ("" (grind) nil nil )"even_int" integers nil ))nil 3280127668"" (skosimp*)"" (split)"1" (flatten)"1" "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" "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" "x!1 * n0z!1 - y!1 * n0z!1 = n0z!1*(x!1-y!1)" )"1" "zero_times3" "x" "n0z!1" "y" "x!1-y!1" ))"1" (replace -3 -1)"1" "1" "1" "n0z!1" )"1" "1" (assert ) nil nil )"2" "2" "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" "commutative_mult" "x" "x!1" "y" "n0z!1" ))"2" replace -1)"2" assert )"2" "2" "inverse_add" "x" "y!1" ))"2" "distributive" "x" "n0z!1" "y" "y!1" "z" "-y!1" ))"2" replace -2)"2" rewrite "zero_times2" "2" rewrite "commutative_mult" "2" "both_sides_plus2" "z" "-(y!1 * n0z!1)" "x" "0" "y" "y!1 * n0z!1 + (n0z!1 * -y!1)" ))"2" "identity_add" "x" "-(y!1*n0z!1)" ))"2" replace -1)"2" "2" "inverse_add" "x" "y!1*n0z!1" ))"2" "-(y!1 * n0z!1) + (y!1 * n0z!1 + (n0z!1 * -y!1)) = (n0z!1 * -y!1)" )"1" assert )nil nil )"2" "2" "associative_add" "x" "-(y!1 * n0z!1)" "y" "y!1 * n0z!1" "z" "n0z!1 * -y!1" ))"2" "commutative_add" "x" "y!1 * n0z!1" "y" "-(y!1 * n0z!1)" ))"2" replace "2" replace "2" replace "2" rewrite "commutative_add" 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 )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil )nil number_fields nil )"nznum" nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil number_fields_bis nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil number_fields_bis nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields_bis nil )nil number_fields_bis nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil number_fields nil )nil number_fields nil )nil number_fields nil ))nil 3280128353"" (skosimp*)"" (rewrite "commutative_mult" )"" (lemma "commutative_mult" ("x" "n0z!1" "y" "y!1" ))"" (replace -1)"" "both_sides_times1" "x" "x!1" "y" "y!1" "n0z" "n0z!1" ))"" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil number_fields_bis nil ))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 )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields nil )nil number_fields_bis nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3280140171"" (skosimp*)"" (rewrite "div_def" )"" (lemma "inv_ne_0" ("n0x" "nzy!1" ))"" "nznum_times_nznum_is_nznum" "nzx" "nzx!1" "nzy" "1/nzy!1" ))"1" (assert ) nil nil ) ("2" (propax) nil nil )) nil ))nil ))nil ))nil )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields_bisnil )nil number_fields_bis nil ))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)"" "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 )nil number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields_bis nil )"nznum" nil ))nil 3280142404"" (skosimp*)"" (rewrite "div_def" )"" (lemma "div_def" ("y" "n0z!1" "n0x" "n0y!1" ))"" (replace -1 1)"" "both_sides_times2" "n0z" "n0z!1" "x" "1/n0x!1" "y" "1/n0y!1" ))"" (replace -1 1)"" (hide -1 -2)"" (split)"1" (flatten)"1" "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" "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" "1" "identity_mult" "x" "n0x!1" ))"1" "inverse_mult" "n0x" "n0y!1" ))"1" "commutative_mult" )"1" "1 / n0y!1" "n0x!1" )"1" replace -2 1)"1" "associative_mult" "x" "n0x!1" "y" "1/n0y!1" "z" "n0y!1" ))"1" replace -1 1 rl)"1" "1" "1 / n0y!1" "n0y!1" )"1" replace "1" replace "1" "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 )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil number_fields nil )"nznum" nil )"nznum" nil )nil number_fields_bis nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields_bis nil ))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 )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields nil )nil number_fields nil ))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 )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil number_fields nil )"nznum" nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3280129233"" (skosimp*)"" (rewrite "commutative_mult" )"" (rewrite "times_div1" )"" (rewrite "commutative_mult" ) nil nil )) nil ))nil ))nil )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields_bis nil ))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 )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil number_fields nil )"nznum" nil )nil number_fields_bis nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields_bis nil ))nil 3280126859"" (skosimp*)"" (rewrite "div_def" ) (("" (rewrite "inverse_mult" ) nil nil ))nil ))nil )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil number_fields nil )"nznum" nil )"nznum" nil )nil number_fields nil ))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" "both_sides_times1" "n0z" "x!1" "x" "n0z!1 * (1 / n0z!1)" "y" "1" ))"1" (rewrite "identity_mult" -1)"1" "associative_mult" "x" "n0z!1" "y" "1/n0z!1" "z" "x!1" ))"1" "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 )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil number_fields nil )"nznum" nil )"[T, T -> boolean]" equalities nil )nil number_fields_bis nil )nil number_fields_bis nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"nznum" nil )nil number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields_bis nil )nil number_fields nil ))nil 3280134780"" (skosimp*)"" (rewrite "commutative_mult" )"" (rewrite "div_cancel1" ) nil nil )) nil ))nil )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields_bis nil ))nil 3280142714"" (skosimp*)"" (lemma "div_cancel1" ("n0z" "n0z!1" "x" "x!1" ))"" "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 )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil )nil number_fields nil )nil number_fields_bis nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil ))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 )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil ))nil 3280134974"" (skosimp*)"" "div_cancel3" ("x" "x!1" "n0z" "n0x!1" "y" "y!1/n0y!1" ))"" (rewrite "times_div2" -1)"" "div_cancel4" "y" "x!1" "x" "y!1*n0x!1" "n0z" "n0y!1" ))"" (replace -2 1) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil )nil number_fields_bis nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields_bis nil ))nil 3280136949"" (skosimp*)"" (lemma "times_div1" ("x" "x!1/n0x!1" "y" "y!1" "n0z" "n0y!1" ))"" (replace -1 1)"" (hide -1)"" "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 )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil )nil number_fields nil )nil number_fields_bis nil )"nznum" nil )nil number_fields_bis nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3280145209"" (skosimp*)"" "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" )"" "(x!1 / n0x!1) + (y!1 / n0y!1)" "n0x!1 * n0y!1" )"" (replace -2 1)"" "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" )"" "n0y!1" "n0x!1" "x!1 / n0x!1" )"" (replace -4 -2 rl)"" "div_cancel1" )"" "n0x!1" "x!1" )"" replace -2 -4)"" replace -4 1 rl)"" "" "n0y!1" "y!1" )"" "n0x!1" "n0y!1" "y!1/n0y!1" )"" replace -1 -2)"" replace -2 1 rl)"" "" "n0y!1" "x!1" )"" "n0x!1" "y!1" )"" replace -1 1)"" replace "" 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 )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil )"nznum" nil )nil number_fields nil )nil number_fields nil )nil number_fields_bis nil )nil number_fields nil ))nil 3280143033"" (skosimp*)"" "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" "div_def" "y" "-y!1" "n0x" "n0y!1" ))"1" (replace -1 1)"1" "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" "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" "distributive" "x" "y!2" "y" "x!2" "z" "-x!2" ))"2" (replace -2)"2" (rewrite "zero_times2" -1)"2" (hide -2)"2" "commutative_mult" )"2" "y!2" "x!2" )"2" replace -2)"2" "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 )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil )nil number_fields_bis nil )nil number_fields nil )nil number_fields nil )nil number_fields_bis nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"nznum" nil )"odd_int" integers nil )nil number_fields nil )"nznum" nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil ))nil 3280143932"" (skosimp*)"" (lemma "div_def" ("n0x" "n0x!1" ))"" (inst-cp - "x!1" )"" (inst-cp - "y!1" )"" (inst - "x!1-y!1" )"" (replace -1)"" (replace -2)"" (replace -3)"" (hide-all-but 1)"" (lemma "commutative_mult" ("y" "1/n0x!1" ))"" (inst-cp - "x!1" )"" (inst-cp - "y!1" )"" (inst - "x!1-y!1" )"" (replace -1)"" replace -2)"" replace -3)"" "" "distributive" "x" "1/n0x!1" "y" "x!1" "z" "-y!1" ))"" "minus_add" )"" "x!1" "y!1" )"" replace -2)"" replace -3)"" "1 / n0x!1 * x!1" "1 / n0x!1 * y!1" )"" replace -1)"" "" assert )"" "both_sides_plus2" "z" "1 / n0x!1 * y!1" "x" "-(1 / n0x!1 * y!1)" "y" "1 / n0x!1 * -y!1" ))"" replace "" "" rewrite "inverse_add" )"" "distributive" "x" "1/n0x!1" "y" "y!1" "z" "-y!1" ))"" replace "" rewrite "inverse_add" "" rewrite "zero_times2" 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 number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields nil )"nznum" nil )"odd_int" integers nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"nznum" nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields_bis nil )nil number_fields_bis nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil ))nil 3280144554"" (skosimp*)"" (lemma "div_def" ("n0x" "n0z!1" ))"" (inst-cp - "x!1" )"" (inst-cp - "y!1" )"" (inst - "x!1+y!1" )"" (replace -1)"" (replace -2)"" (replace -3)"" (hide-all-but 1)"" (lemma "commutative_mult" ("y" "1/n0z!1" ))"" (inst-cp - "x!1" )"" (inst-cp - "y!1" )"" (inst - "x!1+y!1" )"" (replace -1)"" replace -2)"" replace -3)"" "" "distributive" "x" "1/n0z!1" "y" "x!1" "z" "y!1" ))"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"nznum" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil ))nil 3280137015"" (skosimp*)"" (lemma "minus_div2" ("x" "x!1" "y" "y!1" "n0x" "n0z!1" ))"" (propax) nil nil )) nil ))nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil ))nil 3280144769"" (skosimp*)"" "nznum_div_nznum_is_nznum" ("nzx" "n0y!1" "nzy" "n0z!1" ))"" "cross_mult" "x" "x!1" "n0x" "n0y!1 / n0z!1" "y" "x!1 * n0z!1" "n0y" "n0y!1" ))"" (replace -1 1)"" (hide -1)"" (lemma "div_cancel1" ("x" "n0y!1" "n0z" "n0z!1" ))"" "associative_mult" "x" "x!1" "y" "n0z!1" "z" "n0y!1/n0z!1" ))"" (replace -2 -1) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil )nil number_fields_bis nil )nil number_fields nil )"nznum" nil )nil number_fields_bis nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3280145858"" (skosimp*)"" "nznum_times_nznum_is_nznum" "nzx" "n0y!1" "nzy" "n0z!1" ))"" "cross_mult" "x" "x!1 / n0y!1" "n0x" "n0z!1" "y" "x!1" "n0y" "n0y!1 * n0z!1" ))"" (replace -1 1)"" (hide -1)"" (rewrite "associative_mult" )"" (lemma "div_cancel2" ("x" "x!1" "n0z" "n0y!1" ))"" (replace -1) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bisnil )nil number_fields nil )nil number_fields_bis nil )"nznum" nil )nil number_fields_bis nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil ))nil 3280137061"" (skosimp*)"" (grind)"" (case "x!1/=0" )"1" (lemma "both_sides_times1" ("n0z" "x!1" "x" "2" "y" "1" ))"1" (assert ) (("1" (rewrite "identity_mult" 1) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil number_fields nil )nil number_fields_bis nil )nil number_fields nil )nil number_fields nil )nil numbers nil )nil booleans nil )"boolean" notequal nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil ))nil 3280295656"" (skosimp*)"" (lemma "zero_times3" ("x" "n0x!1" "y" "y!1" ))"" (assert ) nil nil )) nil ))nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil ))nil 3280295688"" (skosimp*)"" (lemma "zero_times3" ("x" "x!1" "y" "n0y!1" ))"" (assert ) nil nil )) nil ))nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil ))nil 3280295710"" (skosimp*)"" (lemma "zero_times3" ("x" "n0x!1" "y" "n0y!1" ))"" (assert ) nil nil )) nil ))nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil )"nznum" nil ))nil 3280295888"" (skosimp*)"" (split)"1" (flatten)"1" "both_sides_minus1" "z" "x!1" "x" "x!1*x!1" "y" "x!1" ))"1" (replace -1 -2 rl)"1" (hide -1)"1" (lemma "inverse_add" ("x" "x!1" ))"1" (lemma "minus_add" ("x" "x!1" "y" "x!1" ))"1" (replace -2)"1" (replace -1)"1" (hide -1 -2)"1" "distributive" "x" "x!1" "y" "x!1" "z" "-1" ))"1" "(x!1 * x!1) + (x!1 * -1) = x!1 * x!1 - x!1" )"1" (replace -3)"1" "1" "zero_times3" "x" "x!1" "y" "x!1 + -1" ))"1" assert )"1" "1" "both_sides_minus1" "z" "1" "x" "x!1" "y" "1" ))"1" replace -1 1 rl)"1" "1" replace -1 1)"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" assert )"2" rewrite "commutative_mult" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields_bis nil )nil number_fields nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields_bis nil )"even_int" integersnil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"odd_int" integers nil )"nznum" nil )nil number_fields nil )"odd_int" integers nil )"posint" nil )"nznum" nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil ))nil 3294692619"" (skosimp)"" "number_fields_negate_is_right_inverse" ("x" "x!1*y!1" ))"" (lemma "number_fields_negate_is_right_inverse" ("x" "x!1" ))"" (lemma "distributive" ("x" "y!1" "y" "x!1" "z" "-x!1" ))"" (replace -2 -1)"" (lemma "commutative_mult" ("x" "y!1" "y" "x!1" ))"" (lemma "commutative_mult" ("x" "y!1" "y" "-x!1" ))"" (replace -1 -3)"" (replace -2 -3)"" (rewrite "zero_times2" )"" (replace -3 -5) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil number_fields_bis nil ))nil 3294693138"" (skosimp)"" "number_fields_negate_is_right_inverse" ("x" "x!1 * y!1" ))"" (lemma "number_fields_negate_is_right_inverse" ("x" "y!1" ))"" (lemma "distributive" ("x" "x!1" "y" "y!1" "z" "-y!1" ))"" (replace -2 -1)"" (rewrite "zero_times2" )"" (replace -1 -3)"" (hide -1 -2) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil number_fields_bis nil ))nil 3596478685"" (skeep)"" (rewrite "number_fields_negative_times" )"" (rewrite "identity_mult" ) nil nil )) nil ))nil )nil number_fields_bisnil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"nznum" nil )"odd_int" integers nil )nil number_fields nil )nil number_fields nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.48 Sekunden
(vorverarbeitet am 2026-05-03)
¤ *© Formatika GbR, Deutschland
2026-05-26
