| products/Sources/formale Sprachen/PVS/structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: atan2_props.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(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 (("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) ELSIF pq = sis!1`length THEN s`seq(j) ELSE default ENDIF) #)") (("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" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.72 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.Bot Zugriff |
