|
(matrices
(det_id 0
(det_id-1 nil 3254652082 ("" (grind) nil nil)
((id const-decl "Mat3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(det const-decl "real" matrices nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(det_T 0
(det_T-1 nil 3254652082 ("" (grind) nil nil)
((det const-decl "real" matrices nil)
(T const-decl "Mat3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(id_left1 0
(id_left1-1 nil 3254652082
("" (skolem 1 "m")
(("" (decompose-equality 1) (("" (grind) nil nil)) nil)) nil)
((Mat3 type-eq-decl nil matrices nil)
(* const-decl "Mat3" matrices nil)
(id const-decl "Mat3" matrices nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(mat3 const-decl "Mat3" matrices nil)
(row const-decl "Vect3" matrices nil)
(col const-decl "Vect3" matrices nil)
(vect3 const-decl "Vect3" vect3D nil)
(sigma def-decl "real" sigma "reals/")
(* const-decl "real" vectors nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(id_right1 0
(id_right1-1 nil 3254652082
("" (skolem 1 "m")
(("" (decompose-equality 1) (("" (grind) nil nil)) nil)) nil)
((Mat3 type-eq-decl nil matrices nil)
(* const-decl "Mat3" matrices nil)
(id const-decl "Mat3" matrices nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(row const-decl "Vect3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(col const-decl "Vect3" matrices nil)
(vect3 const-decl "Vect3" vect3D nil)
(sigma def-decl "real" sigma "reals/")
(* const-decl "real" vectors nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(id_left2 0
(id_left2-1 nil 3254652082
("" (skolem 1 "v")
(("" (decompose-equality 1) (("" (grind) nil nil)) nil)) nil)
((below type-eq-decl nil naturalnumbers nil)
(Mat3 type-eq-decl nil matrices nil)
(Vect3 type-eq-decl nil vect3D nil)
(* const-decl "Vect3" matrices nil)
(id const-decl "Mat3" matrices nil)
(Index type-eq-decl nil vectors nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(* const-decl "real" vectors nil)
(sigma def-decl "real" sigma "reals/")
(vect3 const-decl "Vect3" vect3D nil)
(row const-decl "Vect3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(id_right2 0
(id_right2-1 nil 3254652082
("" (skolem 1 "v")
(("" (decompose-equality 1) (("" (grind) nil nil)) nil)) nil)
((Vect3 type-eq-decl nil vect3D nil)
(below type-eq-decl nil naturalnumbers nil)
(Mat3 type-eq-decl nil matrices nil)
(* const-decl "Vect3" matrices nil)
(id const-decl "Mat3" matrices nil)
(Index type-eq-decl nil vectors nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(* const-decl "real" vectors nil)
(sigma def-decl "real" sigma "reals/")
(vect3 const-decl "Vect3" vect3D nil)
(col const-decl "Vect3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(associativity_1 0
(associativity_1-1 nil 3254652082 ("" (grind) nil nil)
((row const-decl "Vect3" matrices nil)
(col const-decl "Vect3" matrices nil)
(vect3 const-decl "Vect3" vect3D nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sigma def-decl "real" sigma "reals/")
(* const-decl "real" vectors nil)
(* const-decl "Mat3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(associativity_2 0
(associativity_2-1 nil 3254652082 ("" (grind) nil nil)
((row const-decl "Vect3" matrices nil)
(col const-decl "Vect3" matrices nil)
(vect3 const-decl "Vect3" vect3D nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sigma def-decl "real" sigma "reals/")
(* const-decl "real" vectors nil)
(* const-decl "Mat3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(* const-decl "Vect3" matrices nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(associativity_3 0
(associativity_3-1 nil 3254652082 ("" (grind) nil nil)
((col const-decl "Vect3" matrices nil)
(vect3 const-decl "Vect3" vect3D nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sigma def-decl "real" sigma "reals/")
(* const-decl "real" vectors nil)
(* const-decl "Vect3" matrices nil)
(row const-decl "Vect3" matrices nil)
(* const-decl "Mat3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(distribution_minus 0
(distribution_minus-1 nil 3254652082
("" (grind)
(("" (decompose-equality 1)
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil)
((Vect3 type-eq-decl nil vect3D nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Mat3 type-eq-decl nil matrices nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "Vect3" matrices nil)
(* const-decl "real" vectors nil)
(sigma def-decl "real" sigma "reals/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(- const-decl "real" vectors nil)
(vect3 const-decl "Vect3" vect3D nil)
(row const-decl "Vect3" matrices nil))
nil))
(distribution_add 0
(distribution_add-1 nil 3254652082
("" (grind)
(("" (decompose-equality 1)
(("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil)
((Vect3 type-eq-decl nil vect3D nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Mat3 type-eq-decl nil matrices nil)
(Vector type-eq-decl nil vectors nil)
(Index type-eq-decl nil vectors nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "Vect3" matrices nil)
(* const-decl "real" vectors nil)
(sigma def-decl "real" sigma "reals/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(+ const-decl "real" vectors nil)
(vect3 const-decl "Vect3" vect3D nil)
(row const-decl "Vect3" matrices nil))
nil))
(mat2_TCC1 0
(mat2_TCC1-1 nil 3254652082 ("" (subtype-tcc) nil nil)
((mat3 const-decl "Mat3" matrices nil)) nil))
(det_mat2 0
(det_mat2-1 nil 3254652082 ("" (grind) nil nil)
((mat2 const-decl "Mat2" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(det const-decl "real" matrices nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(inv_TCC1 0
(inv_TCC1-1 nil 3254652082 ("" (subtype-tcc) nil nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(Mat3 type-eq-decl nil matrices nil)
(singular? const-decl "bool" matrices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(NonSingular type-eq-decl nil matrices nil)
(det const-decl "real" matrices nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(inv_id_TCC1 0
(inv_id_TCC1-1 nil 3254652082 ("" (subtype-tcc) nil nil)
((id const-decl "Mat3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(det const-decl "real" matrices nil)
(singular? const-decl "bool" matrices nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(inv_id 0
(inv_id-1 nil 3254652082 ("" (grind) nil nil)
((id const-decl "Mat3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(det const-decl "real" matrices nil)
(cofactor_ij const-decl "Mat3" matrices nil)
(cofactor const-decl "Mat3" matrices nil)
(T const-decl "Mat3" matrices nil)
(* const-decl "Mat3" matrices nil)
(inv const-decl "Mat3" matrices nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil))
nil))
(inv_left 0
(inv_left-2 nil 3254652189
("" (skeep :preds? t)
(("" (expand "singular?")
(("" (expand "id")
(("" (decompose-equality 2)
(("" (expand "*")
(("" (expand "inv")
(("" (name-replace "D" "det(ns)")
(("" (expand "mat3")
(("" (lift-if)
(("" (split)
(("1" (grind)
(("1" (field 1)
(("1" (hide -1 2)
(("1" (expand "D")
(("1"
(expand "det")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split 2)
(("1" (grind) nil nil)
("2" (flatten)
(("2" (split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1"
(grind)
(("1"
(field 1)
(("1"
(hide -1 3)
(("1"
(expand "D")
(("1"
(expand "det")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1"
(grind)
nil
nil)
("2"
(flatten)
(("2"
(split 2)
(("1"
(grind)
(("1"
(field 1)
(("1"
(hide -1 4)
(("1"
(expand
"D")
(("1"
(expand
"det")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((singular? const-decl "bool" matrices nil)
(Mat3 type-eq-decl nil matrices nil)
(* const-decl "Mat3" matrices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(NonSingular type-eq-decl nil matrices nil)
(inv const-decl "Mat3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(both_sides_times1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(D skolem-const-decl "real" matrices nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(cofactor_ij const-decl "Mat3" matrices nil)
(cofactor const-decl "Mat3" matrices nil)
(T const-decl "Mat3" matrices nil)
(* const-decl "Mat3" matrices nil)
(row const-decl "Vect3" matrices nil)
(col const-decl "Vect3" matrices nil)
(vect3 const-decl "Vect3" vect3D nil)
(sigma def-decl "real" sigma "reals/")
(* const-decl "real" vectors nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(det const-decl "real" matrices nil)
(id const-decl "Mat3" matrices nil))
nil)
(inv_left-1 nil 3254652082
("" (skolem 1 "ns")
(("" (expand "id")
(("" (decompose-equality 1)
(("" (expand "*")
(("" (expand "inv")
(("" (name-replace "D" "det(ns)")
(("" (expand "mat3")
(("" (lift-if)
(("" (split)
(("1" (grind)
(("1" (field 1)
(("1" (expand "D")
(("1" (expand "det") (("1" (propax) nil nil))
nil))
nil)
("2" (typepred "ns")
(("2" (expand "singular?")
(("2" (expand "D") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split 2)
(("1" (grind) nil nil)
("2" (flatten)
(("2" (split 2)
(("1" (grind) nil nil)
("2" (flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1"
(grind)
(("1"
(field 1)
(("1"
(expand "D")
(("1"
(expand "det")
(("1" (propax) nil nil))
nil))
nil)
("2"
(typepred "ns")
(("2"
(expand "singular?")
(("2"
(expand "D")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1"
(grind)
(("1"
(field 1)
(("1"
(expand "D")
(("1"
(expand
"det")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(typepred
"ns")
(("2"
(expand
"singular?")
(("2"
(expand
"D")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil nil))
(inv_right 0
(inv_right-2 nil 3254652310
("" (skeep :preds? t)
(("" (expand "singular?")
(("" (expand "id")
(("" (decompose-equality 2)
(("" (expand "*")
(("" (expand "inv")
(("" (name-replace "D" "det(ns)")
(("" (expand "mat3")
(("" (lift-if)
(("" (split)
(("1" (grind)
(("1" (field 1)
(("1" (hide -1 2)
(("1" (expand "D")
(("1"
(expand "det")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split 2)
(("1" (grind) nil nil)
("2" (flatten)
(("2" (split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1"
(grind)
(("1"
(field 1)
(("1"
(hide -1 3)
(("1"
(expand "D")
(("1"
(expand "det")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1"
(grind)
nil
nil)
("2"
(flatten)
(("2"
(split 2)
(("1"
(grind)
(("1"
(field 1)
(("1"
(hide -1 4)
(("1"
(expand
"D")
(("1"
(expand
"det")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((singular? const-decl "bool" matrices nil)
(Mat3 type-eq-decl nil matrices nil)
(* const-decl "Mat3" matrices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(NonSingular type-eq-decl nil matrices nil)
(inv const-decl "Mat3" matrices nil)
(mat3 const-decl "Mat3" matrices nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(both_sides_times1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(D skolem-const-decl "real" matrices nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(row const-decl "Vect3" matrices nil)
(cofactor_ij const-decl "Mat3" matrices nil)
(cofactor const-decl "Mat3" matrices nil)
(T const-decl "Mat3" matrices nil)
(* const-decl "Mat3" matrices nil)
(col const-decl "Vect3" matrices nil)
(vect3 const-decl "Vect3" vect3D nil)
(sigma def-decl "real" sigma "reals/")
(* const-decl "real" vectors nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(det const-decl "real" matrices nil)
(id const-decl "Mat3" matrices nil))
nil)
(inv_right-1 nil 3254652082
("" (skolem 1 "ns")
(("" (expand "id")
(("" (decompose-equality 1)
(("" (expand "*")
(("" (expand "inv")
(("" (name-replace "D" "det(ns)")
(("" (expand "mat3")
(("" (lift-if)
(("" (split)
(("1" (grind)
(("1" (field 1)
(("1" (expand "D")
(("1" (expand "det") (("1" (propax) nil nil))
nil))
nil)
("2" (typepred "ns")
(("2" (expand "singular?")
(("2" (expand "D") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split 2)
(("1" (grind) nil nil)
("2" (flatten)
(("2" (split 2)
(("1" (grind) nil nil)
("2" (flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1"
(grind)
(("1"
(field 1)
(("1"
(expand "D")
(("1"
(expand "det")
(("1" (propax) nil nil))
nil))
nil)
("2"
(typepred "ns")
(("2"
(expand "singular?")
(("2"
(expand "D")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(split 2)
(("1"
(grind)
(("1"
(field 1)
(("1"
(expand "D")
(("1"
(expand
"det")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(typepred
"ns")
(("2"
(expand
"singular?")
(("2"
(expand
"D")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil nil))
(sol_eqs_correctness 0
(sol_eqs_correctness-1 nil 3254652082
("" (skolem 1 ("A" "B"))
(("" (expand "sol_eqs")
(("" (lemma "associativity_2")
(("" (inst?)
(("" (rewrite "inv_right")
(("" (rewrite "id_left2") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sol_eqs const-decl "Vect3" matrices nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(Mat3 type-eq-decl nil matrices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(singular? const-decl "bool" matrices nil)
(NonSingular type-eq-decl nil matrices nil)
(inv const-decl "Mat3" matrices nil)
(Index type-eq-decl nil vectors nil)
(Vect3 type-eq-decl nil vect3D nil)
(id_left2 formula-decl nil matrices nil)
(inv_right formula-decl nil matrices nil)
(associativity_2 formula-decl nil matrices nil))
nil)))
¤ Dauer der Verarbeitung: 0.81 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.
|
