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

Instance-Of: Function

Arity: 3

Equivalence Axioms:

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

Axioms:

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

(Nth-Domain Matrix-Less-Row 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-Row ?A ?I) ?B)
    (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))))))

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

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

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

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

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