the class of model fragments about a contol-volume
(Forall (?Cv-Involved) (<=> (Control-Volume ?Cv-Involved) (Exists (?Self) (And (Control-Volume-Op-Mode ?Self) (= (Cv-Involved ?Self) ?Cv-Involved))))) (Forall (?Self ?Time) (<=> (Active ?Time Control-Volume-Op-Mode ?Self) (Control-Volume-Op-Mode ?Self)))
(Forall (?Self) (<=> (Cycle-Heat-Input ?Self) (And (Thermal-Process-Op-Mode ?Self) (Thermal-Cycle-Op-Mode ?Self) (Control-Volume-Op-Mode ?Self) (Thermal-Component-Op-Mode ?Self) (Process-Cv Process-Involved Cv-Involved) (Component-Cv Component-Involved Cv-Involved) (Connected-To-External-Heat-Source-P Component-Involved True)))) (Forall (?Self ?Time) (<=> (Active ?Time Cycle-Heat-Input ?Self) (And (Cycle-Heat-Input ?Self) (Active ?Time Thermal-Process-Op-Mode ?Self) (Active ?Time Thermal-Cycle-Op-Mode ?Self) (Active ?Time Control-Volume-Op-Mode ?Self) (Active ?Time Thermal-Component-Op-Mode ?Self)))) (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) (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)))) (Forall (?Cv-Involved) (<=> (Control-Volume ?Cv-Involved) (Exists (?Self) (And (Control-Volume-Op-Mode ?Self) (= (Cv-Involved ?Self) ?Cv-Involved))))) (Forall (?Self ?Time) (<=> (Active ?Time Control-Volume-Op-Mode ?Self) (Control-Volume-Op-Mode ?Self))) (Participant-Function-Of Cv-Involved Control-Volume-Op-Mode) (Forall (?Self) (<=> (Control-Volume-Inlet-Stream-Ideal-Gas-Law ?Self) (And (Control-Volume-Op-Mode ?Self) (Ideal-Gas-P (Substance-In Cv-Involved) true)))) (Forall (?Self ?Time) (<=> (Active ?Time Control-Volume-Inlet-Stream-Ideal-Gas-Law ?Self) (And (Control-Volume-Inlet-Stream-Ideal-Gas-Law ?Self) (Active ?Time Control-Volume-Op-Mode ?Self)))) (Forall (?Self) (<=> (Control-Volume-Outlet-Stream-Ideal-Gas-Law ?Self) (And (Control-Volume-Op-Mode ?Self) (Ideal-Gas-P (Substance-In Cv-Involved) true)))) (Forall (?Self ?Time) (<=> (Active ?Time Control-Volume-Outlet-Stream-Ideal-Gas-Law ?Self) (And (Control-Volume-Outlet-Stream-Ideal-Gas-Law ?Self) (Active ?Time Control-Volume-Op-Mode ?Self)))) (Forall (?Self) (<=> (Control-Volume-Inlet-Stream-Thermodynamic-State ?Self) (And (Air-Operating-Mode ?Self) (Control-Volume-Op-Mode ?Self) (Substance-In (Cv-Involved ?Self) (Air-Involved ?Self))))) (Forall (?Self ?Time) (<=> (Active ?Time Control-Volume-Inlet-Stream-Thermodynamic-State ?Self) (And (Control-Volume-Inlet-Stream-Thermodynamic-State ?Self) (Active ?Time Air-Operating-Mode ?Self) (Active ?Time Control-Volume-Op-Mode ?Self)))) (Forall (?Self) (<=> (Control-Volume-Outlet-Stream-Thermodynamic-State ?Self) (And (Air-Operating-Mode ?Self) (Control-Volume-Op-Mode ?Self) (Substance-In (Cv-Involved ?Self) (Air-Involved ?Self))))) (Forall (?Self ?Time) (<=> (Active ?Time Control-Volume-Outlet-Stream-Thermodynamic-State ?Self) (And (Control-Volume-Outlet-Stream-Thermodynamic-State ?Self) (Active ?Time Air-Operating-Mode ?Self) (Active ?Time Control-Volume-Op-Mode ?Self)))) (Forall (?Self) (<=> (Control-Volume-Negligible-Pe-Change ?Self) (And (Control-Volume-Op-Mode ?Self) (Even-Pe Cv-Involved true)))) (Forall (?Self ?Time) (<=> (Active ?Time Control-Volume-Negligible-Pe-Change ?Self) (And (Control-Volume-Negligible-Pe-Change ?Self) (Active ?Time Control-Volume-Op-Mode ?Self)))) (Forall (?Self) (<=> (Control-Volume-Negligible-Ke-Change ?Self) (And (Control-Volume-Op-Mode ?Self) (Even-Ke Cv-Involved true)))) (Forall (?Self ?Time) (<=> (Active ?Time Control-Volume-Negligible-Ke-Change ?Self) (And (Control-Volume-Negligible-Ke-Change ?Self) (Active ?Time Control-Volume-Op-Mode ?Self))))