Quelle elementary_matrices.prf
Sprache: Lisp
(elementary_matricesnil 3522729752 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )nil naturalnumbers nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"bool" elementary_matrices nil )"boolean" notequal nil )"bool" elementary_matrices nil ))nil 3522729758 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )nil naturalnumbers nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"bool" elementary_matrices nil )"boolean" notequal nil )"bool" elementary_matrices nil ))nil 3522729771 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )nil naturalnumbers nil )nil matrices nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil ))nil 3492633163 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil integers nil )nil naturalnumbers nil )nil reals nil )nil matrices nil )"bool" matrices nil )nil matrices nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"boolean" notequal nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3492633163 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil integers nil )nil naturalnumbers nil )nil reals nil )nil matrices nil )"bool" matrices nil )nil matrices nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"boolean" notequal nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3492633163 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil integers nil )nil naturalnumbers nil )nil reals nil )nil matrices nil )"bool" matrices nil )nil matrices nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil ))nil ))nil 3492633163 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil integers nil )nil naturalnumbers nil )nil reals nil )nil matrices nil )"bool" matrices nil )nil matrices nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil ))nil ))nil 3492633163 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil integers nil )nil naturalnumbers nil )nil reals nil )nil matrices nil )"bool" matrices nil )nil matrices nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil ))nil ))nil 3492633163 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil integers nil )nil naturalnumbers nil )nil reals nil )nil matrices nil )"bool" matrices nil )nil matrices nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil ))nil ))nil 3492633163 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil integers nil )nil naturalnumbers nil )nil reals nil )nil matrices nil )"bool" matrices nil )nil matrices nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil ))nil ))nil 3500317945 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )nil matrices nil )"bool" matrices nil )nil matrices nil )"bool" matrices nil )nil matrices nil )"bool" elementary_matrices nil )nil elementary_matrices nil )"(strict_total_order?[real])" real_props nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil ))nil ))nil 3500318534 ("" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )nil matrices nil )"bool" matrices nil )nil matrices nil )"bool" matrices nil )nil matrices nil )"bool" elementary_matrices nil )nil elementary_matrices nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil ))nil ))nil 3500318534 ("" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )nil matrices nil )"bool" matrices nil )nil matrices nil )"bool" matrices nil )nil matrices nil )"bool" elementary_matrices nil )nil elementary_matrices nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil ))nil ))nil 3500318534 ("" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )nil matrices nil )"bool" matrices nil )nil matrices nil )"bool" matrices nil )nil matrices nil )"bool" elementary_matrices nil )nil elementary_matrices nil )"(strict_total_order?[real])" real_props nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil )"boolean" notequal nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil ))nil ))nil 3492635698"" (skolem-typepred)"" (prop)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (grind)"3" (inst 1 "i!1" "j!1" )"3" (skolem-typepred)"3" (prop)"1" (lift-if) (("1" (assert ) nil nil )) nil )"2" (lift-if) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" matrices nil )"bool" matrices nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"bool" elementary_matrices nil )"bool" elementary_matrices nil )"boolean" notequal nil )nil naturalnumbers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3492635698"" (skolem-typepred)"" (prop)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (expand "elemMat2?" )"3" (inst 1 "i!1" "j!1" ) (("3" (grind) nil nil )) nil )) nil ))nil ))nil )"bool" matrices nil )"bool" matrices nil )"bool" elementary_matrices nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"bool" elementary_matrices nil )"boolean" notequal nil )nil naturalnumbers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3492635698"" (skolem-typepred)"" (prop)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (expand "elemMat3?" )"3" (inst 1 "i!1" ) (("3" (grind) nil nil )) nil )) nil ))nil ))nil )"bool" matrices nil )"bool" matrices nil )"bool" elementary_matrices nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"bool" elementary_matrices nil )nil reals nil )"boolean" notequal nil )nil naturalnumbers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))"" 3520306768"" (skolem-typepred)"" (expand "invertible?" )"" (expand "elemM1?" )"" (skolem-typepred)"" "elemM1(M!1`rows)(i!1, j!1)(-(M!1`matrix(i!1, j!1)))" )"1" (prop)"1" (grind) nil nil )"2" (expand "inverse?" )"2" (prop)"1" (expand "elemM1?" )"1" (expand "elemM1" )"1" (expand "*" )"1" (apply-extensionality :hide? t)"1" (grind) nil nil )"2" (apply-extensionality :hide? t)"1" (expand "I" )"1" "1" "1" "sigma_middle[below(M!1`cols)]" )"1" "low" "0" "high" "M!1`cols-1" "i" "x!1" ))"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k_1: below(M!1`cols)): IF (k_1 = x!2) THEN 1AND (x!2 = j!1))" "LAMBDA (k_1: below(M!1`cols)): 0" "x!1-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" "LAMBDA (k_1: below(M!1`cols)): IF (k_1 = x!2) THEN 1AND (x!2 = j!1))" "LAMBDA (k_1: below(M!1`cols)): 0" "M!1`cols-1" "x!1+1" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" "x!1" "x!1" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "x!1" "n!1" )"1" assert )"1" "1" assert )nil nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "x!1" "n!1" )"2" assert )"2" assert )"2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "x!1 = i!1" )"1" "i!1" _)"1" case "x!2 = j!1" )"1" replace -1)"1" "sigma_middle[below(M!1`cols)]" )"1" "low" "0" "high" "M!1`cols-1" "i" "min(i!1,j!1)" ))"1" "1" replace -1 :hide? t)"1" "sigma_middle[below(M!1`cols)]" )"1" "low" "min(i!1,j!1)+1" "high" "M!1`cols-1" "i" "max(i!1, j!1)" ))"1" "1" replace "1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k_1: below(M!1`cols)): IF (k_1 = j!1) THEN 1" "LAMBDA (k_1: below(M!1`cols)): 0" "min(i!1,j!1)-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" "LAMBDA (k_1: below(M!1`cols)): IF (k_1 = j!1) THEN 1" "LAMBDA (k_1: below(M!1`cols)): 0" "max(i!1,j!1)-1" "min(i!1,j!1)+1" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" "LAMBDA (k_1: below(M!1`cols)): IF (k_1 = j!1) THEN 1" "LAMBDA (k_1: below(M!1`cols)): 0" "M!1`cols-1" "max(i!1,j!1)+1" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" expand "min" )"1" "1" "1" expand "max" )"1" assert )"1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "max" )"2" assert )"2" assert )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "max" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "max(i!1,j!1)" )"1" nil nil )"2" nil nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "min" )"2" "2" "1" assert )"1" expand "max" )"1" assert )nil nil ))nil ))nil )"2" expand "max" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "min(i!1,j!1)" )"1" quality 100%
¤ 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.0.18Bemerkung:
(vorverarbeitet)
¤ *Bot Zugriff
2026-03-28
