Function COLUMN


Slots on this function:

Documentation:
Function that returns the i-th column of a given matrix
Arity: 3

Axioms:

(Nth-Domain Column 3 Column-Matrix)

(Nth-Domain Column 2 Positive-Integer)

(Nth-Domain Column 1 Matrix)

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