Function ROW

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

Slots on this function:

Documentation:

Function that returns the i-th row of a given matrix

Instance-Of: Function

Arity: 3

Equivalence Axioms:

(<=> (Row ?M ?I)
     (And (Matrix ?M)
          (Positive-Integer ?I)
          (=< ?I (Row-Dimension ?M))
          (Row-Matrix ?L)
          (= (Column-Dimension ?M) (Column-Dimension ?L))
          (Forall (?J) (= (Value ?M ?I ?J) (Value ?L 1 ?J)))))

Axioms:

(Nth-Domain Row 3 Row-Matrix)

(Nth-Domain Row 2 Positive-Integer)

(Nth-Domain Row 1 Matrix)

Other Related Axioms:

(=> (= (Matrix-Of-Rows @Elements) ?M)
    (= (Row ?I ?M) (Nth (Listof @Elements) ?I)))

(=> (= (Row ?M ?I) ?L)
    (Forall (?J) (= (Value ?M ?I ?J) (Value ?L 1 ?J))))

(=> (= (Row ?M ?I) ?L)
    (= (Column-Dimension ?M) (Column-Dimension ?L)))

(=> (= (Row ?M ?I) ?L) (Row-Matrix ?L))

(=> (= (Row ?M ?I) ?L) (=< ?I (Row-Dimension ?M)))

(=> (= (Row ?M ?I) ?L) (Positive-Integer ?I))

(=> (= (Row ?M ?I) ?L) (Matrix ?M))

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

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