Function that returns the spatial dimension associated with a tensor.
(Inherited-Facet-Value Slot-Value-Type
Tensor-Quantity
Spatial.Dimension
Non-Negative-Integer)
(Inherited-Facet-Value Slot-Cardinality
Tensor-Quantity
Spatial.Dimension
1)
(=> (Tensor-Quantity ?T)
(And (Value-Cardinality ?T Tensor-Order 1)
(Value-Type ?T Tensor-Order Non-Negative-Integer)
(Value-Cardinality ?T Tensor-Order 1)
(Value-Cardinality ?T Spatial.Dimension 1)
(Value-Type ?T Spatial.Dimension Non-Negative-Integer)
(Value-Cardinality ?T Spatial.Dimension 1)))
(=> (Spatial.Dimension $X $Y) (Positive-Integer $Y))
(=> (Spatial.Dimension $X $Y) (Tensor-Quantity $X))
(Forall (?B ?I)
(=> (And (Orthonormal-Basis ?B)
(= (Basis.Dimension ?B) (Spatial.Dimension ?V))
(Positive-Integer ?I)
(=< ?I (Spatial.Dimension ?V)))
(And (Defined (Vector-Component ?V ?I ?B))
(= (Quantity.Dimension (Vector-Component ?V ?I ?B))
(Quantity.Dimension ?V)))))
(<=> (Vector-Quantity ?V)
(And (Constant-Quantity ?V)
(Tensor-Quantity ?V)
(= (Tensor-Order ?V) 1)
(Forall (?B ?I)
(=> (And (Orthonormal-Basis ?B)
(= (Basis.Dimension ?B)
(Spatial.Dimension ?V))
(Positive-Integer ?I)
(=< ?I (Spatial.Dimension ?V)))
(And (Defined (Vector-Component ?V ?I ?B))
(= (Quantity.Dimension (Vector-Component ?V
?I
?B))
(Quantity.Dimension ?V)))))
(Forall (?U)
(=> (And (Unit-Of-Measure ?U)
(= (Quantity.Dimension ?U)
(Quantity.Dimension ?V)))
(Numeric-Tensor (Magnitude ?V ?U))))))
(Forall (?B ?I ?J)
(=> (And (Orthonormal-Basis ?B)
(= (Basis.Dimension ?B) (Spatial.Dimension ?D))
(Positive-Integer ?I)
(=< ?I (Spatial.Dimension ?D))
(Positive-Integer ?J)
(=< ?J (Spatial.Dimension ?D)))
(And (Defined (Dyad-Component ?D ?I ?J ?B))
(= (Quantity.Dimension (Dyad-Component ?D ?I ?J ?B))
(Quantity.Dimension ?D)))))
(<=> (Dyad ?D)
(And (Constant-Quantity ?D)
(Tensor-Quantity ?D)
(= (Tensor-Order ?D) 2)
(Forall (?B ?I ?J)
(=> (And (Orthonormal-Basis ?B)
(= (Basis.Dimension ?B)
(Spatial.Dimension ?D))
(Positive-Integer ?I)
(=< ?I (Spatial.Dimension ?D))
(Positive-Integer ?J)
(=< ?J (Spatial.Dimension ?D)))
(And (Defined (Dyad-Component ?D ?I ?J ?B))
(= (Quantity.Dimension (Dyad-Component ?D
?I
?J
?B))
(Quantity.Dimension ?D)))))
(Forall (?U)
(=> (And (Unit-Of-Measure ?U)
(= (Quantity.Dimension ?U)
(Quantity.Dimension ?D)))
(Numeric-Tensor (Magnitude ?D ?U))))))
(=> (= (Tensor-To-Matrix ?T ?Basis) ?M)
(=> (= (Tensor-Order ?T) 2)
(Square-Matrix ?M)
(= (Size ?M) (Spatial.Dimension ?T))
(Forall (?I ?J)
(= (Value ?M ?I ?J) (Dyad-Component ?T ?I ?J ?Basis)))))
(=> (= (Tensor-To-Matrix ?T ?Basis) ?M)
(=> (= (Tensor-Order ?T) 1)
(= (Row-Dimension ?M) 1)
(= (Column-Dimension ?M) (Spatial.Dimension ?T))
(Forall (?I)
(= (Value ?M 1 ?I) (Vector-Component ?T ?I ?Basis)))))
(=> (= (Vector-Component ?V ?I ?B) ?S)
(=< ?I (Spatial.Dimension ?V)))
(=> (= (Vector-Component ?V ?I ?B) ?S)
(= (Spatial.Dimension ?V) (Basis.Dimension ?B)))
(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S)
(=< ?J (Spatial.Dimension ?T)))
(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S)
(=< ?I (Spatial.Dimension ?T)))
(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S)
(= (Spatial.Dimension ?T) (Basis.Dimension ?B)))
(=> (= (The-Vector-Quantity ?M ?B) ?V)
(= ?V
(Summation (Lambda (?J) (* (Value ?M 1 ?J) (Basis.Vec ?B ?J)))
1
(Spatial.Dimension ?V))))
(=> (= (The-Vector-Quantity ?M ?B) ?V)
(= (Spatial.Dimension ?V) (Column-Dimension ?M)))
(=> (= (The-Dyad ?M ?B) ?T)
(= ?T
(Summation (Lambda (?I)
(Summation (Lambda (?J)
(* (Basis.Vec ?B ?I)
(* (Value ?M ?I ?J)
(Basis.Vec ?B ?J))))
1
(Spatial.Dimension ?T)))
1
(Spatial.Dimension ?T))))
(=> (= (The-Dyad ?M ?B) ?T) (= (Spatial.Dimension ?T) (Size ?M)))
(=> (And (Dyad ?X) (Dyad ?Y))
(=> (+ ?X ?Y ?Z)
(And (Dyad ?Z)
(Forall (?B ?I ?J)
(=> (And (Orthonormal-Basis ?B)
(= (Spatial.Dimension ?X)
(Basis.Dimension ?B))
(Positive-Integer ?I)
(Positive-Integer ?J)
(=< ?I (Spatial.Dimension ?X))
(=< ?J (Spatial.Dimension ?X)))
(= (Dyad-Component ?Z ?I ?J ?B)
(+ (Dyad-Component ?X ?I ?J ?B)
(Dyad-Component ?Y ?I ?J ?B))))))))
(=> (And (Vector-Quantity ?X) (Vector-Quantity ?Y))
(=> (+ ?X ?Y ?Z)
(And (Vector-Quantity ?Z)
(Forall (?B ?I)
(=> (And (Orthonormal-Basis ?B)
(= (Spatial.Dimension ?X)
(Basis.Dimension ?B))
(Positive-Integer ?I)
(=< ?I (Spatial.Dimension ?X)))
(= (Vector-Component ?Z ?I ?B)
(+ (Vector-Component ?X ?I ?B)
(Vector-Component ?Y ?I ?B))))))))
(=> (And (Tensor-Quantity ?X) (Tensor-Quantity ?Y) (+ ?X ?Y ?Z))
(And (Tensor-Quantity ?Z)
(= (Spatial.Dimension ?X) (Spatial.Dimension ?Y))
(= (Spatial.Dimension ?X) (Spatial.Dimension ?Z))))
(=> (And (Vector-Quantity ?X) (- ?X ?Y))
(And (Vector-Quantity ?Y)
(= (+ ?X ?Y)
(The-Zero-Vector-Of-Type (Quantity.Dimension ?X)
(Spatial.Dimension ?X)))))
(=> (And (Vector-Quantity ?V1) (Dyad ?T1))
(<=> (Dot ?V1 ?T1 ?V)
(And (Vector-Quantity ?V)
(Forall (?B)
(= ?T
(The-Vector-Quantity (* (Tensor-To-Matrix ?V1
?B)
(Tensor-To-Matrix ?T1
?B))
?B)))
(Forall
(?B ?I ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?V1))
(= ?T
(Summation
(Lambda
(?I)
(* (Basis.Vec ?B ?I)
(Summation
(Lambda (?J)
(* (Vector-Component
?V1
?J
?B)
(Dyad-Component ?T1
?J
?I
?B)))
1
(Spatial.Dimension ?V1))))
1
(Spatial.Dimension ?V1))))))))
(=> (And (Dyad ?T1) (Vector-Quantity ?V1))
(<=> (Dot ?T1 ?V1 ?V)
(And (Vector-Quantity ?V)
(Forall
(?B)
(= ?T
(The-Vector-Quantity
(Transpose (* (Tensor-To-Matrix ?T1 ?B)
(Transpose (Tensor-To-Matrix
?V1
?B))))
?B)))
(Forall
(?B ?I ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?V1))
(= ?T
(Summation
(Lambda
(?I)
(* (Basis.Vec ?B ?I)
(Summation
(Lambda (?J)
(* (Dyad-Component ?T1
?I
?J
?B)
(Vector-Component
?V1
?J
?B)))
1
(Spatial.Dimension ?V1))))
1
(Spatial.Dimension ?V1))))))))
(=> (And (Dyad ?T1) (Dyad ?T2))
(<=> (Dot ?T1 ?T2 ?T)
(And (Dyad ?T)
(Forall (?B)
(= ?T
(The-Dyad (* (Tensor-To-Matrix ?T1 ?B)
(Tensor-To-Matrix ?T2 ?B))
?B)))
(Forall
(?B ?I ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?T1))
(= ?T
(Summation
(Lambda
(?I)
(Summation
(Lambda (?J)
(* (* (Basis.Vec ?B ?I)
(Basis.Vec ?B ?J))
(* (Dyad-Component ?T1
?I
?J
?B)
(Dyad-Component ?T2
?J
?I
?B))))
1
(Spatial.Dimension ?T1)))
1
(Spatial.Dimension ?T1))))))))
(=> (And (Vector-Quantity ?V1) (Vector-Quantity ?V2))
(<=> (Dot ?V1 ?V2 ?S)
(And (Scalar-Quantity ?S)
(Forall (?B)
(= ?S
(Value (* (Tensor-To-Matrix ?V1 ?B)
(Transpose (Tensor-To-Matrix ?V2
?B)))
11)))
(Forall (?B ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?V1))
(= ?S
(Summation (Lambda (?J)
(* (Vector-Component
?V1
?J
?B)
(Vector-Component
?V2
?J
?B)))
1
(Spatial.Dimension ?V1))))))))
(=> (= (Dot ?T1 ?T2) ?T)
(= (Spatial.Dimension ?T1) (Spatial.Dimension ?T2)))
(=> (And (Scalar-Quantity ?S) (Vector-Quantity ?V1) (* ?S ?V1 ?V))
(And (Vector-Quantity ?V)
(= (Spatial.Dimension ?V1) (Spatial.Dimension ?V))
(Forall (?B ?I)
(=> (= (Basis.Dimension ?B) (Spatial.Dimension ?V1))
(= (Vector-Component ?V ?I ?B)
(* ?S (Vector-Component ?V1 ?I ?B)))))))
(<- (Vector-Quantities-Of-Dimensions ?Physim ?Spatdim)
(If (And (Physical-Dimension ?Physim)
(Positive-Integer ?Spatdim))
(Kappa (?Vq)
(And (Vector-Quantity ?Vq)
(= (Spatial.Dimension ?Vq) ?Spatdim)
(= (Quantity.Dimension ?Vq) ?Physim)))))
(<- (Dyad-Of-Dimensions ?Physim ?Spatdim)
(If (And (Physical-Dimension ?Physim)
(Positive-Integer ?Spatdim))
(Kappa (?Vq)
(And (Dyad ?Vq)
(= (Spatial.Dimension ?Vq) ?Spatdim)
(= (Quantity.Dimension ?Vq) ?Physim)))))