a one-input one-output turbine
(Forall (?Self ?Time)
(<=> (Active ?Time Simple-Turbine ?Self)
(And (Simple-Turbine ?Self)
(Active ?Time Turbine ?Self)
(Active ?Time 1-1-Port-Thermal-Component ?Self))))