|
(sort_array
(sort_TCC1 0
(sort_TCC1-1 nil 3282575942
("" (case "N = 0")
(("1" (inst + "(LAMBDA (A: [below(N) -> T]): A)")
(("1" (skosimp*)
(("1" (rewrite "perm_reflexive")
(("1" (expand "sorted?")
(("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (inst + "(LAMBDA A: asort(A,N-1))")
(("1" (skosimp*)
(("1" (rewrite "asort_perm")
(("1" (assert)
(("1" (lemma "asort_P_and_Q")
(("1" (inst?)
(("1" (expand "sorted?")
(("1" (skosimp*)
(("1" (expand "P")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) (("2" (skosimp*) (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(below_array type-eq-decl nil below_arrays nil)
(below type-eq-decl nil nat_types nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" sort_array nil)
(asort def-decl "below_array" sort_array_def 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)
(asort_perm formula-decl nil sort_array_def nil)
(asort_P_and_Q formula-decl nil sort_array_def nil)
(P const-decl "bool" sort_array_def nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil sort_array nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(permutation_of? const-decl "bool" permutations nil)
(sorted? const-decl "bool" sort_array nil)
(perm_reflexive formula-decl nil permutations 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)
(= const-decl "[T, T -> boolean]" equalities 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)
(N formal-const-decl "nat" sort_array nil))
nil))
(sort_lem 0
(sort_lem-1 nil 3282575942
("" (skosimp*)
(("" (typepred "sort(A!1)") (("" (assert) nil nil)) nil)) nil)
((sort const-decl "{a | permutation_of?(A, a) AND sorted?(a)}"
sort_array nil)
(sorted? const-decl "bool" sort_array nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(permutation_of? const-decl "bool" permutations nil)
(T formal-type-decl nil sort_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "nat" sort_array nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(sort_in? 0
(sort_in?-1 nil 3282575942
("" (skosimp*)
(("" (lemma "sort_lem")
(("" (inst?)
(("" (flatten)
(("" (lemma "perm_in?")
(("" (inst?)
(("" (inst -1 "sort(A!1)")
(("" (assert)
(("" (replace -1)
(("" (hide -1) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sort_lem formula-decl nil sort_array 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(perm_in? formula-decl nil permutations nil)
(T formal-type-decl nil sort_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "nat" sort_array nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(sort_map_TCC1 0
(sort_map_TCC1-1 nil 3282575942
(""
(inst + "(LAMBDA (A: [below(N) -> T]):
choose({map: [below(N) -> below(N)] |
bijective?[below(N), below(N)](map) AND
FORALL i: A(i) = sort(A)(map(i))}))")
(("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (lemma "sort_lem")
(("" (inst?)
(("" (flatten)
(("" (expand "permutation_of?")
(("" (skosimp*)
(("" (inst -4 "f!1") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(sort_lem formula-decl nil sort_array 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 "{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)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil nat_types nil)
(bijective? const-decl "bool" functions nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil sort_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "nat" sort_array nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(sort_map_def 0
(sort_map_def-1 nil 3282575942
("" (skosimp*)
(("" (assert)
(("" (typepred "sort_map(A!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)
(N formal-const-decl "nat" sort_array nil)
(below type-eq-decl nil naturalnumbers nil)
(bijective? const-decl "bool" functions nil)
(T formal-type-decl nil sort_array nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(permutation_of? const-decl "bool" permutations nil)
(sorted? const-decl "bool" sort_array nil)
(sort const-decl "{a | permutation_of?(A, a) AND sorted?(a)}"
sort_array nil)
(sort_map const-decl "{map: [below(N) -> below(N)] |
bijective?(map) AND (FORALL i: A(i) = sort(A)(map(i)))}"
sort_array nil))
nil))
(sort_map_bij 0
(sort_map_bij-1 nil 3282575942
("" (skosimp*) (("" (assert) nil nil)) nil) nil nil))
(isort_map_TCC1 0
(isort_map_TCC1-1 nil 3282575942
(""
(inst + "(LAMBDA (A: [below(N) -> T]):
choose({map: [below(N) -> below(N)] |
bijective?[below(N), below(N)](map) AND
FORALL i: A(map(i)) = sort(A)(i)}))")
(("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (lemma "sort_lem")
(("" (inst?)
(("" (flatten)
(("" (expand "permutation_of?")
(("" (skosimp*)
(("" (case "N = 0")
(("1" (inst -5 "f!1")
(("1" (assert) (("1" (skosimp*) nil nil))
nil))
nil)
("2" (inst -4 "inverse(f!1)")
(("1" (prop)
(("1"
(lemma
"bij_inv_is_bij[below(N), below(N)]")
(("1"
(inst?)
(("1" (assert) nil nil))
nil)
("2"
(inst + "0")
(("2" (assert) nil nil))
nil))
nil)
("2" (skosimp*)
(("2"
(inst -2 "inverse(f!1)(i!1)")
(("1"
(assert)
(("1"
(expand "bijective?")
(("1"
(flatten)
(("1"
(lemma
"comp_inverse_right_surj[below(N),below(N)]")
(("1"
(inst -1 "i!1" "f!1")
(("1" (assert) nil nil))
nil)
("2" (inst + "0") nil nil))
nil))
nil))
nil))
nil)
("2" (inst + "0") nil nil))
nil))
nil))
nil)
("2" (inst + "0") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(sort_lem formula-decl nil sort_array nil)
(inverse const-decl "D" function_inverse nil)
(surjective? const-decl "bool" functions nil)
(f!1 skolem-const-decl "[below(N) -> below(N)]" sort_array nil)
(comp_inverse_right_surj formula-decl nil function_inverse nil)
(bij_inv_is_bij 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 "{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)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil nat_types nil)
(bijective? const-decl "bool" functions nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil sort_array nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "nat" sort_array nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(isort_map_def 0
(isort_map_def-1 nil 3282575942
("" (skosimp*)
(("" (assert)
(("" (typepred "isort_map(A!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)
(N formal-const-decl "nat" sort_array nil)
(below type-eq-decl nil naturalnumbers nil)
(bijective? const-decl "bool" functions nil)
(T formal-type-decl nil sort_array nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(permutation_of? const-decl "bool" permutations nil)
(sorted? const-decl "bool" sort_array nil)
(sort const-decl "{a | permutation_of?(A, a) AND sorted?(a)}"
sort_array nil)
(isort_map const-decl "{map: [below(N) -> below(N)] |
bijective?(map) AND (FORALL i: A(map(i)) = sort(A)(i))}"
sort_array nil))
nil))
(isort_map_bij 0
(isort_map_bij-1 nil 3282575942
("" (skosimp*) (("" (assert) nil nil)) nil) nil nil)))
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
