| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 218 kB |
|
SSL sort_fseq.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(sort_fseq (sort_TCC1 0 (sort_TCC1-2 nil 3559142815 ("" (inst 1 "(LAMBDA s: (# length := length(s), seq := (LAMBDA (n: nat): IF n < length(s) THEN sort[length(s),T,<=](seq_to_array(s))(n) ELSE default ENDIF) #))") (("1" (skosimp*) (("1" (prop) (("1" (typepred "sort[length(s!1), T, <=](seq_to_array(s!1))") (("1" (expand "permutation_of?") (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst + "f!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sort[length(s!1), T, <=](seq_to_array(s!1))") (("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil nat_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (default const-decl "T" fseqs nil) (seq_to_array const-decl "below_array[length(s), T]" sort_fseq nil) (below_array type-eq-decl nil below_arrays nil) (sort const-decl "{a | permutation_of?(A, a) AND sorted?(a)}" sort_array nil) (sorted? const-decl "bool" sort_array nil) (permutation_of? const-decl "bool" permutations nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def 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) (increasing? const-decl "bool" sort_fseq nil) (permutation? const-decl "bool" permutations_fseq nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (fsq type-eq-decl nil fsq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (T formal-nonempty-type-decl nil sort_fseq nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil) (sort_TCC1-1 nil 3280843647 ("" (skosimp*) (("" (typepred "ss!1") (("" (inst + "ss!1(0)") nil nil)) nil)) nil) ((barray type-eq-decl nil fseqs nil) (fseq type-eq-decl nil fseqs nil)) nil)) (sort_length 0 (sort_length-1 nil 3280843647 ("" (skosimp*) (("" (typepred "sort(s!1)") (("" (lemma "perm_length[T,<=]") (("" (inst -1 "s!1" "sort(s!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq nil) (increasing? const-decl "bool" sort_fseq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (permutation? const-decl "bool" permutations_fseq nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (fsq type-eq-decl nil fsq nil) (T formal-nonempty-type-decl nil sort_fseq nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (perm_length formula-decl nil permutations_fseq nil)) nil)) (sort_fseq_lem 0 (sort_fseq_lem-1 nil 3280843647 ("" (skosimp*) (("" (typepred "sort(s!1)") (("" (assert) nil nil)) nil)) nil) ((sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq nil) (increasing? const-decl "bool" sort_fseq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (permutation? const-decl "bool" permutations_fseq nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (fsq type-eq-decl nil fsq nil) (T formal-nonempty-type-decl nil sort_fseq nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (sort_fseq_in? 0 (sort_fseq_in?-1 nil 3281101912 ("" (skosimp*) (("" (expand "in?") (("" (typepred "sort(s!1)") (("" (expand "permutation?") (("" (skosimp*) (("" (prop) (("1" (skosimp*) (("1" (inst? -) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -1) (("2" (typepred "ii!1") (("2" (inst - "inverse(f!1)(ii!1)") (("1" (case-replace "f!1(inverse(f!1)(ii!1)) = ii!1") (("1" (inst + "inverse(f!1)(ii!1)") (("1" (assert) nil nil) ("2" (assert) (("2" (inst + "ii!1") nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "comp_inverse_right[below(length(s!1)),below(length(sort(s!1)))]") (("1" (inst - "ii!1" "f!1") nil nil) ("2" (assert) (("2" (hide 2) (("2" (inst + "ii!1") nil nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (inst + "ii!1") nil nil)) nil)) nil) ("2" (assert) (("2" (inst + "ii!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((in? const-decl "bool" fsq 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (s!1 skolem-const-decl "fseq[T]" sort_fseq nil) (TRUE const-decl "bool" booleans nil) (inverse const-decl "D" function_inverse nil) (bijective? const-decl "bool" functions nil) (f!1 skolem-const-decl "[below(length(s!1)) -> below(length(sort(s!1)))]" sort_fseq nil) (comp_inverse_right formula-decl nil function_inverse nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sort_length formula-decl nil sort_fseq nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil sort_fseq nil) (fsq type-eq-decl nil fsq nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (permutation? const-decl "bool" permutations_fseq nil) (barray type-eq-decl nil fseqs nil) (fseq type-eq-decl nil fseqs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (increasing? const-decl "bool" sort_fseq nil) (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq nil)) nil)) (sort_fseq_in 0 (sort_fseq_in-1 nil 3280843667 ("" (skosimp*) (("" (lemma "sort_fseq_in?") (("" (inst - "s!1" "_") (("" (inst - "seq(sort(s!1))(ii!1)") (("" (assert) (("" (hide 2) (("" (expand "in?") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sort_fseq_in? formula-decl nil sort_fseq nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fsq type-eq-decl nil fsq nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (permutation? const-decl "bool" permutations_fseq nil) (increasing? const-decl "bool" sort_fseq nil) (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (sort_length formula-decl nil sort_fseq nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (in? const-decl "bool" fsq nil) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (T formal-nonempty-type-decl nil sort_fseq nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (sort_fseq_in2 0 (sort_fseq_in2-1 nil 3281102536 ("" (skosimp*) (("" (lemma "sort_fseq_in?") (("" (inst - "s!1" "seq(s!1)(ii!1)") (("" (assert) (("" (hide 2) (("" (expand "in?") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sort_fseq_in? formula-decl nil sort_fseq nil) (in? const-decl "bool" fsq nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (T formal-nonempty-type-decl nil sort_fseq nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (sort_fseq_lt 0 (sort_fseq_lt-1 nil 3440778026 ("" (skosimp*) (("" (typepred "sort(s!1)") (("" (expand "<") (("" (flatten) (("" (expand "increasing?") (("" (inst - "j!1" "i!1") (("" (assert) (("" (typepred "<=") (("" (expand "total_order?") (("" (flatten) (("" (expand "partial_order?") (("" (flatten) (("" (expand "antisymmetric?") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq nil) (increasing? const-decl "bool" sort_fseq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (permutation? const-decl "bool" permutations_fseq nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (fsq type-eq-decl nil fsq nil) (T formal-nonempty-type-decl nil sort_fseq nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (sort_length formula-decl nil sort_fseq nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sort_singleton 0 (sort_singleton-1 nil 3473181323 ("" (skeep) (("" (lemma "singleton_length") (("" (inst - "sort(singleton(x))") (("" (ground) (("1" (expand "singleton?") (("1" (skosimp*) (("1" (replace -1) (("1" (typepred "sort(singleton(x))") (("1" (expand "permutation?") (("1" (skosimp*) (("1" (inst - "0") (("1" (expand "bijective?") (("1" (flatten) (("1" (expand "surjective?") (("1" (inst - "0") (("1" (skosimp*) (("1" (case "x!2 = 0") (("1" (replace -1) (("1" (hide -1) (("1" (replace -2) (("1" (replace -5) (("1" (expand "singleton" -3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-type-decl nil sort_fseq nil) (singleton_length formula-decl nil fseqs nil) (sort_length formula-decl nil sort_fseq nil) (NOT const-decl "[bool -> bool]" booleans nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (= const-decl "[T, T -> boolean]" equalities 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (singleton? const-decl "bool" fseqs nil) (singleton const-decl "ne_fseq" fseqs nil) (ne_fseq type-eq-decl nil fseqs 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) (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq nil) (increasing? const-decl "bool" sort_fseq nil) (permutation? const-decl "bool" permutations_fseq nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (fsq type-eq-decl nil fsq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (member_sort 0 (member_sort-1 nil 3473182956 ("" (skeep) (("" (expand "member") (("" (typepred "sort(s)") (("" (expand "permutation?") (("" (skosimp*) (("" (expand "bijective?") (("" (flatten) (("" (label "surj" -2) (("" (label "inj" -1) (("" (ground) (("1" (skosimp*) (("1" (inst - "i!1") (("1" (inst + "f!1(i!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "surjective?") (("2" (inst - "i!1") (("2" (skosimp*) (("2" (inst - "x!1") (("2" (inst + "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" fseqs nil) (bijective? const-decl "bool" functions 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (surjective? const-decl "bool" functions nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil sort_fseq nil) (fsq type-eq-decl nil fsq nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (permutation? const-decl "bool" permutations_fseq nil) (barray type-eq-decl nil fseqs nil) (fseq type-eq-decl nil fseqs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (increasing? const-decl "bool" sort_fseq nil) (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq nil)) shostak)) (strictly_sort_TCC1 0 (strictly_sort_TCC1-1 nil 3490977275 ("" (case "FORALL (n:nat): (FORALL (s:fseq[T]): increasing?(s) and s`length=n IMPLIES (EXISTS (("1" (name "xit" "LAMBDA (szz:fseq[T]): choose({ss: fseq[T] | strictly_increasing?(ss) AND (FORALL (x: T): member[T](x, szz) IFF member[T](x, ss))})") (("1" (inst + "xit") nil nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst -2 "szz`length") (("2" (inst -2 "sort(szz)") (("2" (assert) (("2" (lemma "sort_length") (("2" (inst -1 "szz") (("2" (assert) (("2" (skosimp*) (("2" (inst - "sis!1") (("2" (expand "member") (("2" (assert) (("2" (skosimp*) (("2" (lemma "member_sort") (("2" (inst - "szz" "x!1") (("2" (expand "member") (("2" (inst - "x!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skeep) (("1" (inst + "s") (("1" (assert) (("1" (expand "strictly_increasing?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (label "increasings" -2) (("2" (copy "increasings") (("2" (label "sincreasing" -1) (("2" (hide "sincreasing") (("2" (label "slength" -3) (("2" (case "NOT j > 0") (("1" (case "j = 0") (("1" (replace -1) (("1" (inst + "s") (("1" (assert) (("1" (expand "strictly_increasing?") (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (name "slow" "(# length := j, seq := (LAMBDA (pq:nat): IF pq < j THEN s`seq(pq) ELSE default ENDIF) #)") (("2" (label "slowname" -1) (("2" (label "sisfact" -3) (("2" (inst - "slow") (("1" (assert) (("1" (case "increasing?(slow)") (("1" (label "slowincreasing" -1) (("1" (assert) (("1" (skosimp*) (("1" (label "sisincreasing" -4) (("1" (case "NOT s`seq(j) = s`seq(j-1)") (("1" (name "stop" "(# length := sis!1`length+1, seq := (LAMBDA (pq:nat): IF pq < sis!1`length THEN sis!1`seq(pq) (("1" (label "stopname" -1) (("1" (inst + "stop") (("1" (split 2) (("1" (expand "strictly_increasing?") (("1" (skosimp*) (("1" (case "j!1 < sis!1`length") (("1" (inst - "i!1" "j!1") (("1" (assert) (("1" (flatten) (("1" (case "seq(stop)(i!1) = seq(sis!1)(i!1) AND seq(stop)(j!1) = seq(sis!1)(j!1)") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (expand "stop" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1 = sis!1`length") (("1" (case "seq(stop)(j!1) = s`seq(j)") (("1" (replace -1) (("1" (assert) (("1" (expand "stop" +) (("1" (inst "sisfact" "sis!1`seq(i!1)") (("1" (case "member(sis!1`seq(i!1), sis!1)") (("1" (assert) (("1" (expand "member") (("1" (skosimp*) (("1" (replace "sisfact") (("1" (expand "slow" +) (("1" (expand "increasing?" "increasings") (("1" (inst "increasings" "i!3" "j") (("1" (assert) (("1" (replace -12) (("1" (reveal "sincreasing") (("1" (expand "increasing?" "sincreasing") (("1" (copy "sincreasing") (("1" (case "s`seq(i!3) <= s`seq(j-1) AND s`seq(j-1) <= s`seq(j)") (("1" (flatten) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (flatten) (("1" (expand "partial_order?") (("1" (flatten) (("1" (expand "antisymmetric?") (("1" (inst - "s`seq(j-1)" "s`seq(j)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "i!3" "j-1") (("2" (assert) (("2" (assert) (("2" (inst - "j-1" "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "stop" 1) (("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "member" +) (("2" (expand "stop" +) (("2" (assert) (("2" (ground) (("1" (skosimp*) (("1" (replace -1) (("1" (case "i!1 = j") (("1" (replace -1) (("1" (assert) (("1" (inst + "sis!1`length") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (copy "sisfact") (("2" (inst -1 "x!1") (("2" (case "member(x!1,slow)") (("1" (assert) (("1" (expand "member" -2) (("1" (skosimp*) (("1" (replace -3 :dir rl) (("1" (replace -2) (("1" (inst + "i!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member" 1) (("2" (inst + "i!1") (("1" (assert) (("1" (expand "slow" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lift-if) (("2" (case "i!1 < sis!1`length") (("1" (assert) (("1" (copy "sisfact") (("1" (inst - "x!1") (("1" (case "member(x!1,sis!1)") (("1" (assert) (("1" (expand "member" -2) (("1" (skosimp*) (("1" (inst + "i!2") (("1" (replace -2) (("1" (expand "slow" +) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -3) (("2" (expand "member") (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst + "j") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (assert) (("2" (expand "stop" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "sis!1") (("2" (assert) (("2" (skosimp*) (("2" (case "FORALL (x:T): member(x,slow) IFF member(x,s)") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (ground) nil nil)) nil)) nil) ("2" (hide-all-but (-1 "slowname" 1)) (("2" (skosimp*) (("2" (ground) (("1" (expand "member") (("1" (skosimp*) (("1" (case "i!1 = j") (("1" (inst + "j-1") (("1" (assert) nil nil)) nil) ("2" (inst + "i!1") (("2" (expand "slow") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (skosimp*) (("2" (case "i!1 = j") (("1" (inst + "j-1") (("1" (assert) (("1" (expand "slow") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "i!1") (("1" (expand "slow") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "increasing?") (("2" (skosimp*) (("2" (inst "increasings" "i!1" "j!1") (("2" (assert) (("2" (expand "slow" +) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) (("3" (expand "slow") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "slow") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil) (default const-decl "T" fseqs nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (partial_order? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (below type-eq-decl nil naturalnumbers nil) (i!1 skolem-const-decl "below(s`length)" sort_fseq nil) (s skolem-const-decl "fseq[T]" sort_fseq nil) (stop skolem-const-decl "[# length: posint, seq: [nat -> T] #]" sort_fseq nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (i!1 skolem-const-decl "below(s`length)" sort_fseq nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (slow skolem-const-decl "[# length: nat, seq: [nat -> T] #]" sort_fseq 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (> const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (nat_induction formula-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (empty? const-decl "bool" sets nil) (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq nil) (permutation? const-decl "bool" permutations_fseq nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (fsq type-eq-decl nil fsq nil) (member_sort formula-decl nil sort_fseq nil) (member const-decl "bool" sets nil) (sort_length formula-decl nil sort_fseq nil) (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) (T formal-nonempty-type-decl nil sort_fseq nil) (barray type-eq-decl nil fseqs nil) (fseq type-eq-decl nil fseqs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (increasing? const-decl "bool" sort_fseq nil) (= const-decl "[T, T -> boolean]" equalities nil) (strictly_increasing? const-decl "bool" sort_fseq nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs nil)) nil)) (strictly_sort_length 0 (strictly_sort_length-1 nil 3491746831 ("" (skeep) (("" (name "sss" "strictly_sort(s)") (("" (replace -1) (("" (hide -) (("" (case "EXISTS (fm:[below(s`length)->below(sss`length)]): surjective?(fm)") (("1" (case "FORALL (mm,nn:nat): (EXISTS (fm: [below(mm) -> below(nn)]): surjective?(fm)) IMPLIE (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (induct "nn") (("1" (skeep) (("1" (skeep -) (("1" (assert) nil nil)) nil)) nil) ("2" (skolem 1 "nn") (("2" (flatten) (("2" (assert) (("2" (skeep) (("2" (assert) (("2" (inst - "mm-1") (("1" (assert) (("1" (hide 2) (("1" (skeep -) (("1" (case "NOT fm(mm-1) = nn") (("1" (label "fnot" 1) (("1" (hide "fnot") (("1" (name "newfm" "(LAMBDA (ii:below(mm-1)): IF fm(ii) /= nn THEN fm(ii) ELSE fm(mm-1) ENDIF)") (("1" (inst + "newfm") (("1" (copy -2) (("1" (expand "surjective?") (("1" (inst - "nn") (("1" (skeep) (("1" (typepred "y") (("1" (inst - "y") (("1" (skolem -2 "ab") (("1" (skosimp*) (("1" (case "x!1 = mm-1") (("1" (replace -1) (("1" (inst + "ab") (("1" (expand "newfm" +) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (inst + "x!1") (("1" (assert) (("1" (expand "newfm" +) (("1" (propax) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "newfm" +) (("2" (lift-if) (("2" (ground) (("2" (reveal "fnot") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "gfm" "(LAMBDA (iz:below(mm-1)): IF fm(iz) = nn THEN 0 ELSE fm(iz) ENDIF)") (("2" (inst + "gfm") (("1" (hide -1) (("1" (expand "surjective?") (("1" (skeep) (("1" (inst - "y") (("1" (skeep -2) (("1" (inst + "x") (("1" (expand "gfm") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "gfm" +) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (case "mm = 0") (("1" (expand "surjective?" -) (("1" (inst - "0") (("1" (skosimp*) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -) (("2" (expand "surjective?") (("2" (inst - "0") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name "thisfm" "(LAMBDA (jj:below(s`length)): choose({ii:below(sss`length) | sss`seq(ii) = s`seq(jj)} (("1" (inst + "thisfm") (("1" (expand "surjective?") (("1" (skeep) (("1" (hide -) (("1" (expand "thisfm" +) (("1" (typepred "sss") (("1" (inst - "sss`seq(y)") (("1" (case "member(sss`seq(y),sss)") (("1" (assert) (("1" (hide -1) (("1" (expand "member") (("1" (skosimp*) (("1" (inst + "i!1") (("1" (name "pz" "choose({ii: below(sss`length) | sss`seq(ii) = s`seq(i!1)})") (("1" (replace -1) (("1" (hide -1) (("1" (typepred "pz") (("1" (expand "strictly_increasing?") (("1" (case "pz < y") (("1" (inst - "pz" "y") (("1" (assert) nil nil)) nil) ("2" (inst - "y" "pz") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "y") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "y") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (typepred "sss") (("2" (inst - "s`seq(jj)") (("2" (case "member(s`seq(jj),s)") (("1" (assert) (("1" (hide -1) (("1" (expand "member") (("1" (skosimp*) (("1" (inst - "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((strictly_sort const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq nil) (member const-decl "bool" fseqs nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (strictly_increasing? const-decl "bool" sort_fseq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (T formal-nonempty-type-decl nil sort_fseq nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (thisfm skolem-const-decl "[jj: below(s`length) -> ({ii: below(sss`length) | sss`seq(ii) = s`seq(jj)})]" sort_fseq nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (mm skolem-const-decl "nat" sort_fseq nil) (NOT const-decl "[bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nn skolem-const-decl "nat" sort_fseq nil) (newfm skolem-const-decl "[below(mm - 1) -> below(1 + nn)]" sort_fseq nil) (x!1 skolem-const-decl "below(mm)" sort_fseq nil) (ab skolem-const-decl "below(mm)" sort_fseq nil) (/= const-decl "boolean" notequal nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (gfm skolem-const-decl "[below(mm - 1) -> naturalnumber]" sort_fseq nil) (x skolem-const-decl "below(mm)" sort_fseq nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (surjective? const-decl "bool" functions nil)) shostak)) (strictly_sort_subint_eq 0 (strictly_sort_subint_eq-1 nil 3491669354 ("" (skeep) (("" (name "sss" "strictly_sort(s)") (("" (replace -1) (("" (assert) (("" (label "ssname" -1) (("" (flatten) (("" (skeep) (("" (label "sinc" -2) (("" (case "EXISTS (jjj:below(s`length-1)): sss`seq(ii) = s`seq(jjj) AND s`seq(jjj) /= s`seq(j (("1" (skeep -1) (("1" (inst + "jjj") (("1" (assert) (("1" (typepred "sss") (("1" (inst - "sss`seq(1+ii)") (("1" (case "member(sss`seq(1+ii),sss)") (("1" (assert) (("1" (hide -1) (("1" (expand "member") (("1" (skosimp*) (("1" (replace -2) (("1" (case "i!1 > jjj") (("1" (copy "sinc") (("1" (copy -1) (("1" (expand "increasing?" (-1 -2)) (("1" (inst - "jjj+1" "i!1") (("1" (assert) (("1" (inst - "jjj" "jjj+1") (("1" (assert) (("1" (typepred "sss") (("1" (inst - "s`seq(1+jjj)") (("1" (case "member(s`seq(1+jjj),s)") (("1" (assert) (("1" (hide -1) (("1" (expand "member") (("1" (skosimp*) (("1" (case "i!2 > ii") (("1" (case "sss`seq(1+ii) <= sss`seq(i!2)") (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (flatten) (("1" (expand "partial_order?") (("1" (flatten) (("1" (expand "antisymmetric?") (("1" (inst - "s`seq(i!1)" "s`seq(1+jjj)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "strictly_increasing?") (("2" (inst - "1+ii" "i!2") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (case "i!2 = ii") (("1" (assert) nil nil) ("2" (expand "strictly_increasing?") (("2" (inst - "i!2" "ii") (("2" (assert) (("2" (copy "sinc") (("2" (typepred "<=") (("2" (expand "total_order?") (("2" (flatten) (("2" (expand "partial_order?") (("2" (flatten) (("2" (expand "antisymmetric?") (("2" (inst - "sss`seq(ii)" "sss`seq(i!2)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "1+jjj") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "strictly_increasing?") (("2" (inst - "ii" "1+ii") (("2" (assert) (("2" (flatten) (("2" (expand "increasing?") (("2" (inst - "i!1" "jjj") (("2" (assert) (("2" (typepred "<=") (("2" (expand "total_order?") (("2" (flatten) (("2" (expand "partial_order?") (("2" (flatten) (("2" (expand "antisymmetric?") (("2" (inst - "s`seq(i!1)" "s`seq(jjj)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "1+ii") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "EXISTS (pp:below(s`length-1)): sss`seq(ii) = s`seq(pp)") (("1" (skeep -1) (("1" (case "FORALL (n:nat): pp+n < s`length-1 and sss`seq(ii) = s`seq(pp+n) IMPLIES s`seq(pp+n) = s (("1" (case "FORALL (n: nat): pp + n < s`length - 1 IMPLIES s`seq(pp + n) = s`seq(pp + n + 1)") (("1" (case "FORALL (n: nat): pp + n < s`length IMPLIES s`seq(pp) = s`seq(pp + n)") (("1" (typepred "sss") (("1" (inst - "sss`seq(ii+1)") (("1" (case "member(sss`seq(ii+1),sss)") (("1" (assert) (("1" (hide -1) (("1" (expand "member") (("1" (skosimp*) (("1" (case "i!1 > pp") (("1" (inst - "i!1-pp") (("1" (assert) (("1" (expand "strictly_increasing?") (("1" (inst - "ii" "1+ii") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (case "s`seq(pp) <= s`seq(i!1) and s`seq(pp) /= s`seq(i!1)") (("1" (flatten) (("1" (expand "increasing?") (("1" (inst - "i!1" "pp") (("1" (assert) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (flatten) (("1" (expand "partial_order?") (("1" (flatten) (("1" (expand "antisymmetric?") (("1" (inst - "s`seq(i!1)" "s`seq(pp)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "strictly_increasing?") (("2" (inst - "ii" "1+ii") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "1+ii") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (2 3)) (("2" (induct "n") (("1" (assert) nil nil) ("2" (skeep) (("2" (assert) (("2" (inst - "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (2 3)) (("2" (case "FORALL (n:nat): pp+n < s`length IMPLIES s`seq(pp+n) = sss`seq(ii)") (("1" (skeep) (("1" (inst-cp - "n") (("1" (inst - "n+1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (assert) nil nil) ("2" (skeep) (("2" (inst - "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skeep) (("2" (inst + "pp+n") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (2 3)) (("2" (typepred "sss") (("2" (inst - "sss`seq(ii)") (("2" (case "member(sss`seq(ii),sss)") (("1" (assert) (("1" (hide -1) (("1" (expand "member") (("1" (assert) (("1" (skosimp*) (("1" (case "i!1 /= s`length-1") (("1" (inst + "i!1") (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (hide +) (("2" (expand "strictly_increasing?") (("2" (inst - "ii" "1+ii") (("2" (assert) (("2" (flatten) (("2" (typepred "sss") (("2" (inst - "sss`seq(1+ii)") (("2" (case "member(sss`seq(1+ii),sss)") (("1" (assert) (("1" (hide -1) (("1" (expand "member") (("1" (skosimp*) (("1" (expand "increasing?") (("1" (inst - "i!2" "s`length-1") (("1" (assert) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (flatten) (("1" (expand "partial_order?") (("1" (flatten) (("1" (expand "antisymmetric?") (("1" (inst - "sss`seq(ii)" "sss`seq(1+ii)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "1+ii") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "ii") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((strictly_sort const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq nil) (member const-decl "bool" fseqs nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (strictly_increasing? const-decl "bool" sort_fseq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (T formal-nonempty-type-decl nil sort_fseq nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (int_plus_int_is_int application-judgement "int" integers nil) (pp skolem-const-decl "below(s`length - 1)" sort_fseq nil) (i!1 skolem-const-decl "below(s`length)" sort_fseq nil) (s skolem-const-decl "fseq[T]" sort_fseq nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (n skolem-const-decl "nat" sort_fseq nil) (i!1 skolem-const-decl "below(s`length)" sort_fseq nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (increasing? const-decl "bool" sort_fseq 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) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (> const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (strictly_sort_map_TCC1 0 (strictly_sort_map_TCC1-1 nil 3491738423 ("" (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil sort_fseq nil) (barray type-eq-decl nil fseqs nil) (fseq type-eq-decl nil fseqs nil) (strictly_increasing? const-decl "bool" sort_fseq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (/= const-decl "boolean" notequal nil) (increasing? const-decl "bool" sort_fseq nil)) nil)) (strictly_sort_map_TCC2 0 (strictly_sort_map_TCC2-1 nil 3491738423 ("" (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil sort_fseq nil) (barray type-eq-decl nil fseqs nil) (fseq type-eq-decl nil fseqs nil) (strictly_increasing? const-decl "bool" sort_fseq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs nil) (below 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) (increasing? const-decl "bool" sort_fseq nil)) nil)) (strictly_sort_map_TCC3 0 (strictly_sort_map_TCC3-2 nil 3491814737 ("" (case "FORALL (s:fseq): LET sss = strictly_sort(s) IN sss`length >= 1 and increasing?(s) IMPLI (("1" (label "ssslem" -1) (("1" (hide -1) (("1" (case "FORALL (s:fseq): EXISTS (sq: [below(strictly_sort(s)`length)->below(s`length)]) LET sss = strictly_sort(s) IN (increasing?(s) AND strictly_sort(s)`length >= 1 IMPLIES sq(strictly_sort(s)`length - 1) = s`length - 1) AND (FORALL (ii:below(sss`length)): (sss`seq(ii) = s`seq(sq(ii)) AND (increasing?(s) AND ii<sss`length-1 IMPLIES sss`seq(ii+1) = s`seq(sq(ii)+1))))") (("1" (name "sfun" "(LAMBDA (s:fseq): LET sss = strictly_sort(s) IN choose({sq: [below(sss`length)->below(s` (increasing?(s) AND strictly_sort(s)`length >= 1 IMPLIES sq(strictly_sort(s)`length - 1) = s`length - 1) AND (FORALL (ii:below(sss`length)): (sss`seq(ii) = s`seq(sq(ii)) AND (increasing?(s) AND ii<sss`length-1 IMPLIES sss`seq(ii+1) = s`seq(sq(ii)+1))))}))") (("1" (inst + "sfun") nil nil) ("2" (hide 2) (("2" (skeep) (("2" (split +) (("1" (skeep) (("1" (ground) nil nil)) nil) ("2" (name "iz" "choose[[below(sss`length) -> below(s`length)]] ({sq: [below(sss`length) -> below(s`length)] | (increasing?(s) AND strictly_sort(s)`length >= 1 IMPLIES sq(strictly_sort(s)`length - 1) = s`length - 1) AND (FORALL (ii: below(sss`length)): (sss`seq(ii) = s`seq(sq(ii)) AND (increasing?(s) AND ii < sss`length - 1 IMPLIES sss`seq(1 + ii) = s`seq(1 + sq(ii)))))})") (("1" (replace -1) (("1" (flatten) (("1" (typepred "iz") (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst -3 "s") (("2" (skosimp*) (("2" (inst - "sq!1") (("1" (expand "member") (("1" (assert) (("1" (flatten) (("1" (replace -1 :dir rl) (("1" (replace -2) (("1" (skeep) (("1" (inst - "ii") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) (("2" (skeep) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (ground) nil nil)) nil)) nil) ("3" (replace -1 :dir rl) (("3" (skeep) (("3" (name "ip" "choose[[below(sss`length) -> below(s`length)]] ({sq: [below(sss`length) -> below(s`length)] | (increasing?(s) IMPLIES sq(sss`length - 1) = s`length - 1) AND (FORALL (ii: below(sss`length)): (sss`seq(ii) = s`seq(sq(ii)) AND (increasing?(s) AND ii < sss`length - 1 IMPLIES sss`seq(1 + ii) = s`seq(1 + sq(ii)))))})") (("1" (replace -1) (("1" (typepred "ip") (("1" (inst - "ii_1") (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst -3 "s") (("2" (skosimp*) (("2" (inst - "sq!1") (("1" (assert) (("1" (expand "member") (("1" (flatten) (("1" (replace -1 :dir rl) (("1" (replace -2) (("1" (skeep) (("1" (inst - "ii") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (expand "nonempty?") (("3" (expand "empty?") (("3" (inst -3 "s") (("3" (skosimp*) (("3" (inst - "sq!1") (("1" (assert) (("1" (expand "member") (("1" (flatten) (("1" (replace -1 :dir rl) (("1" (replace -2) (("1" (skeep) (("1" (inst - "ii") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (skosimp*) (("4" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (name "sss" "strictly_sort(s)") (("2" (replace -1) (("2" (assert) (("2" (case "FORALL (ii:below(sss`length)): EXISTS (jj:below(s`length)): (increasing?(s) AND (("1" (name "sqz" "(LAMBDA (ii:below(sss`length)): choose({jj:below(s`length) | (increasing?(s) AND ii=s (increasing?(s) AND ii < sss`length - 1 IMPLIES sss`seq(1 + ii) = s`seq(1 + jj))}))") (("1" (inst + "sqz") (("1" (expand "sqz" +) (("1" (split +) (("1" (flatten) (("1" (assert) (("1" (typepred "choose({jj: below(s`length) | jj = s`length - 1 AND sss`seq(sss`length - 1) = s`seq(jj)})") (("1" (propax) nil nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "s`length-1") (("2" (expand "member") (("2" (reveal "ssslem") (("2" (inst - "s") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (name "iz" "choose({jj: below(s`length) | (increasing?(s) AND ii = sss`length - 1 IMPLIES jj = s`length - 1) AND sss`seq(ii) = s`seq(jj) AND (increasing?(s) AND ii < sss`length - 1 IMPLIES sss`seq(1 + ii) = s`seq(1 + jj))})") (("1" (replace -1) (("1" (typepred "iz") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst -3 "ii") (("2" (skeep -3) (("2" (inst - "jj") (("2" (expand "member") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (ground) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst -2 "ii") (("2" (skeep -2) (("2" (inst - "jj") (("2" (expand "member") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (lemma "strictly_sort_subint_eq") (("2" (inst - "s") (("2" (replace -2) (("2" (assert) (("2" (case "NOT increasing?(s)") (("1" (assert) (("1" (typepred "sss") (("1" (inst - "sss`seq(ii)") (("1" (case "member(sss`seq(ii),sss)") (("1" (assert) (("1" (hide -1) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst + "ii") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "sincreasing" -1) (("2" (assert) (("2" (case "NOT ii = sss`length-1") (("1" (inst - "ii") (("1" (skosimp*) (("1" (inst + "jj!1") (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (inst + "s`length-1") (("1" (assert) (("1" (reveal "ssslem") (("1" (inst - "s") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "strictly_sort_length") (("2" (inst - "s") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (skeep) (("3" (ground) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (skeep) (("4" (ground) nil nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skeep) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (name "sss" "strictly_sort(s)") (("2" (replace -1) (("2" (hide -) (("2" (assert) (("2" (flatten) (("2" (typepred "<=") (("2" (expand "total_order?") (("2" (flatten) (("2" (expand "partial_order?") (("2" (flatten) (("2" (expand "antisymmetric?") (("2" (inst?) (("1" (ground) (("1" (hide 2) (("1" (typepred "sss") (("1" (inst - "sss`seq(sss`length-1)") (("1" (case "member(sss`seq(sss`length-1),sss)") (("1" (assert) (("1" (hide -1) (("1" (expand "member") (("1" (skosimp*) (("1" (expand "increasing?") (("1" (inst - "i!1" "s`length-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "member") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sss") (("2" (inst - "s`seq(s`length-1)") (("1" (case "member(s`seq(s`length-1),s)") (("1" (assert) (("1" (hide -1) (("1" (expand "member") (("1" (skosimp*) (("1" (expand "strictly_increasing?") (("1" (inst - "i!1" "sss`length-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member" +) (("2" (inst + "s`length-1") (("2" (lemma "strictly_sort_length") (("2" (inst - "s") (("2" (assert) (("2" (expand "sss") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "strictly_sort_length") (("3" (inst - "s") (("3" (expand "sss") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "strictly_sort_length") (("2" (inst - "s") (("2" (expand "sss") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "strictly_sort_length") (("2" (inst - "s") (("2" (expand "sss") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "strictly_sort_length") (("3" (inst - "s") (("3" (expand "sss") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (assert) (("3" (lemma "fseq_length_zero") (("3" (inst - "s") (("3" (assert) (("3" (typepred "sss") (("3" (inst - "sss`seq(0)") (("3" (ground) (("1" (expand "member") (("1" (skosimp*) nil nil)) nil) ("2" (expand "member") (("2" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil) ((empty_seq_fseq name-judgement "fseq" sort_fseq nil) (fseq_length_zero formula-decl nil fseqs nil) (partial_order? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (sss skolem-const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq nil) (s skolem-const-decl "fseq[T]" sort_fseq nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (s skolem-const-decl "fseq[T]" sort_fseq nil) (sss skolem-const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sss skolem-const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq nil) (s skolem-const-decl "fseq[T]" sort_fseq nil) (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (ii_1 skolem-const-decl "below(strictly_sort(s)`length)" sort_fseq nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (s skolem-const-decl "fseq[T]" sort_fseq nil) (sss skolem-const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq nil) (sqz skolem-const-decl "[ii: below(sss`length) -> ({jj: below(s`length) | (increasing?(s) AND ii = sss`length - 1 IMPLIES jj = s`length - 1) AND sss`seq(ii) = s`seq(jj) AND (increasing?(s) AND ii < sss`length - 1 IMPLIES sss`seq(1 + ii) = s`seq(1 + jj))})]" sort_fseq nil) (ii skolem-const-decl "below(sss`length)" sort_fseq nil) (strictly_sort_length formula-decl nil sort_fseq nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (strictly_sort_subint_eq formula-decl nil sort_fseq nil) (int_minus_int_is_int application-judgement "int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil sort_fseq nil) (barray type-eq-decl nil fseqs nil) (fseq type-eq-decl nil fseqs nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (strictly_increasing? const-decl "bool" sort_fseq nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs nil) (IMPLIES const-decl "[bool, 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) (increasing? const-decl "bool" sort_fseq nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (strictly_sort const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq nil)) nil) (strictly_sort_map_TCC3-1 nil 3491814655 ("" (existence-tcc) nil nil) nil nil)) (strictly_sort_map_between_TCC1 0 (strictly_sort_map_between_TCC1-1 nil 3491753372 ("" (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil sort_fseq nil) (barray type-eq-decl nil fseqs nil) (fseq type-eq-decl nil fseqs nil) (strictly_increasing? const-decl "bool" sort_fseq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs nil) (/= const-decl "boolean" notequal nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (increasing? const-decl "bool" sort_fseq nil)) nil)) (strictly_sort_map_between_TCC2 0 (strictly_sort_map_between_TCC2-1 nil 3491753372 ("" (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil sort_fseq nil) (barray type-eq-decl nil fseqs nil) (fseq type-eq-decl nil fseqs nil) (strictly_increasing? const-decl "bool" sort_fseq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs nil) (/= const-decl "boolean" notequal nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (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) (below type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (increasing? const-decl "bool" sort_fseq nil)) nil)) (strictly_sort_map_between 0 (strictly_sort_map_between-1 nil 3491753373 ("" (skeep) (("" (name "sss" "strictly_sort(s)") (("" (replace -1) (("" (assert) (("" (skeep) (("" (skeep) (("" (name "sig" "strictly_sort_map(s)") (("" (replace -1) (("" (case "FORALL (ij:below(sss`length-1)): s`seq(sig(ij)+1) = s`seq(sig(ij+1))") (("1" (inst - "ii") (("1" (case "s`seq(sig(ii)+1) <= s`seq(jj) AND s`seq(jj) <= s`seq(sig(ii+1))") (("1" (flatten) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (flatten) (("1" (expand "partial_order?") (("1" (flatten) (("1" (expand "antisymmetric?") (("1" (inst - "s`seq(sig(ii+1))" "s`seq(jj)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (expand "increasing?") (("1" (inst - "sig(ii)+1" "jj") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "increasing?") (("2" (inst - "jj" "sig(ii+1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -2 1)) (("2" (skeep) (("2" (typepred "sig") (("2" (inst - "ij") (("2" (assert) (("2" (flatten) (("2" (hide -1) (("2" (replace -3) (("2" (typepred "sig") (("2" (inst - "ij+1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((strictly_sort const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq nil) (member const-decl "bool" fseqs nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (strictly_increasing? const-decl "bool" sort_fseq nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (T formal-nonempty-type-decl nil sort_fseq nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (partial_order? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (increasing? const-decl "bool" sort_fseq nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (strictly_sort_map const-decl "{sq: [below(strictly_sort(s)`length) -> below(s`length)] | LET sss = strictly_sort(s) IN (increasing?(s) AND sss`length >= 1 IMPLIES sq(sss`length - 1) = s`length - 1) AND (FORALL (ii: below(sss`length)): (sss`seq(ii) = s`seq(sq(ii)) AND (increasing?(s) AND ii < sss`length - 1 IMPLIES sss`seq(ii + 1) = s`seq(sq(ii) + 1))))}" sort_fseq nil)) shostak)) (strictly_sort_map_increasing 0 (strictly_sort_map_increasing-1 nil 3491840372 ("" (skeep) (("" (skeep) (("" (name "sq" "strictly_sort_map(s)") (("" (replace -1) (("" (assert) (("" (flatten) (("" (typepred "sq") (("" (hide -1) (("" (inst-cp - "ii") (("" (inst - "jj") (("" (flatten) (("" (assert) (("" (name "sss" "strictly_sort(s)") (("" (replace -1) (("" (assert) (("" (case "s`seq(sq(jj)) <= s`seq(sq(ii))") (("1" (typepred "sss") (("1" (expand "strictly_increasing?") (("1" (inst - "ii" "jj") (("1" (assert) (("1" (flatten) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "antisymmetric?") (("1" (flatten) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing?") (("2" (inst - "sq(jj)" "sq(ii)") (("2" (assert) (("2" (typepred "<=") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (flatten) (("2" (expand "reflexive?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (partial_order? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (reflexive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (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) (< const-decl "bool" reals nil) (T formal-nonempty-type-decl nil sort_fseq nil) (barray type-eq-decl nil fseqs nil) (fseq type-eq-decl nil fseqs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (strictly_increasing? const-decl "bool" sort_fseq nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" fseqs nil) (strictly_sort const-decl "{ss: fseq | strictly_increasing?(ss) AND (FORALL (x: T): member(x, s) IFF member(x, ss))}" sort_fseq nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (increasing? const-decl "bool" sort_fseq nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (strictly_sort_map const-decl "{sq: [below(strictly_sort(s)`length) -> below(s`length)] | LET sss = strictly_sort(s) IN (increasing?(s) AND sss`length >= 1 IMPLIES sq(sss`length - 1) = s`length - 1) AND (FORALL (ii: below(sss`length)): (sss`seq(ii) = s`seq(sq(ii)) AND (increasing?(s) AND ii < sss`length - 1 IMPLIES sss`seq(ii + 1) = s`seq(sq(ii) + 1))))}" sort_fseq nil)) shostak)) (sort_map_TCC1 0 (sort_map_TCC1-2 nil 3410539887 ("" (inst + "(LAMBDA (s: fseq[T]): choose({map: [below(length(s)) -> below(length(s))] | bijective?[below(length(s)), below(length(s))](map) AND (FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}))") (("" (skosimp*) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (lemma "sort_fseq_lem") (("" (inst?) (("" (expand "permutation?") (("" (skosimp*) (("" (inst -3 "f!1") (("1" (assert) (("1" (prop) (("1" (assert) (("1" (expand "bijective?") (("1" (split +) (("1" (flatten) (("1" (expand "injective?") (("1" (propax) nil nil)) nil)) nil) ("2" (flatten) (("2" (expand "surjective?") (("2" (skosimp*) (("2" (inst -2 "y!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x1!1") (("2" (typepred "f!1(x1!1)") (("2" (rewrite "sort_length") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (sort_fseq_lem formula-decl nil sort_fseq nil) (s!1 skolem-const-decl "fseq[T]" sort_fseq nil) (f!1 skolem-const-decl "[below(length(s!1)) -> below(length(sort(s!1)))]" sort_fseq nil) (sort_length formula-decl nil sort_fseq nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq nil) (increasing? const-decl "bool" sort_fseq nil) (permutation? const-decl "bool" permutations_fseq nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (fsq type-eq-decl nil fsq nil) (= const-decl "[T, T -> boolean]" equalities nil) (bijective? const-decl "bool" functions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (T formal-nonempty-type-decl nil sort_fseq nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil) (sort_map_TCC1-1 nil 3280843647 ("" (skosimp*) (("" (typepred "map!1(i!1)") (("" (rewrite "sort_length") nil nil)) nil)) nil) nil nil)) (sort_map_def 0 (sort_map_def-1 nil 3280843647 ("" (skosimp*) (("" (typepred "sort_map(s!1)(i!1)") (("" (typepred "sort_map(s!1)") (("" (inst?) nil nil)) nil)) nil)) nil) ((sort_map const-decl "{map: [below(length(s)) -> below(length(s))] | bijective?(map) AND (FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}" sort_fseq nil) (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq nil) (increasing? const-decl "bool" sort_fseq nil) (permutation? const-decl "bool" permutations_fseq nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (fsq type-eq-decl nil fsq nil) (= const-decl "[T, T -> boolean]" equalities nil) (bijective? const-decl "bool" functions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below 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) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (T formal-nonempty-type-decl nil sort_fseq 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)) nil)) (sort_map_bij 0 (sort_map_bij-1 nil 3280843647 ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil)) (isort_map_TCC1 0 (isort_map_TCC1-1 nil 3280843647 ("" (inst + "(LAMBDA (s: {ss: fseq[T] | length(ss) > 0}): choose({map: [below(length(s)) -> below(length(s))] | bijective?[below(length(s)), below(length(s))](map) AND (FORALL (i: below(length(s))): seq(s)(map(i)) = seq(sort(s))(i))}))") (("" (skosimp*) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (lemma "sort_fseq_lem") (("" (inst?) (("" (expand "permutation?") (("" (skosimp*) (("" (inst -3 "inverse(f!1)") (("1" (assert) (("1" (prop) (("1" (lemma "bij_inv_is_bij[below(length(s!1)), below(length(sort(s!1)))]") (("1" (inst?) (("1" (assert) (("1" (hide -2 -3) (("1" (expand "bijective?") (("1" (flatten) (("1" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "surjective?") (("2" (skosimp*) (("2" (inst - "y!1") (("2" (assert) (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (inst + "0") nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("1" (lemma "comp_inverse_right_surj[below(length(s!1)), below(length(sort(s!1)))]") (("1" (inst?) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (expand "bijective?") (("2" (flatten) nil nil)) nil)) nil) ("2" (inst 1 "0") nil nil)) nil) ("2" (inst 1 "0") nil nil)) nil)) nil)) nil)) nil) ("2" (inst 1 "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (sort_fseq_lem formula-decl nil sort_fseq nil) (inverse const-decl "D" function_inverse nil) (sort_length formula-decl nil sort_fseq nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (s!1 skolem-const-decl "{ss: fseq[T] | length(ss) > 0}" sort_fseq nil) (x!1 skolem-const-decl "below(length(sort(s!1)))" sort_fseq nil) (NOT const-decl "[bool -> bool]" booleans nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (bij_inv_is_bij formula-decl nil function_inverse nil) (f!1 skolem-const-decl "[below(length(s!1)) -> below(length(sort(s!1)))]" sort_fseq nil) (comp_inverse_right_surj formula-decl nil function_inverse nil) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq nil) (increasing? const-decl "bool" sort_fseq nil) (permutation? const-decl "bool" permutations_fseq nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (fsq type-eq-decl nil fsq nil) (= const-decl "[T, T -> boolean]" equalities nil) (bijective? const-decl "bool" functions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers 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) (> 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) (fseq type-eq-decl nil fseqs nil) (barray type-eq-decl nil fseqs nil) (T formal-nonempty-type-decl nil sort_fseq nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (isort_map_def_TCC1 0 (isort_map_def_TCC1-1 nil 3282578124 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (isort_map_def 0 (isort_map_def-1 nil 3280843647 ("" (skosimp*) (("" (assert) (("" (typepred "isort_map(s!1)") (("" (inst?) nil nil)) nil)) 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) (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) (T formal-nonempty-type-decl nil sort_fseq nil) (barray type-eq-decl nil fseqs nil) (fseq type-eq-decl nil fseqs nil) (below type-eq-decl nil naturalnumbers nil) (bijective? const-decl "bool" functions nil) (> const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (fsq type-eq-decl nil fsq nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" sort_fseq nil) (permutation? const-decl "bool" permutations_fseq nil) (increasing? const-decl "bool" sort_fseq nil) (sort const-decl "{ss: fseq | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_fseq nil) (isort_map const-decl "{map: [below(length(s)) -> below(length(s))] | bijective?(map) AND (FORALL (i: below(length(s))): seq(s)(map(i)) = seq(sort(s))(i))}" sort_fseq nil)) nil)) (isort_map_bij 0 (isort_map_bij-1 nil 3280843647 ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil)))
¤ 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.0.215Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26