(Forall (?Self)
(<=> (Cycle-Work-Output ?Self)
(And (Thermal-Process-Op-Mode ?Self)
(Thermal-Cycle-Op-Mode ?Self)
(Control-Volume-Op-Mode ?Self)
(Process-Cv Process-Involved Cv-Involved))))
(Forall
(?Self ?Time)
(=> (Active ?Time Cycle-Work-Output ?Self)
(C+ (Lambda (?T)
(If (= ?T ?Time)
(Value-At (Work-Rate (Process-Involved ?Self))
?T)))
(Lambda
(?T)
(If (= ?T ?Time)
(Value-At
(Net-Work-Output-Rate (Cycle-Involved ?Self))
?T))))))
(Forall (?Self ?Time)
(<=> (Active ?Time Cycle-Work-Output ?Self)
(And (Cycle-Work-Output ?Self)
(Active ?Time Thermal-Process-Op-Mode ?Self)
(Active ?Time Thermal-Cycle-Op-Mode ?Self)
(Active ?Time Control-Volume-Op-Mode ?Self))))