Function MATRIX-LESS-ROW

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

Slots on this function:

Documentation:

Function that returns the matrix with a row deleted

Arity: 3

Axioms:

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

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

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