| products/sources/formale sprachen/PVS/matrices/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: notgram_ops.mli Sprache: LispOriginal von: PVS© |
|
||||||
|
(matrix_inv
(left_inv_TCC1 0 (left_inv_TCC1-1 nil 3615726331 ("" (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) (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) (Square type-eq-decl nil matrices nil) (/= const-decl "boolean" notequal nil) (det def-decl "real" matrix_props nil) (SquareMatrix 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)) (left_inv_TCC2 0 (left_inv_TCC2-1 nil 3615726331 ("" (skeep) (("" (skosimp*) nil nil)) nil) nil nil)) (left_inv_TCC3 0 (left_inv_TCC3-2 nil 3615802147 ("" (skeep) (("" (skeep) (("" (case "diagonal?(dg`ans)") (("1" (label "idz" -1) (("1" (hide "idz") (("1" (skeep) (("1" (case "NOT diagonal?(newT)") (("1" (hide 2) (("1" (replace -3 +) (("1" (expand "diagonal?") (("1" (skosimp*) (("1" (rewrite "entry_form_matrix") (("1" (lift-if) (("1" (assert) nil nil)) nil) ("2" (hide 3) (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "diagonal_simple_prod") (("2" (inst - "false" "rows(S)" "newT") (("1" (assert) (("1" (split) (("1" (case "rows(newT) = rows(S) AND columns(newT) = rows(S)") (("1" (flatten) (("1" (assert) (("1" (rewrite "matrix_mult_assoc") (("1" (rewrite "full_matrix_eq") (("1" (split) (("1" (rewrite "rows_mult") (("1" (assert) nil nil)) nil) ("2" (rewrite "columns_mult") (("1" (assert) (("1" (rewrite "columns_mult") (("1" (assert) nil nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "rows") (("2" (expand "length" -2 1) (("2" (rewrite "length_rows" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (rewrite "entry_mult") (("3" (lift-if) (("3" (split 1) (("1" (flatten) (("1" (expand "*" + 1) (("1" (rewrite "dot_eq_sigma") (("1" (rewrite "length_row") (("1" (replace -4) (("1" (rewrite "length_col") (("1" (rewrite "rows_mult") (("1" (expand "min" 1) (("1" (rewrite "entry_Id") (("1" (assert) (("1" (rewrite "columns_mult" -2) (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (rewrite "sigma_restrict_eq_0") (("1" (hide 3) (("1" (skosimp*) (("1" (rewrite "access_row") (("1" (rewrite "access_col") (("1" (case "i!1 = i!2") (("1" (typepred "dg") (("1" (assert) (("1" (replace -16 :dir rl) (("1" (replace -3) (("1" (reveal "idz") (("1" (expand "diagonal?") (("1" (inst - "i!2" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "diagonal?") (("2" (inst - "i!1" "i!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (lemma "sigma_eq_one_arg2") (("2" (inst?) (("2" (inst - "j!1") (("2" (assert) (("2" (split -1) (("1" (replaces -1) (("1" (rewrite "access_row") (("1" (rewrite "access_col") (("1" (typepred "dg") (("1" (assert) (("1" (replace -16 1) (("1" (rewrite "entry_form_matrix") (("1" (assert) (("1" (lift-if) (("1" (split +) (("1" (flatten) (("1" (lemma "det_upper_triangular_zero") (("1" (inst - "R*S") (("1" (assert) (("1" (inst + "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (rewrite "access_row") (("2" (rewrite "access_col") (("2" (typepred "dg") (("2" (reveal "idz") (("2" (expand "diagonal?") (("2" (inst - "i!2" "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "columns_mult" 1) (("1" (assert) (("1" (rewrite "entry_eq_0") (("1" (ground) nil nil)) nil)) nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "R") (("2" (expand "rows") (("2" (expand "length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -5 1) (("2" (rewrite "rows_form_matrix") (("1" (lemma "columns_form_matrix") (("1" (inst?) (("1" (assert) nil nil) ("2" (skosimp*) nil nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "rows_mult") (("2" (assert) (("2" (replace -5 1) (("2" (rewrite "rows_form_matrix") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("3" (rewrite "rows_mult") (("3" (rewrite "columns_mult" 1) (("1" (replace -5 1) (("1" (rewrite "rows_form_matrix") (("1" (assert) nil nil) ("2" (skosimp*) nil nil)) nil)) nil) ("2" (typepred "newT") (("2" (expand "rows") (("2" (lemma "rows_form_matrix") (("2" (inst?) (("1" (assert) (("1" (expand "rows" -1) (("1" (expand "length" -1 1) (("1" (rewrite "length_rows" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (rewrite "rows_mult") (("4" (replace -5) (("4" (rewrite "rows_form_matrix") (("1" (assert) nil nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil) ("5" (rewrite "columns_mult" 1) (("1" (assert) nil nil) ("2" (lemma "rows_form_matrix") (("2" (inst?) (("1" (assert) (("1" (expand "rows" -1 1) (("1" (expand "length" -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "rows(newT) = rows(S)") (("1" (case "columns(newT) = rows(S)") (("1" (assert) (("1" (flatten) (("1" (lemma "form_matrix_square") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst - "i!1" "j!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -5 +) (("2" (lemma "columns_form_matrix") (("2" (inst?) (("1" (assert) nil nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4 1) (("2" (rewrite "rows_form_matrix") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "dg") (("2" (assert) (("2" (expand "diagonal?") (("2" (skosimp*) (("2" (inst - "i!1" "j!1") (("2" (inst - "i!1" "j!1") (("2" (assert) (("2" (rewrite "entry_eq_0" 3) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((diagonal_simple_prod formula-decl nil matrix_det 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) (form_matrix_square judgement-tcc nil matrices nil) (mult_full application-judgement "FullMatrix" matrices nil) (Id const-decl "{M: SquareMatrix(pm) | (FORALL (i, j): entry(M)(i, j) = IF i < pm AND i = j THEN 1 ELSE 0 ENDIF) AND (FORALL (pn: posnat, N: MatrixMN(pm, pn)): M * N = N) AND (FORALL (pn: posnat, N: MatrixMN(pn, pm)): N * M = N)}" matrices nil) (full_matrix_eq formula-decl nil matrices nil) (entry_eq_0 formula-decl nil matrices nil) (dot_eq_sigma formula-decl nil matrices nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (entry_Id formula-decl nil matrices nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_eq_one_arg2 formula-decl nil sigma "reals/") (det_upper_triangular_zero formula-decl nil matrix_det nil) (subrange type-eq-decl nil integers nil) (access_row formula-decl nil matrices nil) (access_col formula-decl nil matrices nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (access const-decl "real" matrices nil) (T_high type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (T_low type-eq-decl nil sigma "reals/") (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (length_col formula-decl nil matrices nil) (length_row formula-decl nil matrices nil) (entry_mult formula-decl nil matrices nil) (columns_mult formula-decl nil matrices nil) (length_rows formula-decl nil matrices nil) (rows_mult formula-decl nil matrices nil) (matrix_mult_assoc formula-decl nil matrices nil) (columns_form_matrix formula-decl nil matrices nil) (rows_form_matrix formula-decl nil matrices nil) (newT skolem-const-decl "{M: MatrixMN(rows(S), rows(S)) | FORALL (i_1: below(rows(S)), j_1: below(rows(S))): nth(row(M)(i_1), j_1) = IF i_1 /= j_1 OR entry(R * S)(i_1, i_1) = 0 THEN 0 ELSE 1 / entry(R * S)(i_1, i_1) ENDIF}" matrix_inv nil) (R skolem-const-decl "SquareMatrix(rows(S))" matrix_inv nil) (S skolem-const-decl "{S | det(S) /= 0}" matrix_inv nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (entry_form_matrix formula-decl nil matrices nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (form_matrix_square application-judgement "FullMatrix" matrices nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (NOT const-decl "[bool -> bool]" booleans 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) (diagonal? const-decl "bool" matrix_det nil) (SquareMatrix 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) (rows const-decl "nat" matrices nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt 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) (Square type-eq-decl nil matrices nil) (/= const-decl "boolean" notequal nil) (det def-decl "real" matrix_props nil) (upper_triangular? const-decl "bool" matrix_det nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (entry const-decl "real" matrices nil) (MatrixMN type-eq-decl nil matrices nil) (Vector type-eq-decl nil matrices nil) (* const-decl "real" matrices nil) (row const-decl "Vector" matrices nil) (VectorN type-eq-decl nil matrices nil) (col def-decl "VectorN(rows(M))" matrices nil) (* const-decl "{A: MatrixMN(rows(M), columns(N)) | FORALL (i, j): entry(A)(i, j) = row(M)(i) * col(N)(j)}" matrices nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (is_simple_prod? const-decl "bool" matrix_det nil) (FALSE const-decl "bool" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil)) nil) (left_inv_TCC3-1 nil 3615726331 ("" (skeep) (("" (skeep) (("" (skeep) (("" (label "newTname" -3) (("" (split +) (("1" (rewrite "matrix_mult_assoc") (("1" (label "Rname" -2) (("1" (typepred "dg") (("1" (replace "Rname" :dir rl) (("1" (assert) (("1" (replace -3) (("1" (rewrite "full_matrix_eq" 1) (("1" (assert) (("1" (case "NOT (rows(newT * dg`ans) = rows(Id(rows(S))) AND columns(newT * dg`ans) = columns(Id(rows(S))))") (("1" (hide 2) (("1" (rewrite "rows_mult") (("1" (rewrite "columns_mult") (("1" (assert) (("1" (replace "newTname" 1) (("1" (rewrite "rows_form_matrix") (("1" (assert) nil nil) ("2" (hide 2) (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "newT") (("2" (expand "length" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (skeep) (("2" (typepred "i") (("2" (typepred "j") (("2" (assert) (("2" (rewrite "entry_Id" 1) (("2" (rewrite "entry_mult" 1) (("2" (assert) (("2" (case "NOT rows(newT)=rows(S)") (("1" (replace "newTname" 1) (("1" (rewrite "rows_form_matrix") (("1" (skosimp*) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "*" 1) (("2" (rewrite "dot_eq_sigma") (("2" (case "NOT columns(newT)=columns(S)") (("1" (assert) (("1" (replace "newTname" 1) (("1" (lemma "columns_form_matrix") (("1" (inst?) (("1" (assert) nil nil) ("2" (hide 2) (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "length_col" 1) (("2" (rewrite "length_row" 1) (("1" (expand "min") (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (lift-if) (("1" (split 1) (("1" (flatten) (("1" (rewrite "sigma_restrict_eq_0") (("1" (hide 3) (("1" (skosimp*) (("1" (rewrite "access_row") (("1" (rewrite "access_col") (("1" (case "i!1 = i") (("1" (inst - "i!1" "j") (("1" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) 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" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (mult_left_inv_right_TCC1 0 (mult_left_inv_right_TCC1-1 nil 3615802707 ("" (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) (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) (Square type-eq-decl nil matrices nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (rows const-decl "nat" matrices nil)) nil)) (mult_left_inv_right 0 (mult_left_inv_right-1 nil 3615802708 ("" (skeep) (("" (typepred "left_inv(S)") (("" (case "NOT (left_inv(S) * S)*left_inv(S) = Id(rows(S))*left_inv(S)") (("1" (assert) nil nil) ("2" (rewrite "mult_Id_left") (("2" (rewrite "matrix_mult_assoc") (("1" (case "NOT det(left_inv(S))/=0") (("1" (flatten) (("1" (case "NOT det(left_inv(S)*S) = det(Id(rows(S)))") (("1" (assert) nil nil) ("2" (rewrite "det_mult") (("2" (rewrite "det_Id") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.79 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 |
