SSL max_seq.prf Sprache: Lisp

(max_seq
(Imax_TCC1 0
  (Imax_TCC1-1 nil 3284470599 ("" (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))
(Imax_TCC2 0
  (Imax_TCC2-1 nil 3284470599 ("" (subtype-tcc) nil nil) nil nil))
(Imax_TCC3 0
  (Imax_TCC3-2 nil 3284470935
   (""
    (inst 1 "(LAMBDA ((s: ne_seqs), (ii: dom(s)), (jj:abv(ii, s))):
                      Imax[length(s),T,<=](seq(s),ii,jj))")
    (("" (skosimp*)
      (("" (typepred "Imax[length(s!1), T, <=](seq(s!1), ii!1, jj!1)")
        (("" (inst -3 "j!1")
          (("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)
    (Imax const-decl
     "{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(j) <= A(i))}"
     max_array_def nil)
    (abv type-eq-decl nil max_array_def nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= formal-const-decl "(total_order?[T])" max_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 max_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 max_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-type-decl nil max_seq nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil)
  (Imax_TCC3-1 nil 3284470599
   (""
    (inst 1 "(LAMBDA ((s: seqs), (ii: dom(s)), (jj:abv(ii, s))):
                    Imax[length(s),T,<=](seq(s),ii,jj))")
    (("" (skosimp*)
      (("" (typepred "Imax[length(s!1), T, <=](seq(s!1), ii!1, jj!1)")
        (("" (inst -3 "j!1")
          (("1" (assert) nil) ("2" (assert) nil))))))))
    nil)
   nil nil))
(Imax_1_TCC1 0
  (Imax_1_TCC1-1 nil 3284470599 ("" (subtype-tcc) nil nil) nil nil))
(Imax_1 0
  (Imax_1-1 nil 3284470599
   ("" (skosimp*)
    (("" (typepred "Imax(s!1, ii!1, ii!1)")
      (("1" (inst?) (("1" (assert) nil) ("2" (assert) nil)))
       ("2" (skosimp*) (("2" (assert) nil))))))
    nil)
   ((Imax const-decl "{i: subrange(ii, jj) |
         (FORALL j: ii <= j AND j <= jj IMPLIES seq(s)(j) <= seq(s)(i))}"
     max_seq nil)
    (<= formal-const-decl "(total_order?[T])" max_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 max_seq nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (dom type-eq-decl nil max_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-type-decl nil max_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))
(imax_TCC1 0
  (imax_TCC1-1 nil 3284470599
   ("" (inst 1 "(LAMBDA s: Imax(s,0,length(s)-1))")
    (("" (skosimp*)
      (("" (typepred "Imax(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)
    (Imax const-decl "{i: subrange(ii, jj) |
         (FORALL j: ii <= j AND j <= jj IMPLIES seq(s)(j) <= seq(s)(i))}"
     max_seq nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (abv type-eq-decl nil max_seq nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= formal-const-decl "(total_order?[T])" max_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil max_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-type-decl nil max_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))
(max_TCC1 0
  (max_TCC1-1 nil 3284470599
   ("" (inst 1 "(LAMBDA s: seq(s)(imax(s)))")
    (("" (skosimp*)
      (("" (prop)
        (("1" (skosimp*)
          (("1" (typepred "imax(s!1)") (("1" (inst?) nil)))))
         ("2" (inst?) nil))))))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (imax const-decl
     "{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(ii) <= seq(s)(i))}"
     max_seq nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (<= formal-const-decl "(total_order?[T])" max_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil max_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-type-decl nil max_seq nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
(max_seq_lem 0
  (max_seq_lem-1 nil 3284470599
   ("" (skosimp*) (("" (typepred "max(s!1)") (("" (inst?) nil)))) nil)
   ((max const-decl "{t: T |
         (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
          (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= formal-const-decl "(total_order?[T])" max_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil max_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-type-decl nil max_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))
(max_seq_in? 0
  (max_seq_in?-1 nil 3284470599
   ("" (skosimp*)
    (("" (expand "in?")
      (("" (typepred "max(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-type-decl nil max_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 max_seq nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" max_seq nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (max const-decl "{t: T |
         (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
          (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq nil))
   nil))
(imax_seq_lem 0
  (imax_seq_lem-1 nil 3284470599
   ("" (skosimp*)
    (("" (typepred "imax(s!1)")
      (("" (typepred "max(s!1)")
        (("" (skosimp*)
          (("" (replace -2 * rl)
            (("" (hide -2)
              (("" (inst?)
                (("" (inst -3 "jj!1")
                  (("" (typepred "max_seq.<=")
                    (("" (expand "total_order?")
                      (("" (expand "partial_order?")
                        (("" (flatten)
                          (("" (expand "antisymmetric?")
                            (("" (inst?)
                              ((""
                                (assert)
                                nil))))))))))))))))))))))))))))
    nil)
   ((imax const-decl
     "{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(ii) <= seq(s)(i))}"
     max_seq nil)
    (<= formal-const-decl "(total_order?[T])" max_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil max_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-type-decl nil max_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)
    (max const-decl "{t: T |
         (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
          (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq nil))
   nil))
(max_seq_def 0
  (max_seq_def-1 nil 3284470599
   ("" (skosimp*)
    (("" (prop)
      (("1" (lemma "max_seq_lem") (("1" (inst?) nil)))
       ("2" (rewrite "max_seq_in?") nil))))
    nil)
   ((dom type-eq-decl nil max_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-type-decl nil max_seq nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (max_seq_lem formula-decl nil max_seq nil)
    (max_seq_in? formula-decl nil max_seq nil))
   nil))
(max_seq_it_is 0
  (max_seq_it_is-1 nil 3284470599
   ("" (skosimp*)
    (("" (typepred "max(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)
   ((max const-decl "{t: T |
         (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
          (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= formal-const-decl "(total_order?[T])" max_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil max_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-type-decl nil max_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))
(imax_seq_1 0
  (imax_seq_1-1 nil 3284470599
   ("" (skosimp*) (("" (typepred "imax(s!1)") (("" (assert) nil))))
    nil)
   ((imax const-decl
     "{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(ii) <= seq(s)(i))}"
     max_seq nil)
    (<= formal-const-decl "(total_order?[T])" max_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil max_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-type-decl nil max_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))
(max_seq_2_TCC1 0
  (max_seq_2_TCC1-1 nil 3284470599 ("" (subtype-tcc) nil nil) nil nil))
(max_seq_2_TCC2 0
  (max_seq_2_TCC2-1 nil 3284470599 ("" (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-type-decl nil max_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))
(max_seq_2 0
  (max_seq_2-1 nil 3284470599
   ("" (skosimp*)
    (("" (typepred "max(s!1)")
      (("" (skosimp*)
        (("" (replace -2 * rl)
          (("" (hide -2)
            (("" (inst-cp -1 "0")
              (("" (inst -1 "1")
                (("1" (lift-if)
                  (("1" (ground)
                    (("1" (case-replace "jj!1 = 0 OR jj!1 = 1")
                      (("1" (typepred "max_seq.<=")
                        (("1" (expand "total_order?")
                          (("1" (expand "partial_order?")
                            (("1" (flatten)
                              (("1"
                                (expand "antisymmetric?")
                                (("1"
                                  (inst?)
                                  (("1" (assert) nil)))))))))))))
                       ("2" (hide -1 -2 -3 2)
                        (("2" (typepred "jj!1")
                          (("2" (ground) nil)))))))))))
                 ("2" (assert) nil))))))))))))))
    nil)
   ((max const-decl "{t: T |
         (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
          (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= formal-const-decl "(total_order?[T])" max_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil max_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-type-decl nil max_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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (antisymmetric? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (s!1 skolem-const-decl "ne_seqs[T]" max_seq nil))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.