|
(sort_seq
(increasing?_TCC1 0
(increasing?_TCC1-1 nil 3280843647 ("" (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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(sort_TCC1 0
(sort_TCC1-1 nil 3280843647
(""
(inst 1 "(LAMBDA s: (# length := length(s),
seq := sort[length(s),T,<=](seq_to_array(s)) #))")
(("" (skosimp*)
(("" (typepred "sort[length(s!1), T, <=](seq_to_array(s!1))")
(("" (prop)
(("1" (hide -2)
(("1" (expand "seq_to_array")
(("1" (expand "permutation?")
(("1" (expand "permutation_of?")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (expand "sorted?")
(("2" (expand "increasing?")
(("2" (skosimp*)
(("2" (inst?)
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(seq_to_array const-decl "below_array[length(s), T]" sort_seq 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) (>= 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_seq nil)
(permutation? const-decl "bool" permutations_seq nil)
(<= formal-const-decl "(total_order?[T])" sort_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(seqs type-eq-decl nil sort_seq nil)
(T formal-type-decl nil sort_seq nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq nil)
(increasing? const-decl "bool" sort_seq nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(seqs type-eq-decl nil sort_seq nil)
(permutation? const-decl "bool" permutations_seq nil)
(<= formal-const-decl "(total_order?[T])" sort_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil sort_seq nil)
(below type-eq-decl nil nat_types 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_seq nil))
nil))
(sort_seq_lem 0
(sort_seq_lem-1 nil 3280843647
("" (skosimp*)
(("" (typepred "sort(s!1)") (("" (assert) nil nil)) nil)) nil)
((sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq nil)
(increasing? const-decl "bool" sort_seq nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(seqs type-eq-decl nil sort_seq nil)
(permutation? const-decl "bool" permutations_seq nil)
(<= formal-const-decl "(total_order?[T])" sort_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil sort_seq nil)
(below type-eq-decl nil nat_types 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_seq_in? 0
(sort_seq_in?-1 nil 3281101912
("" (skosimp*)
(("" (expand "in?")
(("" (typepred "sort(s!1)")
(("" (hide -2)
(("" (expand "permutation?")
(("" (skosimp*)
(("" (hide -1)
(("" (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")
(("1"
(assert)
(("1"
(hide 2)
(("1"
(reveal -3)
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(inst + "ii!1")
(("2" (assert) nil nil))
nil))
nil))
nil)
("3" (inst + "ii!1")
(("3" (assert) nil nil)) nil))
nil)
("2" (inst + "ii!1")
(("2" (rewrite "sort_length") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((in? const-decl "bool" seqs 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 "seqs" sort_seq nil)
(TRUE const-decl "bool" booleans nil)
(inverse const-decl "D" function_inverse nil)
(ii!1 skolem-const-decl "below(length(sort(s!1)))" sort_seq nil)
(bijective? const-decl "bool" functions nil)
(f!1 skolem-const-decl
"[below(length(s!1)) -> below(length(sort(s!1)))]" sort_seq 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_seq 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)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil sort_seq nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" sort_seq nil)
(permutation? const-decl "bool" permutations_seq nil)
(seqs type-eq-decl nil sort_seq nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(increasing? const-decl "bool" sort_seq nil)
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq nil))
nil))
(sort_seq_in_TCC1 0
(sort_seq_in_TCC1-1 nil 3281102642 ("" (assert) nil nil)
((sort_length formula-decl nil sort_seq nil)) shostak))
(sort_seq_in 0
(sort_seq_in-1 nil 3280843667
("" (skosimp*)
(("" (lemma "sort_seq_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_seq_in? formula-decl nil sort_seq nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" sort_seq nil)
(permutation? const-decl "bool" permutations_seq nil)
(increasing? const-decl "bool" sort_seq nil)
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq 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_seq nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(in? const-decl "bool" seqs nil)
(seqs type-eq-decl nil sort_seq nil)
(T formal-type-decl nil sort_seq nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
shostak))
(sort_seq_in2 0
(sort_seq_in2-1 nil 3281102536
("" (skosimp*)
(("" (lemma "sort_seq_in?")
(("" (inst - "s!1" "seq(s!1)(ii!1)")
(("" (assert)
(("" (hide 2)
(("" (expand "in?") (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((sort_seq_in? formula-decl nil sort_seq nil)
(in? const-decl "bool" seqs 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)
(seqs type-eq-decl nil sort_seq nil)
(T formal-type-decl nil sort_seq nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(sort_map_TCC1 0
(sort_map_TCC1-1 nil 3280843647
("" (skosimp*)
(("" (typepred "map!1(i!1)") (("" (rewrite "sort_length") nil nil))
nil))
nil)
((below type-eq-decl nil naturalnumbers nil)
(seqs type-eq-decl nil sort_seq nil)
(T formal-type-decl nil sort_seq nil)
(below type-eq-decl nil nat_types 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)
(sort_length formula-decl nil sort_seq nil))
nil))
(sort_map_TCC2 0
(sort_map_TCC2-1 nil 3280843647
(""
(inst + "(LAMBDA (s: seqs):
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)))}))")
(("1" (skosimp*)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (lemma "sort_seq_lem")
(("1" (inst?)
(("1" (expand "permutation?")
(("1" (skosimp*)
(("1" (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)
("2" (skosimp*)
(("2" (typepred "map!1(i!1)") (("2" (propax) nil nil)) nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(sort_seq_lem formula-decl nil sort_seq nil)
(s!1 skolem-const-decl "seqs" sort_seq nil)
(f!1 skolem-const-decl
"[below(length(s!1)) -> below(length(sort(s!1)))]" sort_seq 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq nil)
(increasing? const-decl "bool" sort_seq nil)
(permutation? const-decl "bool" permutations_seq nil)
(<= formal-const-decl "(total_order?[T])" sort_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(finite_sequence type-eq-decl nil finite_sequences 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)
(seqs type-eq-decl nil sort_seq nil)
(T formal-type-decl nil sort_seq nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sort_length formula-decl nil sort_seq nil))
nil))
(sort_map_def_TCC1 0
(sort_map_def_TCC1-1 nil 3280843647
("" (skosimp*)
(("" (typepred "sort_map(s!1)(i!1)")
(("" (rewrite "sort_length") 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_seq nil)
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq nil)
(increasing? const-decl "bool" sort_seq nil)
(permutation? const-decl "bool" permutations_seq nil)
(<= formal-const-decl "(total_order?[T])" sort_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(finite_sequence type-eq-decl nil finite_sequences 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)
(seqs type-eq-decl nil sort_seq nil)
(T formal-type-decl nil sort_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)
(sort_length formula-decl nil sort_seq 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_seq nil)
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq nil)
(increasing? const-decl "bool" sort_seq nil)
(permutation? const-decl "bool" permutations_seq nil)
(<= formal-const-decl "(total_order?[T])" sort_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(finite_sequence type-eq-decl nil finite_sequences 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)
(seqs type-eq-decl nil sort_seq nil)
(T formal-type-decl nil sort_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))
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: finite_sequence[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_seq_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"
(typepred "s!1")
(("2" (inst + "0") nil 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_seq_lem formula-decl nil sort_seq nil)
(inverse const-decl "D" function_inverse nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(s!1 skolem-const-decl "{ss: finite_sequence[T] | length(ss) > 0}"
sort_seq nil)
(x!1 skolem-const-decl "below(length(sort(s!1)))" sort_seq 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_seq 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: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq nil)
(increasing? const-decl "bool" sort_seq nil)
(permutation? const-decl "bool" permutations_seq nil)
(<= formal-const-decl "(total_order?[T])" sort_seq nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(seqs type-eq-decl nil sort_seq 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)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil sort_seq nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sort_length formula-decl nil sort_seq 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)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil sort_seq nil)
(seqs type-eq-decl nil sort_seq nil)
(below type-eq-decl nil naturalnumbers nil)
(bijective? const-decl "bool" functions nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" sort_seq nil)
(permutation? const-decl "bool" permutations_seq nil)
(increasing? const-decl "bool" sort_seq nil)
(sort const-decl
"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
sort_seq 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_seq nil))
nil))
(isort_map_bij 0
(isort_map_bij-1 nil 3280843647
("" (skosimp*) (("" (assert) nil nil)) nil) nil nil)))
¤ Dauer der Verarbeitung: 1.6 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
