(sigma_vector (connected_domain 0 (connected_domain-1 nil 3521046835 ("" (skosimp) (("" (grind) (("" (grind) (("" (postpone) nil nil )) nil )) nil )) nil ) nil shostak)) (low_TCC1 0 (tcc "tcc" 3489915882 ("" (skosimp) (("" (lemma "connected_domain" ) (("" (inst -1 "x!1" "y!1" "z!1" ) (("" (assert ) nil nil )) nil )) nil )) nil ) ((connected_domain formula-decl nil sigma_vector nil ) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil ) (integer nonempty-type-from-decl nil integers nil ) (T formal-subtype-decl nil sigma_vector nil ) (T_pred const-decl "[int -> boolean]" sigma_vector 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 )) shostak) (low_TCC1-1 nil 3489915779 ("" (assuming-tcc) nil nil ) nil nil )) (oh_TCC1 0 (oh_TCC1-1 nil 3518275428 ("" 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 ) (= const-decl "[T, T -> boolean]" equalities nil ) (posnat nonempty-type-eq-decl nil integers nil ) (Vector type-eq-decl nil vectors "vectors/" ) (Maping type-eq-decl nil linear_map nil ) (AND const-decl "[bool, bool -> bool]" 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 ) (>= const-decl "bool" reals nil ) (nonneg_int nonempty-type-eq-decl nil integers nil ) (> const-decl "bool" reals nil ) (n formal-const-decl "posnat" sigma_vector nil ) (Map type-eq-decl nil linear_map nil ) (T_pred const-decl "[int -> boolean]" sigma_vector nil ) (T formal-subtype-decl nil sigma_vector nil ) (nat nonempty-type-eq-decl nil naturalnumbers 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 )) nil )) (oh_TCC2 0 (oh_TCC2-1 nil 3518275428 ("" (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 ) (= const-decl "[T, T -> boolean]" equalities nil ) (posnat nonempty-type-eq-decl nil integers nil ) (Vector type-eq-decl nil vectors "vectors/" ) (Maping type-eq-decl nil linear_map nil ) (AND const-decl "[bool, bool -> bool]" 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 ) (>= const-decl "bool" reals nil ) (nonneg_int nonempty-type-eq-decl nil integers nil ) (> const-decl "bool" reals nil ) (n formal-const-decl "posnat" sigma_vector nil ) (Map type-eq-decl nil linear_map nil ) (T_pred const-decl "[int -> boolean]" sigma_vector nil ) (T formal-subtype-decl nil sigma_vector nil ) (nat nonempty-type-eq-decl nil naturalnumbers 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 )) nil )) (SigmaV_last_TCC1 0 (thm "fin" 3546879131 ("" (skosimp) (("" (typepred "high!1" ) (("" (case " T_pred(high!1)" ) (("1" (inst 2 "high!1" ) (("1" (assert ) nil nil )) nil ) ("2" (case "(EXISTS (j: T): high!1 <= j)" ) (("1" (skosimp) (("1" (grind) nil nil )) nil ) ("2" (assert ) nil nil )) nil )) nil )) nil )) nil ) ((T_high type-eq-decl nil sigma "reals/" ) (<= const-decl "bool" reals nil ) (T formal-subtype-decl nil sigma_vector nil ) (T_pred const-decl "[int -> boolean]" sigma_vector 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 ) (OR const-decl "[bool, bool -> bool]" booleans nil ) (NOT const-decl "[bool -> bool]" booleans nil ) (bool nonempty-type-eq-decl nil booleans nil ) (boolean nonempty-type-decl nil booleans nil ) (high!1 skolem-const-decl "T_high[T]" sigma_vector nil ) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil ) (int_minus_int_is_int application-judgement "int" integers nil ) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil )) shostak) (SigmaV_last_TCC1-1 nil 3546878969 ("" (subtype-tcc) nil nil ) ((T_high type-eq-decl nil sigma "reals/" )) nil )) (SigmaV_last_TCC2 0 (thm "fin" 3546879358 ("" (skosimp) (("" (typepred "high!1" ) (("" (typepred "low!1" ) (("" (grind) (("1" (lemma "connected_domain" ) (("1" (inst -1 "low!1" "j!1" "high!1" ) (("1" (assert ) nil nil )) nil )) nil ) ("2" (lemma "connected_domain" ) (("2" (typepred "low!1" ) (("2" (inst -2 "j!1" "j!2" "high!1" ) (("2" (assert ) nil nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil ) ((T_high type-eq-decl nil sigma "reals/" ) (<= const-decl "bool" reals nil ) (T formal-subtype-decl nil sigma_vector nil ) (T_pred const-decl "[int -> boolean]" sigma_vector 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]" 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 ) (OR const-decl "[bool, bool -> bool]" booleans nil ) (NOT const-decl "[bool -> bool]" booleans nil ) (bool nonempty-type-eq-decl nil booleans nil ) (boolean nonempty-type-decl nil booleans nil ) (real_ge_is_total_order name-judgement "(total_order?[real])" nil ) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil ) (integer nonempty-type-from-decl nil integers nil ) (connected_domain formula-decl nil sigma_vector nil ) (T_low type-eq-decl nil sigma "reals/" )) shostak) (SigmaV_last_TCC2-1 nil 3546878969 ("" (subtype-tcc) nil nil ) ((T_high type-eq-decl nil sigma "reals/" ) (T_low type-eq-decl nil sigma "reals/" )) nil )) (SigmaV_last 0 (SigmaV_last-1 nil 3546883946 ("" (skosimp) (("" (expand "SigmaV" ) (("" (apply-extensionality) (("1" (hide 2) (("1" (expand "+" ) (("1" (lemma "sigma_last[T]" ) (("1" (inst -1 "LAMBDA (j: T): F!1(j)(x!1)" "high!1" "low!1" ) (("1" (assert ) nil nil )) nil )) nil )) nil )) nil ) ("2" (skosimp) (("2" (typepred "high!1" ) (("2" (case " T_pred(high!1)" ) (("1" (inst 2 "high!1" ) (("1" (assert ) nil nil nil ) ("2" (case " (EXISTS (j: T): high!1 <= j)" ) (("1" (skosimp) (("1" (inst 3 "j!1" ) (("1" (assert nil nil )) nil )) nil ) ("2" (assert ) nil nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil ) ((SigmaV const-decl "Vector[n]" sigma_vector nil ) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil ) (NOT const-decl "[bool -> bool]" booleans nil ) (sigma_last formula-decl nil sigma "reals/" ) (real_plus_real_is_real application-judgement "real" reals nil ) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil ) (int_minus_int_is_int application-judgement "int" integers nil ) (high!1 skolem-const-decl "T_high[T]" sigma_vector nil ) (T_high type-eq-decl nil sigma "reals/" ) (<= const-decl "bool" reals nil ) (T formal-subtype-decl nil sigma_vector nil ) (- const-decl "[numfield, numfield -> numfield]" number_fields nil ) (numfield nonempty-type-eq-decl nil number_fields nil ) (T_pred const-decl "[int -> boolean]" sigma_vector nil ) (OR const-decl "[bool, bool -> bool]" booleans nil ) (T_low type-eq-decl nil sigma "reals/" ) (sigma def-decl "real" sigma "reals/" ) (Index type-eq-decl nil vectors "vectors/" ) (Vector type-eq-decl nil vectors "vectors/" ) (+ const-decl "real" vectors "vectors/" ) (below type-eq-decl nil nat_types nil ) (n formal-const-decl "posnat" sigma_vector nil ) (posnat nonempty-type-eq-decl nil integers nil "bool" reals nil ) (nonneg_int nonempty-type-eq-decl nil integers 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 -> boolean]" number_fields nil ) (boolean nonempty-type-decl nil booleans nil ) (number nonempty-type-decl nil numbers nil )) shostak)) (SigmaV_scal 0 (thm "finished" 3546764749 ("" (skosimp) (("" (case "p!1>m!1" ) (("1" (expand "SigmaV" ) (("1" (expand "sigma" ) (("1" (replace -1) (("1" (expand "*" ) (("1" (propax) nil nil )) nil )) nil )) nil )) nil ) ("2" (case "p!1=m!1" ) (("1" (hide 1) (("1" (replace -1) (("1" (expand "SigmaV" ) (("1" (expand "sigma" ) (("1" (expand "sigma" ) (("1" (apply-extensionality) (("1" (hide 2) (("1" (expand "*" ) (("1" (expand "*" ) (("1" (propax) nil nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil ) ("2" (case "p!1) (("1" (hide 1 2) (("1" (expand "SigmaV" ) (("1" (lemma "sigma_scal[T]" ) (("1" (apply-extensionality) (("1" (hide 2) (("1" (inst -1 "LAMBDA (j: T): F!1(j)(x!1)" "a!1" "m!1" "p!1" ) (("1" (case " sigma(p!1, m!1, LAMBDA (i: T): a!1 * F!1(i)(x!1))= sigma(p!1, m!1, LAMBDA (j: T): (a!1 * F!1)(j)(x!1))" ) (("1" (replace -1 -2) (("1" replace -2 1) (("1" (hide -1 -2) (("1" (expand "*" ) (("1" (propax) nil nil )) nil )) nil )) nil )) nil ) ("2" (hide -1 2) (("2" (expand "*" ) (("2" (expand "*" ) (("2" (propax) nil nil )) nil )) nil )) nil nil )) nil )) nil )) nil )) nil )) nil )) nil ) ("2" (assert ) nil nil )) nil )) nil )) nil )) nil ) ((T formal-subtype-decl nil sigma_vector nil ) (T_pred const-decl "[int -> boolean]" sigma_vector 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 ) (sigma def-decl "real" sigma "reals/" ) (* const-decl "Vector" vectors "vectors/" ) (SigmaV const-decl "Vector[n]" sigma_vector nil ) (T_high type-eq-decl nil sigma "reals/" ) (T_low type-eq-decl nil sigma "reals/" ) (<= const-decl "bool" reals nil ) (OR const-decl "[bool, bool -> bool]" booleans nil ) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil ) (* const-decl "[numfield, numfield -> numfield]" number_fields nil ) (real_times_real_is_real application-judgement "real" reals nil ) (sigma_scal formula-decl nil sigma "reals/" ) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil ) (Index type-eq-decl nil vectors "vectors/" ) (Vector type-eq-decl nil vectors "vectors/" ) (* const-decl "[real, [T -> Vector[n]] -> [T -> Vector[n]]]" sigma_vector nil ) (numfield nonempty-type-eq-decl nil number_fields nil ) (below type-eq-decl nil nat_types nil ) (n formal-const-decl "posnat" sigma_vector nil ) (posnat nonempty-type-eq-decl nil integers nil ) (nonneg_int nonempty-type-eq-decl nil integers nil "bool" reals nil ) (nat nonempty-type-eq-decl nil naturalnumbers nil ) (>= const-decl "bool" reals nil ) (= const-decl "[T, T -> boolean]" equalities nil )) shostak) (SigmaV_scal-1 nil 3546675674 ("" (skosimp) (("" (case "p!1>m!1" ) (("1" (expand "SigmaV" ) (("1" (expand "sigma" ) (("1" (replace -1) (("1" (expand "*" ) (("1" (propax) nil nil )) nil )) nil )) nil )) nil "2" (case "p!1=m!1" ) (("1" (hide 1) (("1" (replace -1) (("1" (expand "SigmaV" ) (("1" (expand "sigma" ) (("1" (expand "sigma" ) (("1" (apply-extensionality) (("1" (hide 2) (("1" (expand "*" ) (("1" (expand "*" ) (("1" (propax) nil nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil ) ("2" (case "p!1) (("1" (hide 1 2) (("1" (expand "SigmaV" ) (("1" (lemma "sigma_scal[T]" ) (("1" (apply-extensionality) (("1" (hide 2) (("1" (inst -1 "LAMBDA (j: T): F!1(j)(x!1)" "a!1" "m!1" "p!1" ) (("1" (case " sigma(p!1, m!1, LAMBDA (i: T): a!1 * F!1(i)(x!1))= sigma(p!1, m!1, LAMBDA (j: T): (a!1 * F!1)(j)(x!1))" ) (("1" (replace -1 -2) (("1" (replace -2 1) (("1" (hide -1 -2) (("1" (postpone) nil nil )) nil )) nil )) nil ) ("2" (hide -1 2) (("2" (expand "*" ) (("2" (expand "*" ) (("2" (propax) nil nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil )) nil ) ("2" (assert ) nil nil )) nil )) nil )) nil )) nil ) ((Vector type-eq-decl nil vectors "vectors/" ) (Index type-eq-decl nil vectors "vectors/" ) (sigma_scal formula-decl nil sigma "reals/" ) (T_low type-eq-decl nil sigma "reals/" ) (T_high type-eq-decl nil sigma "reals/" ) (* const-decl "Vector" vectors "vectors/" ) (sigma def-decl "real" sigma "reals/" )) shostak)))quality 100%
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
