| products/Sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: linear_dependence.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(primes_sum_squares
(sum_of_two_squares?_TCC1 0 (sum_of_two_squares?_TCC1-1 nil 3501936852 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (sots_int?_TCC1 0 (sots_int?_TCC1-1 nil 3501939999 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (sots_int_def 0 (sots_int_def-1 nil 3501939999 ("" (skeep) (("" (expand "sum_of_two_squares?") (("" (expand "sots_int?") (("" (skosimp*) (("" (inst + "abs(ai!1)" "abs(bi!1)") (("" (replace -1) (("" (hide -) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat_exp application-judgement "nat" exponentiation nil) (sum_of_two_squares? const-decl "bool" primes_sum_squares nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (int_expt application-judgement "int" exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals 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) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (sots_int? const-decl "bool" primes_sum_squares nil) (int_exp application-judgement "int" exponentiation nil)) shostak)) (Brahmagupta_Fibonacci 0 (Brahmagupta_Fibonacci-1 nil 3501936852 ("" (skeep) (("" (typepred "ns") (("" (typepred "ms") (("" (expand "sum_of_two_squares?") (("" (skosimp*) (("" (name "vv" "(a!1*b!2-b!1*a!2)") (("" (case "vv>=0") (("1" (inst + "(a!1*a!2 + b!1*b!2)" "vv") (("1" (replace -3) (("1" (replace -4) (("1" (hide -) (("1" (expand "vv") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "(a!1*a!2 + b!1*b!2)" "-vv") (("1" (replace -2) (("1" (replace -3) (("1" (expand "vv" +) (("1" (hide-all-but 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sum_of_two_squares? const-decl "bool" primes_sum_squares nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals 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) (nat_exp application-judgement "nat" exponentiation 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) (= const-decl "[T, T -> boolean]" equalities nil) (int_minus_int_is_int application-judgement "int" integers nil) (minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (vv skolem-const-decl "int" primes_sum_squares nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat_expt application-judgement "nat" exponentiation nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_expt application-judgement "int" exponentiation nil) (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak)) (prime_divides 0 (prime_divides-1 nil 3501939374 ("" (case "FORALL (k,r:int): divides(k,r) IFF divides(k,-r)") (("1" (label "intlem" -1) (("1" (hide "intlem") (("1" (case "FORALL (nn, mm: posnat, p: (prime?)): divides(p, nn * mm) IMPLIES (divides(p, nn) OR divides(p, mm))") (("1" (skeep) (("1" (case "ai = 0 OR bi=0") (("1" (split -) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (case "FORALL (nn, mm: posnat, p: (prime?)): divides(p, (-nn) * mm) IMPLIES (divides(p, (-nn)) OR divides(p, mm))") (("1" (case "FORALL (nn, mm: posnat, p: (prime?)): divides(p, (-nn) * (-mm)) IMPLIES (divides(p, (-nn)) OR divides(p, (-mm)))") (("1" (case "ai<0") (("1" (case "bi<0") (("1" (assert) (("1" (inst -3 "-ai" "-bi" "p") (("1" (assert) nil nil)) nil)) nil) ("2" (inst -3 "-ai" "bi" "p") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("2" (case "bi<0") (("1" (inst -3 "-bi" "ai" "p") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (inst -3 "ai" "bi" "p") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide (2 3 4 5 6)) (("2" (skosimp*) (("2" (inst - "nn!1" "mm!1" "p!1") (("2" (assert) (("2" (split -) (("1" (reveal "intlem") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (reveal "intlem") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (2 3 4 5 6)) (("2" (skosimp*) (("2" (inst - "nn!1" "mm!1" "p!1") (("2" (assert) (("2" (split -) (("1" (reveal "intlem") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (reveal "intlem") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "divides" -) (("2" (skolem -1 "r") (("2" (case "FORALL (kr:posnat): (NOT divides(p,kr)) IMPLIES gcd(p,kr) = 1") (("1" (inst - "mm") (("1" (assert) (("1" (lemma "gcd_factors") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (replace -2) (("1" (mult-by -1 "nn") (("1" (assert) (("1" (expand "divides" 1) (("1" (name "vv" "ip!1*nn + jp!1*r") (("1" (case "nn=p*vv") (("1" (case "vv > 0") (("1" (inst + "vv") nil nil) ("2" (lemma "posreal_times_posreal_is_posreal") (("2" (inst - "p" "-vv") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (typepred "p") (("3" (expand "prime?") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (typepred "gcd(p,kr)") (("2" (typepred "p") (("2" (expand "prime?") (("2" (flatten) (("2" (inst - "gcd(p,kr)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "FORALL (k, r: int): divides(k, r) IMPLIES divides(k, -r)") (("1" (skeep) (("1" (ground) (("1" (inst - "k" "r") (("1" (assert) nil nil)) nil) ("2" (inst - "k" "-r") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "divides") (("2" (skosimp*) (("2" (inst + "-x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (prime? const-decl "bool" primes "ints/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (int_times_even_is_even application-judgement "even_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (ai skolem-const-decl "int" primes_sum_squares nil) (bi skolem-const-decl "int" primes_sum_squares nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gcd_factors formula-decl nil gcd "ints/") (p skolem-const-decl "(prime?)" primes_sum_squares nil) (vv skolem-const-decl "int" primes_sum_squares nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd "ints/") (/= const-decl "boolean" notequal nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_int_is_int application-judgement "int" integers 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) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (divides const-decl "bool" divides nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil)) nil)) (sots_div_prime_closed_TCC1 0 (sots_div_prime_closed_TCC1-1 nil 3501939374 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sum_of_two_squares? const-decl "bool" primes_sum_squares nil) (prime_sum_of_two_squares? const-decl "bool" primes_sum_squares nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nat_expt application-judgement "nat" exponentiation nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (prime? const-decl "bool" primes "ints/") (^ const-decl "real" exponentiation nil) (divides const-decl "bool" divides nil) (/= const-decl "boolean" notequal nil)) nil)) (sots_div_prime_closed_TCC2 0 (sots_div_prime_closed_TCC2-1 nil 3501939374 ("" (skeep) (("" (expand "divides") (("" (skosimp*) (("" (case "ns/ps = x!1") (("1" (assert) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ((divides const-decl "bool" divides nil) (prime_sum_of_two_squares? const-decl "bool" primes_sum_squares nil) (sum_of_two_squares? const-decl "bool" primes_sum_squares nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (/ const-decl "[numfield, nznum -> numfield]" 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) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel3 formula-decl nil real_props nil)) nil)) (sots_div_prime_closed 0 (sots_div_prime_closed-1 nil 3501939558 ("" (case "FORALL (rr:nzint,rs:int): divides(rr,rs) IMPLIES integer_pred(rs/rr)") (("1" (label "integerpredlem" -1) (("1" (hide "integerpredlem") (("1" (case "FORALL (rr,rs:int): divides(rr,rs) IFF divides(rr,-rs)") (("1" (label "intlem" -1) (("1" (hide "intlem") (("1" (skeep) (("1" (typepred "ns") (("1" (typepred "ps") (("1" (case "EXISTS (a,b,pp,qq:nat): ns = a^2+b^2 AND ps = pp^2+qq^2") (("1" (skeep -1) (("1" (hide -3) (("1" (hide -3) (("1" (case "divides(ps,(pp*b-a*qq)*(pp*b+a*qq))") (("1" (lemma "prime_divides") (("1" (inst?) (("1" (assert) (("1" (hide -2) (("1" (split -) (("1" (case "divides(ps,(a*pp+b*qq)^2)") (("1" (case "divides(ps^2,(a*pp+b*qq)^2)") (("1" (name "f1" "(a*pp+b*qq)/ps") (("1" (name "f2" "(a*qq-b*pp)/ps") (("1" (lemma "sots_int_def") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (case "integer_pred(f1) and integer_pred(f2)") (("1" (flatten) (("1" (expand "sots_int?") (("1" (inst + "f1" "f2") (("1" (replace -8 +) (("1" (replace -9 +) (("1" (expand "f1" +) (("1" (expand "f2" +) (("1" (replace -9 + :dir rl) (("1" (case "ps*(a^2+b^2) = (a * qq - b * pp)^2+(a * pp + b * qq)^2") (("1" (hide-all-but (-1 1)) (("1" (name "pz" "a^2+b^2") (("1" (replace -1) (("1" (hide -1) (("1" (name "zz" "(a * qq - b * pp)") (("1" (replace -1) (("1" (name "sz" "(a * pp + b * qq)") (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (grind) (("1" (mult-by 1 "ps^2") (("1" (grind) (("1" (field) nil nil)) nil) ("2" (typepred "ps") (("2" (expand "prime_sum_of_two_squares?") (("2" (expand "prime?") (("2" (ground) (("2" (lemma "posreal_times_posreal_is_posreal") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -9 +) (("2" (hide -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "integerpredlem") (("2" (split +) (("1" (expand "f1" +) (("1" (inst?) (("1" (assert) (("1" (lemma "prime_divides") (("1" (inst - "a*pp+b*qq" "a*pp+b*qq" "ps") (("1" (assert) (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "ps") (("2" (expand "prime_sum_of_two_squares?") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "f2" +) (("2" (inst?) (("2" (assert) (("2" (reveal "intlem") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "integerpredlem") (("2" (inst?) (("2" (assert) (("2" (typepred "ps") (("2" (expand "prime_sum_of_two_squares?") (("2" (expand "prime?") (("2" (flatten) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "prime_divides") (("2" (inst - "a*pp+b*qq" "a*pp+b*qq" "ps") (("1" (assert) (("1" (case "divides(ps, a * pp + b * qq)") (("1" (hide -2) (("1" (expand "divides" (-1 1)) (("1" (skosimp*) (("1" (inst + "x!1^2") (("1" (replace -1) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "^") (("2" (expand "expt" -1) (("2" (expand "expt" -1) (("2" (expand "expt" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "ps") (("2" (expand "prime_sum_of_two_squares?") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "divides_sum") (("2" (inst - "ns*ps" "-(a*qq-b*pp)^2" "ps") (("2" (split -) (("1" (replace -3 -1) (("1" (replace -4 -1) (("1" (grind :exclude ("divides" "sum_of_two_squares?")) nil nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "divides") (("2" (skosimp*) (("2" (inst + "x!1*(-pp*b+a*qq)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "divides") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "divides(ps,(a*pp-b*qq)^2)") (("1" (case "divides(ps^2,(a*pp-b*qq)^2)") (("1" (name "f1" "(a*pp-b*qq)/ps") (("1" (name "f2" "(a*qq+b*pp)/ps") (("1" (lemma "sots_int_def") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (case "integer_pred(f1) and integer_pred(f2)") (("1" (flatten) (("1" (expand "sots_int?") (("1" (inst + "f1" "f2") (("1" (replace -8 +) (("1" (replace -9 +) (("1" (expand "f1" +) (("1" (expand "f2" +) (("1" (replace -9 + :dir rl) (("1" (case "ps*(a ^ 2 + b ^ 2) = (a * pp - b * qq) ^ 2 + (a * qq + b * pp) ^ 2") (("1" (hide-all-but (-1 1)) (("1" (name "pz" "a^2+b^2") (("1" (replace -1) (("1" (hide -1) (("1" (name "zz" "(a * pp - b * qq)") (("1" (replace -1) (("1" (name "sz" "(a * qq + b * pp)") (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (grind) (("1" (mult-by 1 --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.180 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 |
