| products/Sources/formale Sprachen/PVS/structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: min_seq.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(min_seq
(Imin_TCC1 0 (Imin_TCC1-1 nil 3284470600 ("" (skosimp*) (("" (assert) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (Imin_TCC2 0 (Imin_TCC2-1 nil 3284470600 ("" (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) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (T formal-nonempty-type-decl nil min_seq nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs nil) (< const-decl "bool" 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) (dom type-eq-decl nil min_seq nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (abv type-eq-decl nil min_seq nil) (subrange type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (Imin_TCC3 0 (Imin_TCC3-2 nil 3284470891 ("" (inst 1 "(LAMBDA ((s: ne_seqs), (ii: dom(s)), (jj:abv(ii, s))): Imin[length(s),T,<=](seq(s),ii,jj))") (("" (skosimp*) (("" (typepred "Imin[length(s!1), T, <=](seq(s!1), ii!1, jj!1)") (("" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (Imin const-decl "{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(i) <= A(j))}" min_array_def nil) (abv type-eq-decl nil min_array_def nil) (below type-eq-decl nil naturalnumbers nil) (<= formal-const-decl "(total_order?[T])" min_seq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (abv type-eq-decl nil min_seq nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (dom type-eq-decl nil min_seq nil) (ne_seqs type-eq-decl nil seqs 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) (finite_sequence type-eq-decl nil finite_sequences nil) (T formal-nonempty-type-decl nil min_seq nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil) (Imin_TCC3-1 nil 3284470600 ("" (inst 1 "(LAMBDA ((s: seqs), (ii: dom(s)), (jj:abv(ii, s))): Imin[length(s),T,<=](seq(s),ii,jj))") (("" (skosimp*) (("" (typepred "Imin[length(s!1), T, <=](seq(s!1), ii!1, jj!1)") (("" (inst?) (("1" (assert) nil) ("2" (assert) nil)))))))) nil) nil nil)) (Imin_seq_1_TCC1 0 (Imin_seq_1_TCC1-1 nil 3284470600 ("" (subtype-tcc) nil nil) nil nil)) (Imin_seq_1 0 (Imin_seq_1-1 nil 3284470600 ("" (skosimp*) (("" (typepred "Imin(s!1, ii!1, ii!1)") (("1" (inst?) (("1" (assert) nil) ("2" (assert) nil))) ("2" (skosimp*) (("2" (assert) nil)))))) nil) ((Imin const-decl "{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES seq(s)(i) <= seq(s)(j))}" min_seq nil) (<= formal-const-decl "(total_order?[T])" min_seq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (abv type-eq-decl nil min_seq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (dom type-eq-decl nil min_seq nil) (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (T formal-nonempty-type-decl nil min_seq nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals 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) (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (imin_TCC1 0 (imin_TCC1-1 nil 3284470600 ("" (inst 1 "(LAMBDA s: Imin(s,0,length(s)-1))") (("" (skosimp*) (("" (typepred "Imin(s!1, 0, length(s!1) - 1)") (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil))))))) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil)))))))))) nil) ((real_le_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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Imin const-decl "{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES seq(s)(i) <= seq(s)(j))}" min_seq nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (abv type-eq-decl nil min_seq nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= formal-const-decl "(total_order?[T])" min_seq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (dom type-eq-decl nil min_seq nil) (< const-decl "bool" reals 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) (ne_seqs type-eq-decl nil seqs 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) (finite_sequence type-eq-decl nil finite_sequences nil) (T formal-nonempty-type-decl nil min_seq nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (min_TCC1 0 (min_TCC1-1 nil 3284470600 ("" (inst 1 "(LAMBDA s: seq(s)(imin(s)))") (("" (skosimp*) (("" (prop) (("1" (skosimp*) (("1" (typepred "imin(s!1)") (("1" (inst?) nil))))) ("2" (inst?) nil)))))) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (imin const-decl "{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(i) <= seq(s)(ii))}" min_seq nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= formal-const-decl "(total_order?[T])" min_seq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (dom type-eq-decl nil min_seq nil) (< const-decl "bool" reals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (ne_seqs type-eq-decl nil seqs 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) (finite_sequence type-eq-decl nil finite_sequences nil) (T formal-nonempty-type-decl nil min_seq nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (min_seq_lem 0 (min_seq_lem-1 nil 3284470600 ("" (skosimp*) (("" (typepred "min(s!1)") (("" (inst?) nil)))) nil) ((min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= formal-const-decl "(total_order?[T])" min_seq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (dom type-eq-decl nil min_seq nil) (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (T formal-nonempty-type-decl nil min_seq nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals 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)) nil)) (min_seq_in? 0 (min_seq_in?-1 nil 3284470600 ("" (skosimp*) (("" (expand "in?") (("" (typepred "min(s!1)") (("" (skosimp*) (("" (hide -1) (("" (inst?) (("" (assert) nil)))))))))))) nil) ((in? const-decl "bool" seqs nil) (below type-eq-decl nil naturalnumbers 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) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (T formal-nonempty-type-decl nil min_seq nil) (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (ne_seqs type-eq-decl nil seqs nil) (dom type-eq-decl nil min_seq nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" min_seq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq nil)) nil)) (min_seq_def 0 (min_seq_def-1 nil 3284470600 ("" (skosimp*) (("" (prop) (("1" (rewrite "min_seq_lem") nil) ("2" (rewrite "min_seq_in?") nil)))) nil) ((dom type-eq-decl nil min_seq nil) (< const-decl "bool" reals 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) (ne_seqs type-eq-decl nil seqs 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) (finite_sequence type-eq-decl nil finite_sequences nil) (T formal-nonempty-type-decl nil min_seq nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (min_seq_lem formula-decl nil min_seq nil) (min_seq_in? formula-decl nil min_seq nil)) nil)) (min_seq_it_is 0 (min_seq_it_is-1 nil 3284470600 ("" (skosimp*) (("" (typepred "min(s!1)") (("" (expand "in?") (("" (skosimp*) (("" (replace -2 * rl) (("" (hide -2) (("" (replace -3) (("" (hide -3) (("" (inst?) (("" (inst -2 "jj!1") (("" (typepred "<=") (("" (expand "total_order?") (("" (expand "partial_order?") (("" (flatten) (("" (expand "antisymmetric?") (("" (inst?) (("" (assert) nil)))))))))))))))))))))))))))))))) nil) ((min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= formal-const-decl "(total_order?[T])" min_seq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (dom type-eq-decl nil min_seq nil) (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (T formal-nonempty-type-decl nil min_seq nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals 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) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (below type-eq-decl nil naturalnumbers nil) (in? const-decl "bool" seqs nil)) nil)) (imin_seq_lem 0 (imin_seq_lem-1 nil 3284470600 ("" (skosimp*) (("" (typepred "imin(s!1)") (("" (typepred "min(s!1)") (("" (skosimp*) (("" (replace -2 * rl) (("" (hide -2) (("" (inst?) (("" (inst -3 "jj!1") (("" (typepred "min_seq.<=") (("" (expand "total_order?") (("" (expand "partial_order?") (("" (flatten) (("" (expand "antisymmetric?") (("" (inst?) (("" (assert) nil)))))))))))))))))))))))))))) nil) ((imin const-decl "{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(i) <= seq(s)(ii))}" min_seq nil) (<= formal-const-decl "(total_order?[T])" min_seq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (dom type-eq-decl nil min_seq 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) (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (T formal-nonempty-type-decl nil min_seq nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq nil)) nil)) (imin_seq_1 0 (imin_seq_1-1 nil 3284470600 ("" (skosimp*) (("" (typepred "imin(s!1)") (("" (assert) nil)))) nil) ((imin const-decl "{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(i) <= seq(s)(ii))}" min_seq nil) (<= formal-const-decl "(total_order?[T])" min_seq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (dom type-eq-decl nil min_seq 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) (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (T formal-nonempty-type-decl nil min_seq nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (min_seq_2_TCC1 0 (min_seq_2_TCC1-1 nil 3284470600 ("" (subtype-tcc) nil nil) nil nil)) (min_seq_2_TCC2 0 (min_seq_2_TCC2-1 nil 3284470600 ("" (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) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (T formal-nonempty-type-decl nil min_seq nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (min_seq_2 0 (min_seq_2-1 nil 3284470600 ("" (skosimp*) (("" (typepred "min(s!1)") (("" (skosimp*) (("" (replace -2 * rl) (("" (hide -2) (("" (inst-cp -1 "0") (("" (inst -1 "1") (("1" (lift-if) (("1" (ground) (("1" (typepred "jj!1") (("1" (case-replace "jj!1 = 0 OR jj!1 = 1") (("1" (prop) (("1" (assert) nil) ("2" (replace -1) (("2" (hide -1) (("2" (typepred "min_seq.<=") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (flatten) (("2" (expand "antisymmetric?") (("2" (inst?) (("2" (assert) nil))))))))))))))))))) ("2" (assert) nil))))))))) ("2" (assert) nil)))))))))))))) nil) ((min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= formal-const-decl "(total_order?[T])" min_seq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (dom type-eq-decl nil min_seq nil) (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (T formal-nonempty-type-decl nil min_seq nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (s!1 skolem-const-decl "ne_seqs[T]" min_seq nil)) nil))) ¤ Dauer der Verarbeitung: 0.7 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 |
