|
(sort_array_def
(swap_TCC1 0
(swap_TCC1-1 nil 3281095548 ("" (subtype-tcc) nil nil) nil nil))
(swap_TCC2 0
(swap_TCC2-1 nil 3281095548 ("" (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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "nat" sort_array_def nil)
(below type-eq-decl nil nat_types 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)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(asort_TCC1 0
(asort_TCC1-1 nil 3281095548 ("" (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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "nat" sort_array_def nil)
(below type-eq-decl nil nat_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_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))
nil))
(asort_TCC2 0
(asort_TCC2-1 nil 3281095548 ("" (termination-tcc) nil nil) nil nil))
(swap_perm 0
(swap_perm-1 nil 3281095548
("" (skosimp*)
(("" (expand "swap")
(("" (expand "permutation_of?")
((""
(inst 1 "(LAMBDA (i: below(N)): IF i = jj!1 THEN
Imin(A!1, jj!1, N - 1)
ELSIF i = Imin(A!1, jj!1, N - 1) THEN
jj!1
ELSE i
ENDIF)")
(("1" (prop)
(("1" (expand "bijective?")
(("1" (prop)
(("1" (expand "injective?")
(("1" (skosimp*)
(("1" (ground)
(("1" (lift-if)
(("1" (lift-if)
(("1" (ground)
(("1" (lift-if) (("1" (ground) nil nil))
nil)
("2" (lift-if) (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "surjective?")
(("2" (skosimp*)
(("2" (case "y!1 = jj!1")
(("1" (inst 1 "Imin(A!1, jj!1, N - 1)")
(("1" (ground)
(("1" (lift-if) (("1" (ground) nil nil))
nil))
nil)
("2" (assert)
(("2" (typepred "Imin(A!1, jj!1, N - 1)")
(("2" (assert) nil nil)) nil))
nil))
nil)
("2" (case "y!1 = Imin(A!1, jj!1, N - 1)")
(("1" (inst 2 "jj!1") (("1" (assert) nil nil))
nil)
("2" (inst 3 "y!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (lift-if)
(("2" (beta)
(("2" (lift-if)
(("2" (prop)
(("1" (assert) nil nil) ("2" (ground) nil nil)
("3" (ground) nil nil)
("4" (ground) (("4" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (typepred "Imin[N, T, <=](A!1, jj!1, N - 1)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((swap const-decl "below_array" sort_array_def nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(A!1 skolem-const-decl "below_array[N, T]" sort_array_def nil)
(below_array type-eq-decl nil below_arrays nil)
(Imin const-decl
"{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(i) <= A(j))}"
min_array_def nil)
(subrange type-eq-decl nil integers nil)
(abv type-eq-decl nil min_array_def nil)
(<= formal-const-decl "(total_order?[T])" sort_array_def nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(<= const-decl "bool" reals nil)
(T formal-type-decl nil sort_array_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(jj!1 skolem-const-decl "below[N]" sort_array_def nil)
(below type-eq-decl nil nat_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "nat" sort_array_def 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)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(bijective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(injective? const-decl "bool" functions nil)
(permutation_of? const-decl "bool" permutations nil))
nil))
(asort_perm 0
(asort_perm-1 nil 3281095548
("" (induct "jj")
(("1" (flatten)
(("1" (skosimp*)
(("1" (expand "asort") (("1" (rewrite "swap_perm") nil nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (assert)
(("2" (expand "asort" 1)
(("2" (inst?)
(("2" (lemma "swap_perm")
(("2" (inst?)
(("2" (lemma "perm_tran")
(("2"
(inst -1 "A!1" "asort(A!1, jb!1)"
"swap(asort(A!1, jb!1), 1 + jb!1)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((perm_tran formula-decl nil permutations nil)
(swap const-decl "below_array" sort_array_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(swap_perm formula-decl nil sort_array_def nil)
(below_induction formula-decl nil bounded_nat_inductions 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)
(N formal-const-decl "nat" sort_array_def nil)
(asort def-decl "below_array" sort_array_def nil)
(permutation_of? const-decl "bool" permutations nil)
(below_array type-eq-decl nil below_arrays nil)
(T formal-type-decl nil sort_array_def nil)
(below type-eq-decl nil nat_types nil)
(pred type-eq-decl nil defined_types nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil))
nil))
(swap_P_and_Q_TCC1 0
(swap_P_and_Q_TCC1-1 nil 3281095548
("" (skosimp*) (("" (assert) nil nil)) nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers 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))
nil))
(swap_P_and_Q 0
(swap_P_and_Q-1 nil 3281095548
("" (skosimp*)
(("" (prop)
(("1" (expand "swap")
(("1" (typepred "Imin(A!1, 1 + j!1, N - 1)")
(("1" (name "IMIN" "Imin(A!1, 1 + j!1, N - 1)")
(("1" (replace -1)
(("1" (hide -1)
(("1" (expand "P")
(("1" (skosimp*)
(("1" (case "i!1= 1+j!1")
(("1" (replace -1)
(("1" (hide -1) (("1" (assert) nil nil)) nil))
nil)
("2" (inst -6 "i!1" "j!2")
(("2" (assert)
(("2" (ground)
(("1" (expand "Q")
(("1"
(lift-if)
(("1"
(ground)
(("1"
(inst -8 "i!1" "IMIN")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (lift-if)
(("2"
(ground)
(("1"
(expand "Q")
(("1"
(inst -7 "i!1" "1+j!1")
(("1" (assert) nil nil))
nil))
nil)
("2"
(expand "Q")
(("2"
(inst -7 "i!1" "IMIN")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "Q")
(("2" (skosimp*)
(("2" (expand "swap")
(("2" (typepred "Imin(A!1, 1 + j!1, N - 1)")
(("2" (name "IMIN" "Imin(A!1, 1 + j!1, N - 1)")
(("2" (replace -1)
(("2" (hide -1)
(("2" (lift-if)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "P")
(("1" (inst -4 "j!2")
(("1" (assert) nil nil)) nil))
nil)
("2" (lift-if)
(("2" (ground)
(("1"
(inst -5 "1+j!1")
(("1" (assert) nil nil))
nil)
("2"
(inst -4 "j!2")
(("2" (assert) nil nil))
nil))
nil))
nil)
("3" (lift-if)
(("3" (ground)
(("1"
(inst -8 "i!1" "j!1+1")
(("1" (assert) nil nil))
nil)
("2"
(inst -7 "i!1" "j!2")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below_array type-eq-decl nil below_arrays nil)
(Imin const-decl
"{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(i) <= A(j))}"
min_array_def nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(abv type-eq-decl nil min_array_def nil)
(<= formal-const-decl "(total_order?[T])" sort_array_def nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil sort_array_def nil)
(below type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(N formal-const-decl "nat" sort_array_def nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(P const-decl "bool" sort_array_def 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)
(Q const-decl "bool" sort_array_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(swap const-decl "below_array" sort_array_def nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(asort_P_and_Q 0
(asort_P_and_Q-1 nil 3281095548
("" (induct "jj")
(("1" (flatten)
(("1" (skosimp*)
(("1" (assert)
(("1" (expand "asort")
(("1" (prop)
(("1" (expand "P")
(("1" (skosimp*)
(("1" (case-replace "i!1 = 0")
(("1" (case-replace "j!1 = 0")
(("1" (expand "swap")
(("1" (lift-if) (("1" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (expand "Q")
(("2" (skosimp*)
(("2" (case-replace "i!1 = 0")
(("1" (expand "swap")
(("1" (lift-if)
(("1" (assert)
(("1" (ground)
(("1" (typepred "Imin(A!1, 0, N - 1)")
(("1"
(inst -3 "j!1")
(("1" (assert) nil nil))
nil))
nil)
("2" (lift-if)
(("2"
(assert)
(("2"
(ground)
(("1"
(typepred "Imin(A!1, 0, N - 1)")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil)
("2"
(typepred "Imin(A!1, 0, N - 1)")
(("2"
(inst -3 "j!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (assert)
(("2" (expand "asort" 1)
(("2" (inst?)
(("2" (assert)
(("2" (lemma "swap_P_and_Q")
(("2" (assert)
(("2" (inst -1 "asort(A!1,jb!1)" "jb!1")
(("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(swap_P_and_Q formula-decl nil sort_array_def nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(swap const-decl "below_array" sort_array_def nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" sort_array_def nil)
(abv type-eq-decl nil min_array_def nil)
(subrange type-eq-decl nil integers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(Imin const-decl
"{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(i) <= A(j))}"
min_array_def nil)
(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)
(below_induction formula-decl nil bounded_nat_inductions 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)
(N formal-const-decl "nat" sort_array_def nil)
(Q const-decl "bool" sort_array_def nil)
(asort def-decl "below_array" sort_array_def nil)
(P const-decl "bool" sort_array_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(below_array type-eq-decl nil below_arrays nil)
(T formal-type-decl nil sort_array_def nil)
(below type-eq-decl nil nat_types nil)
(pred type-eq-decl nil defined_types nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil))
nil)))
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
