|
(tarski_query_matrix
(TQ_vect3k_TCC1 0
(TQ_vect3k_TCC1-1 nil 3620050327
("" (skeep)
(("" (skosimp*)
(("" (replaces -1)
(("" (assert)
(("" (lemma "base_n_lt_n")
(("" (lemma "columns_form_matrix")
(("" (inst?)
(("" (assert)
(("" (lemma "base_n_lt_n")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_exp application-judgement "posint" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(columns_form_matrix formula-decl nil matrices "matrices/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(base_n_lt_n formula-decl nil base_repr "reals/"))
nil))
(TQ_vect3k_TCC2 0
(TQ_vect3k_TCC2-1 nil 3621088362
("" (skeep)
(("" (skeep)
(("" (rewrite "rows_form_matrix")
(("" (lemma "columns_form_matrix")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((columns_form_matrix formula-decl nil matrices "matrices/")
(form_matrix_square application-judgement "FullMatrix" matrices
"matrices/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR 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)
(rows_form_matrix formula-decl nil matrices "matrices/")
(posint_exp application-judgement "posint" exponentiation nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(TQ_vect6k_TCC1 0
(TQ_vect6k_TCC1-1 nil 3620494852
("" (skeep)
(("" (skeep)
(("" (skeep)
(("" (case "x1<=k")
(("1" (inst + "x1")
(("1" (replace -2 +)
(("1" (assert) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (assert)
(("2" (case "GPFun(i1,j1)(x1)=0")
(("1" (assert) nil nil)
("2" (replaces -1)
(("2" (assert)
(("2" (assert)
(("2" (lemma "base_n_0")
(("2" (inst?)
(("2" (assert)
(("2" (lemma "both_sides_expt_gt1_le_aux")
(("2" (inst - "6" "k" "x1-1")
(("2"
(expand "^")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_exp application-judgement "posint" exponentiation nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(x1 skolem-const-decl "nat" tarski_query_matrix nil)
(k skolem-const-decl "nat" tarski_query_matrix nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(base_n_0 formula-decl nil base_repr "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(both_sides_expt_gt1_le_aux formula-decl nil exponentiation nil)
(> const-decl "bool" reals nil))
nil))
(TQ_vect6k_TCC2 0
(TQ_vect6k_TCC2-1 nil 3620494852
("" (skeep)
(("" (skeep)
(("" (rewrite "rows_form_matrix")
(("" (assert)
(("" (lemma "columns_form_matrix")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((form_matrix_square application-judgement "FullMatrix" matrices
"matrices/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(columns_form_matrix formula-decl nil matrices "matrices/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR 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)
(rows_form_matrix formula-decl nil matrices "matrices/")
(posint_exp application-judgement "posint" exponentiation nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(NSol_vect3k_TCC1 0
(NSol_vect3k_TCC1-1 nil 3620051889
("" (skosimp*)
(("" (lemma "base_n_lt_n")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((base_n_lt_n formula-decl nil base_repr "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_exp application-judgement "posint" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(NSol_vect3k_TCC2 0
(NSol_vect3k_TCC2-1 nil 3621088362
("" (skeep)
(("" (rewrite "rows_form_matrix")
(("" (lemma "columns_form_matrix")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_exp application-judgement "posint" exponentiation nil)
(rows_form_matrix formula-decl nil matrices "matrices/")
(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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(naturalnumber type-eq-decl nil naturalnumbers nil)
(form_matrix_square application-judgement "FullMatrix" matrices
"matrices/")
(columns_form_matrix formula-decl nil matrices "matrices/"))
nil))
(NSol_vect6k_TCC1 0
(NSol_vect6k_TCC1-1 nil 3620139071
("" (skosimp*)
(("" (lemma "base_n_lt_n")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((base_n_lt_n formula-decl nil base_repr "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_exp application-judgement "posint" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(NSol_vect6k_TCC2 0
(NSol_vect6k_TCC2-1 nil 3621088362
("" (skeep)
(("" (rewrite "rows_form_matrix")
(("" (assert)
(("" (lemma "columns_form_matrix")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_exp application-judgement "posint" exponentiation nil)
(rows_form_matrix formula-decl nil matrices "matrices/")
(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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(naturalnumber type-eq-decl nil naturalnumbers nil)
(columns_form_matrix formula-decl nil matrices "matrices/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(form_matrix_square application-judgement "FullMatrix" matrices
"matrices/"))
nil))
(A66_inv_TCC1 0
(A66_inv_TCC1-1 nil 3620408236 ("" (grind) nil nil)
((listn_0 name-judgement "listn[real](0)" polynomial_division
"Sturm/")
(listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
(every adt-def-decl "boolean" list_adt nil))
nil))
(A66_inv_TCC2 0
(A66_inv_TCC2-1 nil 3620408236 ("" (grind) nil nil)
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(listn_0 name-judgement "listn[real](0)" polynomial_division
"Sturm/")
(listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
(every adt-def-decl "boolean" list_adt nil))
nil))
(A66_inv_TCC3 0
(A66_inv_TCC3-1 nil 3620408236 ("" (eval-formula) nil nil)
((TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(A66_TCC1 0
(A66_TCC1-1 nil 3621152270
("" (skeep) (("" (eval-formula) nil nil)) nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil))
nil))
(A66_TCC2 0
(A66_TCC2-1 nil 3621152270 ("" (grind) nil nil)
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(listn_0 name-judgement "listn[real](0)" polynomial_division
"Sturm/")
(listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
(every adt-def-decl "boolean" list_adt nil))
nil))
(A66_TCC3 0
(A66_TCC3-1 nil 3621152270 ("" (grind) nil nil)
((posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(listn_0 name-judgement "listn[real](0)" polynomial_division
"Sturm/")
(listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/")
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(every adt-def-decl "boolean" list_adt nil))
nil))
(A66_TCC4 0
(A66_TCC4-1 nil 3621152270 ("" (eval-formula) nil nil)
((TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(multi_sturm_tarski_6by6 0
(multi_sturm_tarski_6by6-1 nil 3620495242
("" (skeep)
(("" (case "2<3^(1+k) AND 3^(1+k)<6^(1+k)")
(("1" (label "2lem" -1)
(("1" (hide "2lem")
(("1" (rewrite "full_matrix_eq" +)
(("1" (invoke (case "NOT %1") (! 2 1))
(("1" (hide 3)
(("1" (rewrite "rows_mult")
(("1" (assert)
(("1" (lemma "tensor_power_rows_alt")
(("1" (inst?)
(("1" (replaces -1 :dir rl)
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (invoke (case "NOT %1") (! 2 1))
(("1" (hide (-1 3))
(("1" (rewrite "columns_mult")
(("1" (assert) nil nil)
("2" (lemma "tensor_power_rows_alt")
(("2" (inst?)
(("2" (expand "rows" -1 2)
(("2" (expand "length" -1)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (skeep)
(("2" (typepred "j")
(("2" (typepred "i")
(("2" (case "NOT i < 6^(k+1)")
(("1" (assert) nil nil)
("2" (case "NOT j = 0")
(("1" (assert) nil nil)
("2"
(replace -1)
(("2"
(assert)
(("2"
(rewrite "entry_mult")
(("2"
(assert)
(("2"
(lemma "tensor_power_rows_alt")
(("2"
(inst?)
(("2"
(assert)
(("2"
(lemma "dot_eq_sigma")
(("2"
(expand "*" + 1)
(("2"
(rewrite -1 +)
(("2"
(expand
"TQ_vect6k"
+)
(("2"
(rewrite
"entry_form_matrix")
(("1"
(case
"EXISTS (p: upto(k)): base_n(6, i)(p) > 2")
(("1"
(replace -1)
(("1"
(rewrite
"length_row"
+)
(("1"
(rewrite
"length_col"
+)
(("1"
(assert)
(("1"
(lemma
"tensor_power_columns_alt")
(("1"
(inst?)
(("1"
(assert)
(("1"
(replace
-1
:dir
rl)
(("1"
(expand
"min"
+)
(("1"
(case
"NOT columns(A66_inv) = 6")
(("1"
(assert)
nil
nil)
("2"
(replace
-1)
(("2"
(assert)
(("2"
(lemma
"mult_tarski_query_simple_6_above_2")
(("2"
(inst
-
"GF"
"KF"
"base_n(6,i)"
"a"
"k"
"n")
(("1"
(assert)
(("1"
(replace
-4)
(("1"
(replace
-13)
(("1"
(invoke
(case
"%1 = %2")
(!
-1
1)
(!
2
2))
(("1"
(assert)
nil
nil)
("2"
(hide
(-1
3))
(("2"
(rewrite
"sigma_eq")
(("1"
(hide
2)
(("1"
(skosimp*)
(("1"
(case
"FORALL (a1,a2,b1,b2:real): a1=b1 AND a2=b2 IMPLIES a1*a2 = b1*b2")
(("1"
(rewrite
-1
1)
(("1"
(hide
2)
(("1"
(rewrite
"access_row")
(("1"
(lemma
"tensor_entry")
(("1"
(inst?)
(("1"
(assert)
(("1"
(replaces
-1)
(("1"
(expand
"sign_coeff6_zero")
(("1"
(rewrite
"product_eq")
(("1"
(hide
2)
(("1"
(skosimp*)
(("1"
(case
"NOT rows(A66_inv)=6")
(("1"
(assert)
nil
nil)
("2"
(replace
-1)
(("2"
(assert)
(("2"
(replace
-3)
(("2"
(expand
"entry_pick"
+)
(("2"
(case
"NOT FORALL (ii1,jj2:upto(5)): IF ii1 = 0
THEN (IF jj2 >= 3 THEN 0 ELSE 1 ENDIF)
ELSIF ii1 = 1
THEN (IF jj2 = 1 THEN 1
ELSIF jj2 = 2 THEN -1
ELSE 0
ENDIF)
ELSIF ii1 = 2
THEN (IF 1 <= jj2 AND jj2 <= 2
THEN 1
ELSE 0
ENDIF)
ELSIF ii1 = 3
THEN (IF 1 <= jj2 AND jj2 <= 2
THEN -1
ELSIF jj2 = 3 THEN 1
ELSE 0
ENDIF)
ELSIF ii1 = 4
THEN (IF jj2 <= 1 THEN -1
ELSIF jj2 = 4 THEN 1
ELSE 0
ENDIF)
ELSIF ii1 = 5
THEN (IF jj2 = 0 OR jj2 = 2 THEN -1
ELSIF jj2 = 5 THEN 1
ELSE 0
ENDIF)
ELSE 0
ENDIF
= entry(A66_inv)(ii1, jj2)")
(("1"
(hide-all-but
1)
(("1"
(eval-formula)
nil
nil))
nil)
("2"
(expand
"sign_coeff6_zero_entry"
+)
(("2"
(inst
-
"base_n(6,i)(n!2)"
"base_n(6,n!1)(n!2)")
(("1"
(assert)
(("1"
(hide-all-but
1)
(("1"
(lemma
"base_n_lt_n")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(lemma
"base_n_lt_n")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(hide-all-but
1)
(("2"
(lemma
"base_n_lt_n")
(("2"
(inst?)
(("2"
(skeep)
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(rewrite
"access_col")
(("2"
(expand
"NSol_vect6k"
+)
(("2"
(rewrite
"entry_form_matrix")
(("2"
(hide
2)
(("2"
(skosimp*)
(("2"
(lemma
"base_n_lt_n")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(skosimp*)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(skosimp*)
(("2"
(lemma
"base_n_lt_n")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(hide
2)
(("3"
(hide-all-but
1)
(("3"
(skosimp*)
(("3"
(lemma
"base_n_lt_n")
(("3"
(inst?)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but
1)
(("3"
(skosimp*)
(("3"
(lemma
"base_n_lt_n")
(("3"
(inst?)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("4"
(hide-all-but
1)
(("4"
(skosimp*)
(("4"
(lemma
"base_n_lt_n")
(("4"
(inst?)
(("4"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.56 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.
|
