|
(poly_systems
(system_roots_enum 0
(system_roots_enum-1 nil 3618845198
("" (skeep)
(("" (case "FORALL (i): i<=k IMPLIES n(i)=0")
(("1"
(case "FORALL (i,x): i<=k IMPLIES polynomial(p(i),n(i))(x)/=0")
(("1" (inst + "0" "LAMBDA (j:below(0)): 0")
(("1" (split)
(("1" (skosimp*) nil nil) ("2" (skosimp*) nil nil)
("3" (skosimp*)
(("3" (inst - "j!1" "b!1") (("3" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skeep)
(("2" (inst - "i")
(("2" (inst - "i")
(("2" (assert)
(("2" (replace -3)
(("2" (expand "polynomial")
(("2" (expand "sigma")
(("2" (expand "sigma") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(name "IGGY"
"LAMBDA (b:real): ((EXISTS (j:nat): j<=k AND polynomial(p(j), n(j))(b) = 0))")
(("2" (case "is_finite[real](IGGY)")
(("1" (copy -1)
(("1" (lemma "card_bij_inv[real]")
(("1" (name "K" "card(IGGY)")
(("1" (inst - "K" "IGGY")
(("1" (assert)
(("1" (label "fbij" -2)
(("1" (skeep)
(("1" (skeep -2)
(("1"
(name "newenum"
"sort_array[K,real,<=].sort(f)")
(("1" (inst + "K" "newenum")
(("1"
(case
"NOT (FORALL (i, j: below(K)): i < j IMPLIES newenum(i) < newenum(j))")
(("1"
(hide 3)
(("1"
(skeep)
(("1"
(case
"NOT newenum(i!1) = newenum(j)")
(("1"
(assert)
(("1"
(typepred "newenum")
(("1"
(expand "sorted?")
(("1"
(inst - "i!1" "j")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(typepred "newenum")
(("2"
(expand "permutation_of?")
(("2"
(skosimp*)
(("2"
(expand "bijective?" -1)
(("2"
(flatten)
(("2"
(expand
"surjective?")
(("2"
(inst-cp - "j")
(("2"
(inst - "i!1")
(("2"
(skosimp*)
(("2"
(inst-cp
-
"x!1")
(("2"
(inst
-
"x!2")
(("2"
(replace
-2)
(("2"
(replace
-3)
(("2"
(copy
"fbij")
(("2"
(expand
"bijective?"
-1)
(("2"
(flatten)
(("2"
(expand
"injective?"
-1)
(("2"
(inst-cp
-
"x!1"
"x!2")
(("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)
("2"
(replace -1)
(("2"
(assert)
(("2"
(split)
(("1"
(skeep)
(("1"
(typepred "newenum")
(("1"
(expand "permutation_of?")
(("1"
(skosimp*)
(("1"
(expand "bijective?")
(("1"
(flatten)
(("1"
(expand
"surjective?"
-2)
(("1"
(inst - "i!1")
(("1"
(skolem
-
"j!1")
(("1"
(inst
-
"j!1")
(("1"
(assert)
(("1"
(typepred
"f(j!1)")
(("1"
(replace
-3)
(("1"
(replace
-4
:dir
rl)
(("1"
(expand
"IGGY"
-1)
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skeep)
(("2"
(typepred "newenum")
(("2"
(expand "permutation_of?")
(("2"
(skosimp*)
(("2"
(expand "bijective?")
(("2"
(flatten)
(("2"
(expand
"surjective?"
-11)
(("2"
(inst -11 "b")
(("1"
(skolem - "ii")
(("1"
(inst - "ii")
(("1"
(inst
+
"f!1(ii)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"IGGY"
1)
(("2"
(assert)
(("2"
(inst
+
"j")
(("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)
("2" (propax) nil nil))
nil))
nil))
nil)
("2" (hide 3)
(("2"
(name "IGGYk"
"LAMBDA (kp:nat): (LAMBDA (b: real):(EXISTS (j: nat):
j <= kp AND polynomial(p(j), n(j))(b) = 0))")
(("2"
(case "FORALL (kp:nat): kp<=k IMPLIES is_finite[real](IGGYk(kp))")
(("1" (inst - "k")
(("1" (assert)
(("1" (case "IGGYk(k) = IGGY")
(("1" (assert) nil nil)
("2" (decompose-equality 1)
(("2" (expand "IGGYk" 1)
(("2" (expand "IGGY" 1)
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2"
(name "IGGYthis"
"LAMBDA (kp:nat): LAMBDA (b:real): polynomial(p(kp),n(kp))(b)=0")
(("2"
(case "FORALL (kp:nat): kp<=k IMPLIES is_finite[real](IGGYthis(kp))")
(("1" (induct "kp")
(("1" (assert)
(("1" (inst - "0")
(("1" (assert)
(("1" (case "IGGYthis(0)=IGGYk(0)")
(("1" (assert) nil nil)
("2"
(decompose-equality 1)
(("2"
(expand "IGGYthis" 1)
(("2"
(expand "IGGYk" 1)
(("2"
(iff)
(("2"
(ground)
(("1"
(inst + "0")
(("1" (assert) nil nil))
nil)
("2"
(skosimp*)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (assert)
(("2"
(case "IGGYk(1+j) = union(IGGYk(j),IGGYthis(1+j))")
(("1" (lemma "finite_union[real]")
(("1"
(inst - "IGGYk(j)" "IGGYthis(1+j)")
(("1" (assert) nil nil)
("2"
(inst - "1+j")
(("2" (assert) nil nil))
nil))
nil))
nil)
("2" (decompose-equality 1)
(("2"
(expand "union" 1)
(("2"
(expand "member")
(("2"
(expand "IGGYk" 1)
(("2"
(expand "IGGYthis" 1)
(("2"
(iff)
(("2"
(ground)
(("1"
(skosimp*)
(("1"
(case "j!1 = 1+j")
(("1" (assert) nil nil)
("2"
(inst + "j!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst + "j!1")
(("2" (assert) nil nil))
nil))
nil)
("3"
(inst + "1+j")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "FORALL (kk:nat,a:[nat->real]): (EXISTS (i:nat):i<=kk AND a(i)/=0) IMPLIES is_finite[real](LAMBDA (b:real): polynomial(a,kk)(b)=0)")
(("1" (skeep)
(("1" (inst - "n(kp)" "p(kp)")
(("1" (split -)
(("1" (assert)
(("1"
(expand "IGGYthis" 1)
(("1" (propax) nil nil))
nil))
nil)
("2" (inst + "n(kp)")
(("2"
(assert)
(("2"
(inst - "kp")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (induct "kk")
(("1" (skeep)
(("1" (skeep -1)
(("1"
(case "i = 0")
(("1"
(replaces -1)
(("1"
(hide -)
(("1"
(assert)
(("1"
(lemma "finite_emptyset[real]")
(("1"
(invoke
(case "%1 = %2")
(! -1 1)
(! 2 1))
(("1" (assert) nil nil)
("2"
(hide (-1 3))
(("2"
(decompose-equality 1)
(("2"
(expand "polynomial")
(("2"
(expand "sigma")
(("2"
(expand "sigma")
(("2"
(expand
"emptyset")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2"
(case
"EXISTS (z:real): polynomial(a,j+1)(z)=0")
(("1"
(skeep -1)
(("1"
(lemma "polynomial_zero_factor")
(("1"
(inst?)
(("1"
(replace -2)
(("1"
(skosimp -1)
(("1"
(invoke
(name "IP" "%1")
(! 1 1))
(("1"
(replace -1)
(("1"
(inst -4 "g!1")
(("1"
(split -4)
(("1"
(invoke
(name "IG" "%1")
(! -1 1))
(("1"
(replace -1)
(("1"
(case
"IP = union(IG,singleton(z))")
(("1"
(lemma
"finite_union[real]")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(decompose-equality
1)
(("2"
(iff)
(("2"
(expand
"IP"
+)
(("2"
(expand
"IG"
+)
(("2"
(expand
"union"
+)
(("2"
(expand
"singleton"
+)
(("2"
(expand
"member"
+)
(("2"
(ground)
(("1"
(inst-cp
-
"x!1")
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(inst
-
"x!1")
(("2"
(replaces
-1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"polynomial_eq_coeff")
(("2"
(inst
-
"a"
"LAMBDA (i:nat): 0"
"j+1")
(("2"
(flatten)
(("2"
(hide -2)
(("2"
(split -1)
(("1"
(skosimp*)
(("1"
(inst
-
"i!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(decompose-equality
1)
(("2"
(case
"polynomial(LAMBDA (i: nat): 0, 1 + j)(x!1) = 0")
(("1"
(replaces
-1)
(("1"
(assert)
(("1"
(inst
-
"x!1")
(("1"
(case
"polynomial(g!1, j)(x!1) = 0")
(("1"
(assert)
nil
nil)
("2"
(expand
"polynomial"
1)
(("2"
(rewrite
"sigma_restrict_eq_0")
(("2"
(hide
2)
(("2"
(skosimp*)
(("2"
(inst
+
"i!1")
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"polynomial"
1)
(("2"
(rewrite
"sigma_restrict_eq_0")
(("2"
(skosimp*)
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "finite_emptyset[real]")
(("2"
(invoke
(case "%1 = %2")
(! -1 1)
(! 2 1))
(("1" (assert) nil nil)
("2"
(decompose-equality 1)
(("2"
(iff)
(("2"
(expand "emptyset" 1)
(("2"
(inst + "x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((= const-decl "[T, T -> boolean]" equalities nil)
(<= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(sigma def-decl "real" sigma "reals/")
(FALSE const-decl "bool" booleans nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(/= const-decl "boolean" notequal nil)
(sequence type-eq-decl nil sequences nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(card_bij_inv formula-decl nil finite_sets nil)
(IGGY skolem-const-decl "[real -> boolean]" poly_systems nil)
(b skolem-const-decl "real" poly_systems nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(bijective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(sort const-decl "{a | permutation_of?(A, a) AND sorted?(a)}"
sort_array "structures/")
(sorted? const-decl "bool" sort_array "structures/")
(permutation_of? const-decl "bool" permutations "structures/")
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(emptyset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset judgement-tcc nil finite_sets nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(IP skolem-const-decl "[real -> boolean]" poly_systems nil)
(real_times_real_is_real application-judgement "real" reals nil)
(IG skolem-const-decl "[real -> boolean]" poly_systems nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(nonempty_union2 application-judgement "(nonempty?)" sets nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(subrange type-eq-decl nil integers nil)
(sigma_restrict_eq_0 formula-decl nil sigma "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation nil)
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(j skolem-const-decl "nat" poly_systems nil)
(i!1 skolem-const-decl "nat" poly_systems nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(polynomial_eq_coeff formula-decl nil polynomials "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(polynomial_zero_factor formula-decl nil polynomials "reals/")
(pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(IGGYthis skolem-const-decl "[nat -> [real -> boolean]]"
poly_systems nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(member const-decl "bool" sets nil)
(finite_union judgement-tcc nil finite_sets nil)
(j skolem-const-decl "nat" poly_systems nil)
(union const-decl "set" sets nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(IGGYk skolem-const-decl "[nat -> [real -> boolean]]" poly_systems
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
nil))
(strict_poly_system_solvable_TCC1 0
(strict_poly_system_solvable_TCC1-1 nil 3618843949
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" real_orders "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/"))
nil))
(strict_poly_system_solvable_TCC2 0
(strict_poly_system_solvable_TCC2-1 nil 3621242993
("" (skosimp*) (("" (assert) nil nil)) nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(sigma_nat application-judgement "nat" sigma_nat "reals/")
(sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/"))
nil))
(strict_poly_system_solvable 0
(strict_poly_system_solvable-4 nil 3618918694
("" (lemma "system_roots_enum")
(("" (skeep)
(("" (inst - "k" "n" "p")
(("" (assert)
(("" (replace -2)
(("" (skeep)
(("" (label "fmz" -1)
(("" (label "skz" -3)
((""
(name "Q" "prod_polynomials
(p, n, (LAMBDA (i: nat): 1), k)")
(("" (replace -1)
(("" (name "Qdeg" "sigma(0, k, n)")
(("" (replace -1)
((""
(case "NOT FORALL (x): polynomial(Q,Qdeg)(x)=0 IFF (EXISTS (i:below(K)): x = enum(i))")
(("1" (hide 2)
(("1"
(skeep)
(("1"
(typepred "Q")
(("1"
(case
"NOT n * (LAMBDA (i: nat): 1) = n")
(("1"
(decompose-equality 1)
(("1"
(expand "*" 1)
(("1" (propax) nil nil))
nil))
nil)
("2"
(replace -1)
(("2"
(inst - "x")
(("2"
(replace -5)
(("2"
(replace -2)
(("2"
(ground)
(("1"
(lemma
"product_eq_0[nat]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(expand "^" -1)
(("1"
(expand
"expt"
-1)
(("1"
(expand
"expt"
-1)
(("1"
(inst
"skz"
"x"
"n!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(assert)
(("2"
(expand "^")
(("2"
(expand "expt")
(("2"
(expand "expt")
(("2"
(assert)
(("2"
(lemma
"product_eq_zero[nat]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(inst
-8
"i!1")
(("2"
(skosimp*)
(("2"
(inst
+
"j!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)
("2" (assert)
(("2"
(split 1)
(("1"
(flatten)
(("1"
(skeep -1)
(("1"
(case "K = 0")
(("1"
(skeep 1)
(("1"
(inst - "i")
(("1"
(assert)
(("1"
(lemma
"poly_sign_near_infinity")
(("1"
(inst - "p(i)" "n(i)")
(("1"
(assert)
(("1"
(inst-cp -11 "i")
(("1"
(assert)
(("1"
(assert)
(("1"
(flatten)
(("1"
(skeep -1)
(("1"
(expand
"sign_ext"
-1
2)
(("1"
(expand
"sign_ext"
-1)
(("1"
(assert)
(("1"
(inst-cp
-
"x")
(("1"
(assert)
(("1"
(inst
-
"M")
(("1"
(assert)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(lemma
"poly_intermediate_value_dec")
(("1"
(inst
-
"p(i)"
"0"
"n(i)"
"x"
"M")
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(inst
-14
"cc!1"
"i")
(("1"
(assert)
(("1"
(skosimp*)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.88Quellennavigators
Analyse erneut starten
]
|
