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

Instance-Of: Function

Arity: 3

Equivalence Axioms:

(<=> (Matrix-Less-Column ?A ?I)
     (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))))))))

Axioms:

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

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

Other Related Axioms:

(=> (= (Matrix-Less-Row-And-Column ?A ?I ?J) ?B)
    (= ?B (Matrix-Less-Row (Matrix-Less-Column ?A ?J) ?I)))

(=> (= (Matrix-Less-Column ?A ?I) ?B)
    (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)))))))

(=> (= (Matrix-Less-Column ?A ?I) ?B)
    (= (Column-Dimension ?B) (- (Column-Dimension ?A) 1)))

(=> (= (Matrix-Less-Column ?A ?I) ?B)
    (= (Row-Dimension ?B) (Row-Dimension ?A)))

(=> (= (Matrix-Less-Column ?A ?I) ?B) (Matrix ?B))

(=> (= (Matrix-Less-Column ?A ?I) ?B) (Defined (Column ?A ?I)))

(=> (= (Matrix-Less-Column ?A ?I) ?B) (Matrix ?A))