| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/trig_fnd/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle tarski_query_matrix.prf Sprache: Lisp |
|||||||||
|
(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.25 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28