| products/Sources/formale Sprachen/PVS/lebesgue/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: matrix_props.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(matrix_props
(matrix_2x2 0 (matrix_2x2-1 nil 3615814158 ("" (skeep) (("" (rewrite "full_matrix_eq") (("1" (split) (("1" (grind :exclude "entry") nil nil) ("2" (grind :exclude "entry") nil nil) ("3" (skosimp*) (("3" (case "(i!1=0 OR i!1=1) AND (j!1 = 0 OR j!1=1)") (("1" (ground) (("1" (replaces -1) (("1" (replaces -1) (("1" (expand "entry" + 2) (("1" (grind :exclude "entry") nil nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (replaces -1) (("2" (expand "entry" + 2) (("2" (grind :exclude "entry") nil nil)) nil)) nil)) nil) ("3" (replaces -1) (("3" (replaces -1) (("3" (expand "entry" + 2) (("3" (grind :exclude "entry") nil nil)) nil)) nil)) nil) ("4" (replaces -1) (("4" (replaces -1) (("4" (expand "entry" + 2) (("4" (grind :exclude "entry") nil nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (case "(i!1=0 OR i!1=1) AND (j!1 = 0 OR j!1=1)") (("1" (ground) (("1" (replaces -1) (("1" (replaces -1) (("1" (expand "entry" + 2) (("1" (grind :exclude "entry") nil nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (replaces -1) (("2" (expand "entry" + 2) (("2" (grind :exclude "entry") nil nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (replaces -1) (("2" (expand "entry" + 2) (("2" (typepred "i!1") (("2" (typepred "j!1") (("2" (hide 2) (("2" (grind :exclude "entry") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((full_matrix_eq formula-decl nil matrices nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (entry const-decl "real" matrices nil) (null adt-constructor-decl "(null?)" list_adt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (access const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (length_row 0 (length_row-1 nil 3614701537 ("" (skeep) (("" (expand "row") (("" (expand "rows") (("" (lift-if) (("" (ground) (("" (typepred "columns(SM)") (("" (assert) (("" (split -) (("1" (grind) nil nil) ("2" (skosimp*) (("2" (typepred "SM") (("2" (split -) (("1" (grind) nil nil) ("2" (inst - "i" "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((row const-decl "Vector" matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (length def-decl "nat" list_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (length_null formula-decl nil more_list_props "structures/") (rows const-decl "nat" matrices nil)) shostak)) (length_nth_row 0 (length_nth_row-1 nil 3614702183 ("" (skeep) (("" (lemma "length_row") (("" (inst - "SM" "i") (("" (assert) (("" (expand "rows") (("" (assert) (("" (expand "row") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((length_row formula-decl nil matrix_props 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) (row const-decl "Vector" matrices nil) (rows const-decl "nat" matrices nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (real nonempty-type-from-decl nil reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil)) shostak)) (columns_cdr_TCC1 0 (columns_cdr_TCC1-1 nil 3614702658 ("" (grind) 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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil)) nil)) (columns_cdr 0 (columns_cdr-1 nil 3614702658 ("" (skeep) (("" (typepred "columns(cdr(D))") (("" (assert) (("" (split -) (("1" (grind) nil nil) ("2" (skosimp*) (("2" (typepred "columns(D)") (("2" (split -) (("1" (grind) nil nil) ("2" (skosimp*) (("2" (typepred "D") (("2" (split -) (("1" (grind) nil nil) ("2" (inst - "i!1+1" "i!2") (("1" (assert) (("1" (expand "nth" -1 1) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "length" 1) (("2" (assert) (("2" (lift-if) (("2" (ground) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((PosFullMatrix type-eq-decl nil matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (<= const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (> const-decl "bool" reals nil) (FullMatrix type-eq-decl nil matrices nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (length def-decl "nat" list_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (D skolem-const-decl "PosFullMatrix" matrix_props nil) (i!1 skolem-const-decl "below(length(cdr(D)))" matrix_props nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (columns_cons 0 (columns_cons-1 nil 3614939393 ("" (induct "M") (("1" (grind) nil nil) ("2" (skolem 1 ("m1" "M")) (("2" (flatten) (("2" (grind) nil nil)) nil)) nil)) nil) ((list_induction formula-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (length def-decl "nat" list_props 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 "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil matrices nil) (Matrix type-eq-decl nil matrices nil)) shostak)) (access_col 0 (access_col-1 nil 3615029745 ("" (skeep) (("" (expand "access") (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (ground) (("1" (lemma "col_def") (("1" (inst?) (("1" (assert) (("1" (inst - "j") (("1" (replaces -1) (("1" (lift-if) (("1" (ground) (("1" (expand "row" 1) (("1" (lift-if) (("1" (ground) (("1" (rewrite "length_col") (("1" (expand "rows") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_nth_row") (("1" (rewrite "length_row") nil nil) ("2" (rewrite "length_col") (("2" (expand "rows") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_row") (("2" (rewrite "length_col") (("2" (assert) (("2" (lemma "col_def") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (lift-if) (("2" (ground) (("2" (rewrite "length_nth_row") (("2" (expand "rows") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "length_col") (("3" (rewrite "length_row") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((access const-decl "real" matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Matrix type-eq-decl nil matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (FullMatrix type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (length_nth_row formula-decl nil matrix_props nil) (length_row formula-decl nil matrix_props nil) (row const-decl "Vector" matrices nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (length_col formula-decl nil matrices nil) (col_def formula-decl nil matrices nil)) shostak)) (remove_TCC1 0 (remove_TCC1-1 nil 3614083040 ("" (skeep) (("" (ground) (("1" (grind) nil nil) ("2" (skeep 1) (("2" (rewrite "columns_0_entry") (("1" (rewrite "columns_0_entry") nil nil) ("2" (expand "columns" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil) (length def-decl "nat" list_props nil) (row const-decl "Vector" matrices nil) (access const-decl "real" matrices nil) (entry const-decl "real" matrices nil) (columns_0_entry formula-decl nil matrices nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Matrix type-eq-decl nil matrices nil) (real nonempty-type-from-decl nil reals nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil)) nil)) (remove_TCC2 0 (remove_TCC2-1 nil 3614083040 ("" (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Matrix type-eq-decl nil matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil)) nil)) (remove_TCC3 0 (remove_TCC3-1 nil 3614083040 ("" (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) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Matrix type-eq-decl nil matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rows const-decl "nat" matrices nil)) nil)) (remove_TCC4 0 (remove_TCC4-1 nil 3614083040 ("" (skeep) (("" (assert) (("" (ground) (("1" (rewrite "rows_form_matrix" 1) nil nil) ("2" (lemma "columns_form_matrix") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (rewrite "entry_form_matrix") (("3" (lift-if) (("3" (split) (("1" (propax) nil nil) ("2" (flatten) (("2" (rewrite "entry_eq_0") (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) 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) (form_matrix_square application-judgement "FullMatrix" matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (entry_eq_0 formula-decl nil matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (entry_form_matrix formula-decl nil matrices nil) (columns_form_matrix formula-decl nil matrices nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (rows_form_matrix formula-decl nil matrices 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (rows const-decl "nat" matrices nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (entry const-decl "real" matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) nil)) (remove_posfullmatrix 0 (remove_posfullmatrix-1 nil 3614602887 ("" (skeep) (("" (skosimp*) (("" (name "R" "remove(D,i,j)") (("" (replace -1) (("" (assert) (("" (expand "remove" -1) (("" (invoke (name "FZ" "%1") (! -1 1)) (("" (replaces -1) (("" (typepred "FZ") (("" (assert) (("" (copy -5) (("" (inst - "i!1" "j!1") (("" (assert) nil nil)) nil)) 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (Vector type-eq-decl nil matrices nil) (row const-decl "Vector" matrices nil) (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (Matrix type-eq-decl nil matrices 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (entry const-decl "real" matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (remove const-decl "{N | (rows(M) > 1 AND columns(M) > 1 IMPLIES (rows(N) = rows(M) - 1 AND columns(N) = columns(M) - 1)) AND (FORALL (m, n): LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF, newn = IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF IN entry(N)(m, n) = entry(M)(newm, newn))}" matrix_props nil) (FullMatrix type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil)) nil)) (rows_remove 0 (rows_remove-1 nil 3615024326 ("" (skeep) (("" (expand "remove") (("" (lift-if) (("" (ground) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (rewrite "rows_form_matrix") nil nil)) nil)) nil)) nil)) nil) ((remove const-decl "{N | (rows(M) > 1 AND columns(M) > 1 IMPLIES (rows(N) = rows(M) - 1 AND columns(N) = columns(M) - 1)) AND (FORALL (m, n): LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF, newn = IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF IN entry(N)(m, n) = entry(M)(newm, newn))}" matrix_props nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (rows const-decl "nat" matrices nil) (length def-decl "nat" list_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (entry const-decl "real" matrices nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (= const-decl "[T, T -> boolean]" equalities nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (Matrix type-eq-decl nil matrices nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (rows_form_matrix formula-decl nil matrices nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (columns_remove 0 (columns_remove-1 nil 3615024543 ("" (skeep) (("" (expand "remove") (("" (lift-if) (("" (ground) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (lemma "columns_form_matrix") (("3" (inst?) (("3" (assert) (("3" (lift-if) (("3" (ground) (("1" (replace -2) (("1" (expand "form_matrix" 1) (("1" (expand "array2list" + 1) (("1" (expand "array2list_it") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (case "rows(M)=1") (("1" (replaces -1) (("1" (assert) (("1" (expand "form_matrix" 1) (("1" (expand "array2list" + 1) (("1" (expand "array2list_it") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((remove const-decl "{N | (rows(M) > 1 AND columns(M) > 1 IMPLIES (rows(N) = rows(M) - 1 AND columns(N) = columns(M) - 1)) AND (FORALL (m, n): LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF, newn = IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF IN entry(N)(m, n) = entry(M)(newm, newn))}" matrix_props nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (rows const-decl "nat" matrices nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Matrix type-eq-decl nil matrices nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (entry const-decl "real" matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (form_matrix const-decl "{M: MatrixMN(m, n) | FORALL (i: below(m), j: below(n)): nth(row(M)(i), j) = F(i, j)}" matrices nil) (columns_form_matrix formula-decl nil matrices nil)) shostak)) (remove_remove_1_0 0 (remove_remove_1_0-1 nil 3614609488 ("" (skeep) (("" (lemma "full_matrix_eq") (("" (inst?) (("1" (assert) (("1" (hide 2) (("1" (invoke (case "NOT %1") (! 1 1)) (("1" (hide 2) (("1" (assert) (("1" (typepred "remove(D,1,1+n)") (("1" (assert) (("1" (assert) (("1" (flatten) (("1" (typepred "remove(D,0,m)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (typepred "remove(remove(D, 1, 1 + n), 0, m)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (typepred "remove(remove(D, 0, m), 0, n)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (invoke (case "NOT %1") (! 1 1)) (("1" (hide 2) (("1" (assert) (("1" (typepred "remove(D,1,1+n)") (("1" (assert) (("1" (assert) (("1" (flatten) (("1" (typepred "remove(D,0,m)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (typepred "remove(remove(D, 1, 1 + n), 0, m)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (typepred "remove(remove(D, 0, m), 0, n)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (typepred "remove(remove(D, 1, 1 + n), 0, m)") (("2" (assert) (("2" (hide (-1 -2)) (("2" (inst?) (("2" (replaces -1) (("2" (assert) (("2" (typepred "remove(remove(D, 0, m), 0, n)") (("2" (hide (-1 -2)) (("2" (inst?) (("2" (replaces -1) (("2" (assert) (("2" (typepred "remove(D,1,1+n)") (("2" (hide (-1 -2)) (("2" (inst?) (("2" (replaces -1) (("2" (typepred "remove(D,0,m)") (("2" (hide (-1 -2)) (("2" (inst?) (("2" (replaces -1) (("2" (assert) (("2" (hide (-1 -2)) (("2" (typepred "remove(D,1,1+n)") (("2" (hide (-1 -3 -4)) (("2" (assert) (("2" (flatten) (("2" (typepred "remove(D,0,m)") (("2" (hide (-1 -3 -4)) (("2" (assert) (("2" (flatten) (("2" (typepred "remove(remove(D, 1, 1 + n), 0, m)") (("2" (hide (-1 -3)) (("2" (assert) (("2" (flatten) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "remove_posfullmatrix") (("2" (inst?) (("1" (split -) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil) ("2" (typepred "remove(D,0,m)") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (lemma "remove_posfullmatrix") (("3" (inst?) (("1" (assert) nil nil) ("2" (typepred "remove(D,1,1+n)") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((full_matrix_eq formula-decl nil matrices nil) (remove_posfullmatrix judgement-tcc nil matrix_props 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" 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) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (Matrix type-eq-decl nil matrices 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (rows const-decl "nat" matrices nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (columns def-decl "{c: nat | (FORALL (i: below(length(M))): length(nth(M, i)) <= c) AND (null?(M) AND c = 0 OR (EXISTS (i: below(length(M))): length(nth(M, i)) = c))}" matrices nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (entry const-decl "real" matrices nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (remove const-decl "{N | (rows(M) > 1 AND columns(M) > 1 IMPLIES (rows(N) = rows(M) - 1 AND columns(N) = columns(M) - 1)) AND (FORALL (m, n): LET newm = IF m >= i OR i >= rows(M) THEN m + 1 ELSE m ENDIF, newn = IF n >= j OR j >= columns(M) THEN n + 1 ELSE n ENDIF IN entry(N)(m, n) = entry(M)(newm, newn))}" matrix_props nil) (FullMatrix type-eq-decl nil matrices nil) (PosFullMatrix type-eq-decl nil matrices nil) (D skolem-const-decl "PosFullMatrix" matrix_props nil) (n skolem-const-decl "nat" matrix_props nil) (m skolem-const-decl "nat" matrix_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (remove_posfullmatrix application-judgement "FullMatrix" matrix_props nil)) shostak)) (remove_remove_1_0_0 0 (remove_remove_1_0_0-1 nil 3614612404 ("" (skeep) (("" (lemma "full_matrix_eq") (("" (inst?) (("1" (assert) (("1" (hide 2) (("1" (invoke (case "NOT %1") (! 1 1)) (("1" (hide 2) (("1" (assert) (("1" (typepred "remove(D,1,0)") (("1" (assert) (("1" (assert) (("1" (flatten) (("1" (typepred "remove(D,0,1+n)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (typepred "remove(remove(D, 1, 0), 0, n)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (typepred "remove(remove(D, 0, 1+n), 0, 0)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (invoke (case "NOT %1") (! 1 1)) (("1" (hide 2) (("1" (assert) (("1" (typepred "remove(D,1,0)") (("1" (assert) (("1" (assert) (("1" (flatten) (("1" (typepred "remove(D,0,1+n)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (typepred "remove(remove(D, 1, 0), 0, n)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (typepred "remove(remove(D, 0, 1+n), 0, 0)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.31 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 |
