SSL 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" 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 )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil )"4" "4" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" 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 ))nil )"2" "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" "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" "2" "n!1" )"1" assert )"1" assert )"1" "1" assert )nil nil )"2" assert )nil nil )"3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "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" "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" "2" "x!1" "n!1" )"1" assert )"1" "1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -4) (("2" (grind) nil nil ))nil )"3" (skolem-typepred)"3" "3" assert )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil )"4" (skolem-typepred)"4" "4" (assert ) nil nil ))nil ))nil )"5" (hide -4) (("5" (grind) nil nil ))nil ))nil )"3" (hide -4) (("3" (grind) nil nil )) nil )"4" (hide -4) (("4" (grind) nil nil )) nil )"5" (hide -4) (("5" (grind) nil nil )) nil )"6" (hide -4) (("6" (grind) nil nil )) nil )"7" (hide -4)"7" (skolem-typepred)"7" "7" (assert ) nil nil ))nil ))nil ))nil )"8" (hide -4) (("8" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "elemM1" )"2" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (apply-extensionality :hide? t)"1" (expand "I" )"1" (assert )"1" (expand "*" )"1" "1" "1" expand "elemM1?" )"1" "sigma_middle[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1) THEN 1AND (k_1 = j!1))" "M!1`rows-1" "x!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1) THEN 1AND (k_1 = j!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "x!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" assert )"1" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1) THEN 1AND (k_1 = j!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "M!1`rows-1" "x!1+1" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" "x!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" "n!1" "x!2" )"1" assert )nil nil ))nil )"2" "n!1" "x!2" )"2" assert )nil nil ))nil )"3" assert )nil nil )"4" "n!1" "x!2" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil )"2" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil )"3" assert )nil nil )"4" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" "3" "x!2" )"3" (grind) nil nil ))nil ))nil ))nil )"4" "4" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" expand "elemM1?" )"2" case "x!1 = i!1" )"1" case "x!2 = j!1" )"1" replace -1)"1" replace -2)"1" "sigma_middle[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (i!1 = k_1) THEN 1" "M!1`rows-1" "min(i!1,j!1)" "0" )"1" "1" replace "1" "LAMBDA (k_1: below(M!1`rows)): IF (i!1 = k_1) THEN 1" "M!1`rows-1" "max(i!1,j!1)" "min(i!1,j!1)+1" )"1" "1" replace "1" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (i!1 = k_1) THEN 1" "LAMBDA (k_1: below(M!1`rows)): 0" "min(i!1, j!1) - 1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" assert )"1" "LAMBDA (k_1: below(M!1`rows)): IF (i!1 = k_1) THEN 1" "LAMBDA (k_1: below(M!1`rows)): 0" "max(i!1, j!1)-1" "min(i!1, j!1)+1" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" assert )"1" "LAMBDA (k_1: below(M!1`rows)): IF (i!1 = k_1) THEN 1" "LAMBDA (k_1: below(M!1`rows)): 0" "M!1`rows-1" "max(i!1, j!1)+1" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" assert )"1" expand "min" )"1" "1" "1" expand "max" )"1" assert )"1" "j!1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "max" )"2" assert )"2" "j!1" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "max" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "min" )"2" expand "max" )"2" assert )"2" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "min" )"2" "2" "1" "n!1" "j!1" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil )"3" "3" nil nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil )"4" "4" nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1) THEN 1AND (k_1 = j!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "M!1`rows-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`rows)]" )nil nil ))nil )"2" "2" assert )"2" "2" "2" "1" "n!1" "x!2" )"1" assert )nil nil )"2" assert )"2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil )"3" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil )"3" "3" "x!2" )"3" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1) THEN 1AND (k_1 = j!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "M!1`rows-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`rows)]" )nil nil ))nil )"2" "2" "2" "2" "1" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil )"2" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil )"3" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil )"4" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" 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 )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(identity?)" matrices nil )identity ? const-decl "bool" matrices nil )"[bool, bool -> bool]" booleans nil )nil integers nil )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"real" reals nil )"below(M!1`rows)" elementary_matrices nil )"below(M!1`rows)" elementary_matrices nil )"real" reals nil )"(total_order?[real])" nil )"posint" nil )nil integers nil )"subrange(1 + x!1, M!1`cols - 1)" nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"subrange(0, M!1`cols - 1)" nil )"subrange(0, M!1`cols - 1)" nil )"{k: nat | k <= i AND k <= j}" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"Matrix" matrices nil )"bool" elementary_matrices nil )"nnreal" vectors "vectors/" )"nat" vectors "vectors/" )"below(((# rows := M!1`rows, LAMBDA (k, l: below(M!1`rows)):IF k = l THEN 1AND l = j!1 THEN -(M!1`matrix(i!1, j!1))" elementary_matrices nil) "below(((# rows := M!1`rows, LAMBDA (k, l: below(M!1`rows)):IF k = l THEN 1AND l = j!1 THEN -(M!1`matrix(i!1, j!1))" elementary_matrices nil) "subrange(0, min(i!1, j!1) - 1)" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{j: below(M!1`rows) | i!1 /= j}" nil )"below(M!1`rows)" elementary_matrices nil )"ElemM1" elementary_matrices nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"ElemMat1(n)" elementary_matrices nil )nil elementary_matrices nil )"bool" elementary_matrices nil )nil matrices nil )"bool" matrices nil )"bool" reals nil )nil integers nil )"bool" matrices nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil elementary_matrices nil )"bool" elementary_matrices nil )nil matrices nil )"bool" matrices nil )nil matrices nil )nil reals nil )nil naturalnumbers nil )nil integers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3492633168"" (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 ))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 )"2" "1" assert )nil nil )"2" assert )nil nil ))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" 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 )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil )"4" "4" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "sigma_eq[below(M!1`cols)]" )"2" "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" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" "2" "n!1" )"1" assert )"1" assert )"1" "1" assert )nil nil )"2" assert )nil nil )"3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "sigma_eq[below(M!1`cols)]" )"2" "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" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" "2" "x!1" "n!1" )"1" assert )"1" "1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -4) (("2" (grind) nil nil ))nil )"3" (skolem-typepred)"3" "3" (assert ) nil nil ))nil ))nil )"4" (skolem-typepred)"4" "4" (assert ) nil nil ))nil ))nil ))nil )"3" (hide -4) (("3" (grind) nil nil )) nil )"4" (hide -4) (("4" (grind) nil nil )) nil )"5" (hide -4) (("5" (grind) nil nil )) nil )"6" (hide -4) (("6" (grind) nil nil )) nil )"7" (hide -4)"7" (skolem-typepred)"7" "7" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "elemM1" )"2" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (apply-extensionality :hide? t)"1" (expand "I" )"1" (assert )"1" (expand "*" )"1" "1" "1" expand "elemM1?" )"1" "sigma_middle[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1) THEN 1AND (k_1 = j!1))" "M!1`rows-1" "x!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1) THEN 1AND (k_1 = j!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "x!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" assert )"1" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1) THEN 1AND (k_1 = j!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "M!1`rows-1" "x!1+1" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" "x!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" "n!1" "x!2" )"1" assert )nil nil ))nil )"2" "n!1" "x!2" )"2" assert )nil nil ))nil )"3" assert )nil nil )"4" "n!1" "x!2" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil )"2" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil )"3" assert )nil nil )"4" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" "3" "x!2" )"3" (grind) nil nil ))nil ))nil ))nil )"4" "4" (grind) nil nil ))nil ))nil ))nil ))nil )"2" expand "elemM1?" )"2" case "x!1 = i!1" )"1" case "x!2 = j!1" )"1" replace -1)"1" replace -2)"1" "sigma_middle[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (i!1 = k_1) THEN 1" "M!1`rows-1" "min(i!1,j!1)" "0" )"1" "1" replace "1" "LAMBDA (k_1: below(M!1`rows)): IF (i!1 = k_1) THEN 1" "M!1`rows-1" "max(i!1,j!1)" "min(i!1,j!1)+1" )"1" "1" replace "1" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (i!1 = k_1) THEN 1" "LAMBDA (k_1: below(M!1`rows)): 0" "min(i!1, j!1) - 1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" assert )"1" "LAMBDA (k_1: below(M!1`rows)): IF (i!1 = k_1) THEN 1" "LAMBDA (k_1: below(M!1`rows)): 0" "max(i!1, j!1)-1" "min(i!1, j!1)+1" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" assert )"1" "LAMBDA (k_1: below(M!1`rows)): IF (i!1 = k_1) THEN 1" "LAMBDA (k_1: below(M!1`rows)): 0" "M!1`rows-1" "max(i!1, j!1)+1" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" assert )"1" expand "min" )"1" "1" "1" expand "max" )"1" assert )"1" "j!1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "max" )"2" assert )"2" "j!1" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "max" )"2" assert )"2" "2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "min" )"2" expand "max" )"2" assert )"2" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "min" )"2" "2" "1" "n!1" "j!1" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil )"3" "3" nil nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil )"4" "4" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "sigma_eq[below(M!1`rows)]" )"2" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1) THEN 1AND (k_1 = j!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "M!1`rows-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`rows)]" )nil nil ))nil )"2" "2" assert )"2" "2" "2" "1" "n!1" "x!2" )"1" assert )nil nil )"2" assert )"2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil )"3" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil )"3" "3" "x!2" )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "sigma_eq[below(M!1`rows)]" )"2" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1) THEN 1AND (k_1 = j!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "M!1`rows-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`rows)]" )nil nil ))nil )"2" "2" "2" "2" "1" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil )"2" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil )"3" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil )"4" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )"bool" matrices nil )nil matrices nil )"bool" matrices nil )"bool" matrices nil )nil matrices nil )"nat" vectors "vectors/" )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )identity ? const-decl "bool" matrices nil )"(identity?)" matrices nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" matrices nil ))"" 3520306846"" (skolem-typepred)"" (expand "invertible?" )"" (expand "elemM2?" )"" (skolem-typepred)"" (inst 1 "M!1" )"" (expand "inverse?" )"" (assert )"" (case "(M!1 * M!1) = I(M!1`rows)" )"1" (assert ) nil nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (apply-extensionality :hide? t)"3" (expand "*" )"3" (expand "I" )"3" (expand "elemM2?" )"3" "3" "1" case "x!1 = i!1" )"1" "sigma_middle[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "M!1`cols-1" "j!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "j!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "j!1+1" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" "i!1" "j!1" )"1" "j!1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" 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 )"5" "5" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" case "x!1 = j!1" )"1" "sigma_middle[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "M!1`cols-1" "i!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "i!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "i!1+1" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" "i!1" "j!1" )"1" "j!1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" (assert ) nil nil ))nil )"2" assert )"2" "2" (grind) nil nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" (grind) nil nil ))nil )"5" "5" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "sigma_middle[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "M!1`cols-1" "x!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "x!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "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" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" "3" "x!2" )"3" (grind) nil nil ))nil ))nil ))nil )"4" "4" (grind) nil nil ))nil )"5" "5" "5" "x!2" )"5" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" case "x!1 = i!1" )"1" case "x!2 = j!1" )"1" replace -1 :hide? t)"1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" case "n!1 = i!1" )"1" "i!1" "n!1" )"1" assert )nil nil ))nil )"2" case "n!1 = j!1" )"1" "n!1" "j!1" )"1" assert )nil nil ))nil )"2" "i!1" "n!1" )"2" assert )nil 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 ))nil ))nil ))nil )"2" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" case "n!1 = x!1" )"1" "x!1" "n!1" )"1" assert )nil nil ))nil )"2" replace -3 :hide? t)"2" "n!1" "x!2" )"1" assert )"1" "1" replace "1" "i!1" "n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" case "x!1 = j!1" )"1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" case "n!1 = i!1" )"1" replace "1" "i!1" "x!2" )"1" assert )nil nil )"2" assert )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "j!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" assert )"2" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )"2" "2" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" "4" "x!1" )"4" nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" 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 )"Matrix" matrices nil )nil integers nil )"bool" reals nil )identity ? const-decl "bool" matrices nil )"(identity?)" matrices nil )"int" integers nil )"real" reals nil )"real" sigma "reals/" )"bool" elementary_matrices nil )nil sigma "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil integers nil )nil sigma "reals/" )nil sigma "reals/" )"posint" nil )"posint" nil )"(total_order?[real])" nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"nnreal" vectors "vectors/" )"nat" vectors "vectors/" )"real" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"{j: below(M!1`rows) | i!1 /= j}" nil )"below(M!1`rows)" elementary_matrices nil )"below((M!1 * M!1)`cols)" nil )"below((M!1 * M!1)`rows)" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"ElemM2" elementary_matrices nil )"[T, T -> boolean]" equalities nil )"bool" matrices nil )nil elementary_matrices nil )"bool" elementary_matrices nil )nil matrices nil )"bool" matrices nil )nil matrices nil )nil reals nil )nil naturalnumbers nil )nil integers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3492745295"" (skolem-typepred)"" (expand "invertible?" )"" (expand "elemM2?" )"" (skolem-typepred)"" (inst 1 "M!1" )"" (expand "inverse?" )"" (assert )"" (case "(M!1 * M!1) = I(M!1`rows)" )"1" (assert ) nil nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (apply-extensionality :hide? t)"3" (expand "*" )"3" (expand "I" )"3" (expand "elemM2?" )"3" "3" "1" case "x!1 = i!1" )"1" "sigma_middle[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "M!1`cols-1" "j!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "j!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "j!1+1" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" "i!1" "j!1" )"1" "j!1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" 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 )"5" "5" (grind) nil nil ))nil ))nil ))nil )"2" case "x!1 = j!1" )"1" "sigma_middle[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "M!1`cols-1" "i!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "i!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "i!1+1" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" "i!1" "j!1" )"1" "j!1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" (assert ) nil nil ))nil )"2" assert )"2" "2" (grind) nil nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" (grind) nil nil ))nil )"5" "5" (grind) nil nil ))nil ))nil ))nil )"2" "sigma_middle[below(M!1`cols)]" )"2" "LAMBDA (k: below(M!1`cols)): " "M!1`cols-1" "x!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "x!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "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" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" "3" "x!2" )"3" (grind) nil nil ))nil ))nil ))nil )"4" "4" (grind) nil nil ))nil )"5" "5" "5" "x!2" )"5" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "x!1 = i!1" )"1" case "x!2 = j!1" )"1" replace -1 :hide? t)"1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" case "n!1 = i!1" )"1" "i!1" "n!1" )"1" assert )nil nil ))nil )"2" case "n!1 = j!1" )"1" "n!1" "j!1" )"1" assert )nil nil ))nil )"2" "i!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "sigma_eq[below(M!1`cols)]" )"2" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" case "n!1 = x!1" )"1" "x!1" "n!1" )"1" assert )nil nil ))nil )"2" replace -3 :hide? t)"2" "n!1" "x!2" )"1" assert )"1" "1" replace "1" "i!1" "n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" (grind) nil nil ))nil ))nil ))nil ))nil )"2" case "x!1 = j!1" )"1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" case "n!1 = i!1" )"1" replace "1" "i!1" "x!2" )"1" assert )nil nil )"2" assert )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "j!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "sigma_eq[below(M!1`cols)]" )"2" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: " "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" "x!1" "n!1" )"2" assert )"2" "2" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" "4" "x!1" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil matrices nil )"bool" matrices nil )nil matrices nil )"bool" matrices nil )nil sigma "reals/" )nil sigma "reals/" )"nat" vectors "vectors/" )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"(identity?)" matrices nil )identity ? const-decl "bool" matrices nil )"bool" matrices nil ))"" 3520307266"" (skolem-typepred)"" (expand "invertible?" )"" (expand "elemM3?" )"" (skolem-typepred)"" (inst 1 "elemM3(M!1`rows)(i!1)(1/M!1`matrix(i!1,i!1))" )"1" (prop)"1" (grind) nil nil )"2" (expand "inverse?" )"2" (expand "elemM3?" )"2" (prop)"1" (expand "*" )"1" (expand "I" )"1" (prop)"1" (grind) nil nil )"2" (apply-extensionality :hide? t)"1" (lift-if)"1" "1" expand "elemM3" )"1" case "x!1 = i!1" )"1" "sigma_middle[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "M!1`cols-1" "i!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k: below(M!1`cols)): 0" "i!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k: below(M!1`cols)): 0" "M!1`cols-1" "i!1+1" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "x!1" "n!1" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "i!1" "i!1" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i!1" "i!1" )"2" assert )"2" nil nil ))nil ))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" "3" "3" "i!1" "i!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "sigma_middle[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "M!1`cols-1" "x!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k: below(M!1`cols)): 0" "x!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k: below(M!1`cols)): 0" "M!1`cols-1" "x!1+1" )"1" "1" replace "1" "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" "x!1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" "n!1" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "i!1" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "i!1" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" 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" "3" "3" "i!1" "i!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: below(M!1`cols)): 0" "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" "2" expand "elemM3" )"2" "2" assert )"2" "1" "x!1" "n!1" )"1" assert )nil nil )"2" assert )nil nil ))nil )"2" "x!1" "n!1" )"1" assert )nil nil )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i!1" "i!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" "4" "4" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (hide -3) (("2" (grind) nil nil ))nil )"3" (skolem-typepred)"3" assert )"3" "3" (grind) nil nil ))nil ))nil ))nil )"4" (hide -3)"4" "4" "4" "i!1" "i!1" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil )"5" (skolem-typepred)"5" expand "elemM3" )"5" assert )"5" "5" (grind) nil nil ))nil ))nil ))nil ))nil )"6" (hide -3) (("6" (grind) nil nil ))nil )"7" (hide -3) (("7" (grind) nil nil ))nil )"8" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (expand "elemM3" )"2" (expand "I" )"2" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (apply-extensionality :hide? t)"1" (lift-if)"1" expand "*" )"1" "1" "sigma_middle[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1)IF (x!1 = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "M!1`rows-1" "x!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1)IF (x!1 = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "x!1-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1)IF (x!1 = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "M!1`rows-1" "x!1+1" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" assert )"1" "1" "1" "i!1" "i!1" )"1" assert )nil nil ))nil )"2" "x!1" "x!2" )"1" assert )nil nil )"2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "2" "i!1" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "2" "i!1" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" "3" "x!2" )"3" (grind) nil nil ))nil ))nil ))nil )"4" "4" "4" "4" "i!1" "i!1" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil )"5" "5" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1)IF (x!1 = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "M!1`rows-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`rows)]" )nil nil ))nil )"2" "2" "2" assert )"2" "2" "1" "n!1" "x!2" )"1" assert )nil nil )"2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil )"2" "n!1" "x!2" )"1" assert )nil nil )"2" "x!2" )"2" nil nil ))nil ))nil )"3" "n!1" "x!2" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" "3" "3" "i!1" "i!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" "4" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3) (("2" (grind) nil nil ))nil )"3" (skolem-typepred)"3" "3" "i!1" "i!1" )"3" (assert ) nil nil ))nil ))nil ))nil )"4" (hide -3) (("4" (grind) nil nil ))nil ))nil )"4" (skolem-typepred)"4" (flatten)"4" "i!1" "i!1" )"4" (assert ) nil nil ))nil ))nil ))nil )"5" (hide -3) (("5" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "elemM3?" )"2" (inst -3 "i!1" "i!1" ) (("2" (assert ) nil nil ))nil ))nil )"3" (hide -3) (("3" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" 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 )"bool" elementary_matrices nil )"below(((# rows := M!1`rows, LAMBDA (k, l: below(M!1`rows)):IF k = lIF k = i!1 THEN 1 / M!1`matrix(i!1, i!1)" elementary_matrices nil) "below(((# rows := M!1`rows, LAMBDA (k, l: below(M!1`rows)):IF k = lIF k = i!1 THEN 1 / M!1`matrix(i!1, i!1)" elementary_matrices nil) "Matrix" matrices nil )"subrange(0, M!1`cols - 1)" nil )"subrange(1 + x!1, M!1`cols - 1)" nil )"below(M!1`rows)" elementary_matrices nil )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"real" reals nil )nil integers nil )"posint" nil )"subrange(1 + i!1, M!1`cols - 1)" nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"below(elemM3(M!1`rows)(i!1)(1 / M!1`matrix(i!1, i!1))`cols)" nil )"(total_order?[real])" nil )"real" reals nil )"int" integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"(identity?)" matrices nil )AND const-decl "[bool, bool -> bool]" booleans nil )"below(M!1`rows)" elementary_matrices nil )"ElemM3" elementary_matrices nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"ElemMat3(n)" elementary_matrices nil )nil elementary_matrices nil )"bool" elementary_matrices nil )nil matrices nil )"bool" matrices nil )nil reals nil )"boolean" notequal nil )"bool" reals nil )nil integers nil )"bool" matrices nil )"[T, T -> boolean]" equalities nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )nil elementary_matrices nil )"bool" elementary_matrices nil )nil matrices nil )"bool" matrices nil )nil matrices nil )nil reals nil )nil naturalnumbers nil )nil integers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3492821906"" (skolem-typepred)"" (expand "invertible?" )"" (expand "elemM3?" )"" (skolem-typepred)"" (inst 1 "elemM3(M!1`rows)(i!1)(1/M!1`matrix(i!1,i!1))" )"1" (prop)"1" (grind) nil nil )"2" (expand "inverse?" )"2" (expand "elemM3?" )"2" (prop)"1" (expand "*" )"1" (expand "I" )"1" (prop)"1" (grind) nil nil )"2" (apply-extensionality :hide? t)"1" (lift-if)"1" "1" expand "elemM3" )"1" case "x!1 = i!1" )"1" "sigma_middle[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "M!1`cols-1" "i!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k: below(M!1`cols)): 0" "i!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k: below(M!1`cols)): 0" "M!1`cols-1" "i!1+1" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "x!1" "n!1" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "i!1" "i!1" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i!1" "i!1" )"2" assert )"2" nil nil ))nil ))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" "3" "3" "i!1" "i!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" "4" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "sigma_middle[below(M!1`cols)]" )"2" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "M!1`cols-1" "x!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`cols)]" )"1" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k: below(M!1`cols)): 0" "x!1-1" "0" )"1" "1" replace "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" "LAMBDA (k: below(M!1`cols)): IF (k = x!2)IF (k = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k: below(M!1`cols)): 0" "M!1`cols-1" "x!1+1" )"1" "1" replace "1" "1" "sigma_zero[below(M!1`cols)]" )"1" replace "1" assert )"1" "x!1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" "n!1" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "i!1" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "i!1" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" 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" "3" "3" "i!1" "i!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"4" "4" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "sigma_eq[below(M!1`cols)]" )"2" "LAMBDA (k: below(M!1`cols)): " "LAMBDA (k: below(M!1`cols)): 0" "M!1`cols-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`cols)]" )nil nil ))nil )"2" "2" "2" expand "elemM3" )"2" "2" assert )"2" "1" "x!1" "n!1" )"1" assert )nil nil )"2" assert )nil nil ))nil )"2" "x!1" "n!1" )"1" assert )nil nil )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i!1" "i!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" "4" "4" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3) (("2" (grind) nil nil ))nil )"3" (skolem-typepred)"3" "i!1" "i!1" )"3" (assert ) nil nil ))nil ))nil )"4" (hide -3) (("4" (grind) nil nil ))nil )"5" (skolem-typepred)"5" expand "elemM3" )"5" assert )"5" "5" (grind) nil nil ))nil ))nil ))nil ))nil )"6" (hide -3) (("6" (grind) nil nil ))nil )"7" (hide -3) (("7" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "elemM3" )"2" (expand "I" )"2" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (apply-extensionality :hide? t)"1" (lift-if)"1" expand "*" )"1" "1" "sigma_middle[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1)IF (x!1 = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "M!1`rows-1" "x!1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1)IF (x!1 = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "x!1-1" "0" )"1" "1" replace -1 :hide? t)"1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" "sigma_eq[below(M!1`rows)]" )"1" "LAMBDA (k_1: below(M!1`rows)): IF (x!1 = k_1)IF (x!1 = i!1) THEN (1 / M!1`matrix(i!1, i!1))" "LAMBDA (k_1: below(M!1`rows)): 0" "M!1`rows-1" "x!1+1" )"1" "1" replace "1" "sigma_zero[below(M!1`rows)]" )"1" replace "1" assert )"1" "1" "1" "i!1" "i!1" )"1" assert )nil nil ))nil )"2" "x!1" "x!2" )"1" assert )nil nil )"2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "2" "i!1" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "2" "i!1" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"2" "2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil )"3" "3" "3" "x!2" )"3" (grind) nil nil ))nil ))nil ))nil )"4" "4" "4" "4" "i!1" "i!1" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil )"5"
Messung V0.5 in Prozent C=100 H=100 G=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.905Bemerkung:
(vorverarbeitet am 2026-05-02)
¤ *Bot Zugriff
2026-05-26
