Function MATRIX-LESS-COLUMN

• Defined in theory: Basic-matrix-algebra
• Source code: basic-matrix.lisp

Slots on this function:

Documentation:

Function that returns the matrix with a column deleted

Arity: 3

Axioms:

(Nth-Domain Matrix-Less-Column 3 Matrix)

(Nth-Domain Matrix-Less-Column 1 Matrix)

(<=> (Matrix-Less-Column ?A ?I ?B)
     (And (Matrix ?A)
          (Defined (Column ?A ?I))
          (Matrix ?B)
          (= (Row-Dimension ?B) (Row-Dimension ?A))
          (= (Column-Dimension ?B) (- (Column-Dimension ?A) 1))
          (Forall (?K ?L)
                  (=> (Defined (Value ?B ?K ?L))
                      (=> (< ?L ?I)
                          (= (Value ?B ?K ?L) (Value ?A ?K ?L)))
                      (=> (>= ?L ?I)
                          (= (Value ?B ?K ?L) (Value ?A ?K (+ ?L 1))))))))