the system consisting of a boiler, a simple turbine, a condenser, and a pump
the boiler subsystem of power-system-eight-one power cycle
the condensor subsystem of the power-system-eight-one power cycle
the pump subsystem of the power-system-eight-one power cycle
the turbine subsystem of power-system-eight-one power cycle
the boiler subsystem of power-system-eight-one power cycle
the condensor subsystem of the power-system-eight-one power cycle
the pump subsystem of the power-system-eight-one power cycle
the turbine subsystem of power-system-eight-one power cycle
(Connected-Terminals (Pmp-Blr-Junction ?Self) (Inlet-Stream (Blr-Cv (Blr-System ?Self)))) (Connected-Terminals (Pmp-Blr-Junction ?Self) (Outlet-Stream (Pmp-Cv (Pmp-System ?Self)))) (Connected-Terminals (Cnd-Pmp-Junction ?Self) (Inlet-Stream (Pmp-Cv (Pmp-System ?Self)))) (Connected-Terminals (Cnd-Pmp-Junction ?Self) (Outlet-Stream (Hf-Cv (Cdnsr-System ?Self)))) (Connected-Terminals (Tbn-Cnd-Junction ?Self) (Inlet-Stream (Hf-Cv (Cdnsr-System ?Self)))) (Connected-Terminals (Tbn-Cnd-Junction ?Self) (Outlet-Stream (Tbn-Cv (Tbn-System ?Self)))) (Connected-Terminals (Blr-Tbn-Junction ?Self) (Inlet-Stream (Tbn-Cv (Tbn-System ?Self)))) (Connected-Terminals (Blr-Tbn-Junction ?Self) (Outlet-Stream (Blr-Cv (Blr-System ?Self)))) (Forall (?Self ?Time) (=> (Active ?Time Power-System-Eight-One ?Self) (And (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Thermal-Efficiency ?Self) ?T))) (/ (- (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Blr-Cv (Blr-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Tbn-Cv (Tbn-System ?Self)))) ?T)))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Pmp-Cv (Pmp-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Hf-Cv (Cdnsr-System ?Self)))) ?T))))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Blr-Cv (Blr-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Pmp-Cv (Pmp-System ?Self)))) ?T)))))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Back-Work-Ratio ?Self) ?T))) (/ (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Pmp-Cv (Pmp-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Hf-Cv (Cdnsr-System ?Self)))) ?T)))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Blr-Cv (Blr-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Tbn-Cv (Tbn-System ?Self)))) ?T)))))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Heat-Rate (Htfr-Prcs (Blr-System ?Self))) ?T))) (* (Lambda (?T) (If (= ?T ?Time) (Value-At (Mass-Rate-In (Blr-Cv (Blr-System ?Self))) ?T))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Blr-Cv (Blr-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Pmp-Cv (Pmp-System ?Self)))) ?T)))) (/ 1 3600000))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Cycle-Mass-Rate ?Self) ?T))) (* 3.6 (/ (Lambda (?T) (If (= ?T ?Time) (Value-At (Net-Work-Output-Rate ?Self) ?T))) (- (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Blr-Cv (Blr-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Tbn-Cv (Tbn-System ?Self)))) ?T)))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Pmp-Cv (Pmp-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Hf-Cv (Cdnsr-System ?Self)))) ?T)))))))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Cycle-Mass-Rate ?Self) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Mass-Rate-In (Blr-Cv (Blr-System ?Self))) ?T)))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Cycle-Mass-Rate ?Self) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Mass-Rate-In (Tbn-Cv (Tbn-System ?Self))) ?T)))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Condensor-Heat-Out-Rate (Cdnsr-System ?Self)) ?T))) (* (Lambda (?T) (If (= ?T ?Time) (Value-At (Cycle-Mass-Rate (Hf-Cv (Cdnsr-System ?Self))) ?T))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Tbn-Cv (Tbn-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Hf-Cv (Cdnsr-System ?Self)))) ?T))))))))) (Forall (?Self ?Time) (<=> (Active ?Time Power-System-Eight-One ?Self) (And (Power-System-Eight-One ?Self) (Active ?Time Thermal-Cycle ?Self))))
(Forall (?Self ?Time) (=> (Active ?Time Power-System-Eight-One ?Self) (And (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Thermal-Efficiency ?Self) ?T))) (/ (- (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Blr-Cv (Blr-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Tbn-Cv (Tbn-System ?Self)))) ?T)))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Pmp-Cv (Pmp-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Hf-Cv (Cdnsr-System ?Self)))) ?T))))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Blr-Cv (Blr-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Pmp-Cv (Pmp-System ?Self)))) ?T)))))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Back-Work-Ratio ?Self) ?T))) (/ (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Pmp-Cv (Pmp-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Hf-Cv (Cdnsr-System ?Self)))) ?T)))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Blr-Cv (Blr-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Tbn-Cv (Tbn-System ?Self)))) ?T)))))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Heat-Rate (Htfr-Prcs (Blr-System ?Self))) ?T))) (* (Lambda (?T) (If (= ?T ?Time) (Value-At (Mass-Rate-In (Blr-Cv (Blr-System ?Self))) ?T))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Blr-Cv (Blr-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Pmp-Cv (Pmp-System ?Self)))) ?T)))) (/ 1 3600000))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Cycle-Mass-Rate ?Self) ?T))) (* 3.6 (/ (Lambda (?T) (If (= ?T ?Time) (Value-At (Net-Work-Output-Rate ?Self) ?T))) (- (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Blr-Cv (Blr-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Tbn-Cv (Tbn-System ?Self)))) ?T)))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Pmp-Cv (Pmp-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Hf-Cv (Cdnsr-System ?Self)))) ?T)))))))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Cycle-Mass-Rate ?Self) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Mass-Rate-In (Blr-Cv (Blr-System ?Self))) ?T)))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Cycle-Mass-Rate ?Self) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Mass-Rate-In (Tbn-Cv (Tbn-System ?Self))) ?T)))) (= (Lambda (?T) (If (= ?T ?Time) (Value-At (Condensor-Heat-Out-Rate (Cdnsr-System ?Self)) ?T))) (* (Lambda (?T) (If (= ?T ?Time) (Value-At (Cycle-Mass-Rate (Hf-Cv (Cdnsr-System ?Self))) ?T))) (- (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Tbn-Cv (Tbn-System ?Self)))) ?T))) (Lambda (?T) (If (= ?T ?Time) (Value-At (Specific-Enthalpy (Outlet-Stream (Hf-Cv (Cdnsr-System ?Self)))) ?T))))))))) (Forall (?Self ?Time) (<=> (Active ?Time Power-System-Eight-One ?Self) (And (Power-System-Eight-One ?Self) (Active ?Time Thermal-Cycle ?Self)))) (Attribute-Function-Of Blr-System Power-System-Eight-One) (Attribute-Function-Of Tbn-System Power-System-Eight-One) (Attribute-Function-Of Cdnsr-System Power-System-Eight-One) (Attribute-Function-Of Pmp-System Power-System-Eight-One) (Attribute-Function-Of Cnd-Pmp-Junction Power-System-Eight-One) (Attribute-Function-Of Blr-Tbn-Junction Power-System-Eight-One) (Attribute-Function-Of Tbn-Cnd-Junction Power-System-Eight-One) (Attribute-Function-Of Pmp-Blr-Junction Power-System-Eight-One) (Attribute-Function-Of Working-Fluid-In-Cycle Power-System-Eight-One)