(Forall (?Self ?Time)
(=> (Active ?Time Positive-Displacement-Component ?Self)
(= (Lambda (?T)
(If (= ?T ?Time)
(Value-At (Compression-Ratio ?Self) ?T)))
(/ (Lambda (?T)
(If (= ?T ?Time)
(Value-At (Displacement ?Self) ?T)))
(Lambda (?T)
(If (= ?T ?Time)
(Value-At (Clearance-Volume ?Self) ?T)))))))
(Forall (?Self ?Time)
(<=> (Active ?Time Positive-Displacement-Component ?Self)
(And (Positive-Displacement-Component ?Self)
(Active ?Time Thermal-Component ?Self))))
(=> (Positive-Displacement-Component ?Self)
(And (Quantity.Dimension (Displacement ?Self) Volume-Dimension)
(Quantity.Dimension (Speed ?Self) Frequency-Dimension)
(Quantity.Dimension (Cycles-Rate ?Self) Frequency-Dimension)
(Quantity.Dimension (Mean-Effective-Pressure ?Self)
Pressure-Dimension)
(Quantity.Dimension (Volumetric-Efficiency ?Self)
Dimensionless)
(Quantity.Dimension (Clearance-Volume ?Self) Dimensionless)
(Quantity.Dimension (Compression-Ratio ?Self) Dimensionless)))