Relation INLETS

• Defined in theory: Thermal-system
• Source code: thermal-system.ol

Slots on this relation:

Documentation:

the set of inlet streams of the control-volume

Instance-Of: Relation

Arity: 2

Domain: Control-volume

Range: 2d-stream

Other Related Axioms:

(Forall 
    (?Self ?Time)
    (=> (Active ?Time Control-Volume ?Self)
        (And (Forall 
                 (?X)
                 (=> (Inlets ?Self ?X)
                     (And (C+ (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Pe-Rate ?X) ?T)))
                              (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Pe-Rate-In ?Self)
                                                    ?T))))
                          (C+ (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Ke-Rate ?X) ?T)))
                              (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Ke-Rate-In ?Self)
                                                    ?T))))
                          (C+ (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Enthalpy-Rate ?X)
                                                    ?T)))
                              (Lambda 
                                  (?T)
                                  (If (= ?T ?Time)
                                      (Value-At (Enthalpy-Rate-In ?Self)
                                                ?T))))
                          (C+ (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Mass-Rate ?X)
                                                    ?T)))
                              (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Mass-Rate-In ?Self)
                                                    ?T))))
                          (C+ (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Entropy-Rate ?X)
                                                    ?T)))
                              (Lambda 
                                  (?T)
                                  (If (= ?T ?Time)
                                      (Value-At (Entropy-Rate-In ?Self)
                                                ?T)))))))
             (Forall 
                 (?X)
                 (=> (Outlets ?Self ?X)
                     (And (C+ (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Pe-Rate ?X) ?T)))
                              (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Pe-Rate-Out ?Self)
                                                    ?T))))
                          (C+ (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Ke-Rate ?X) ?T)))
                              (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Ke-Rate-Out ?Self)
                                                    ?T))))
                          (C+ (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Enthalpy-Rate ?X)
                                                    ?T)))
                              (Lambda 
                                  (?T)
                                  (If (= ?T ?Time)
                                      (Value-At 
                                          (Enthalpy-Rate-Out ?Self)
                                          ?T))))
                          (C+ (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Mass-Rate ?X)
                                                    ?T)))
                              (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At 
                                              (Mass-Rate-Out ?Self)
                                              ?T))))
                          (C+ (Lambda (?T)
                                      (If (= ?T ?Time)
                                          (Value-At (Entropy-Rate ?X)
                                                    ?T)))
                              (Lambda 
                                  (?T)
                                  (If (= ?T ?Time)
                                      (Value-At (Entropy-Rate-Out ?Self)
                                                ?T)))))))
             (= (Lambda (?T)
                        (If (= ?T ?Time)
                            (Value-At (D-Entropy-Rate ?Self) ?T)))
                (- (Lambda (?T)
                           (If (= ?T ?Time)
                               (Value-At (Entropy-Rate-In ?Self) ?T)))
                   (Lambda (?T)
                           (If (= ?T ?Time)
                               (Value-At (Entropy-Rate-Out ?Self) ?T)))))
             (= (Lambda (?T)
                        (If (= ?T ?Time)
                            (Value-At (D-Pe-Rate ?Self) ?T)))
                (- (Lambda (?T)
                           (If (= ?T ?Time)
                               (Value-At (Pe-Rate-Out ?Self) ?T)))
                   (Lambda (?T)
                           (If (= ?T ?Time)
                               (Value-At (Pe-Rate-In ?Self) ?T)))))
             (= (Lambda (?T)
                        (If (= ?T ?Time)
                            (Value-At (D-Ke-Rate ?Self) ?T)))
                (- (Lambda (?T)
                           (If (= ?T ?Time)
                               (Value-At (Ke-Rate-Out ?Self) ?T)))
                   (Lambda (?T)
                           (If (= ?T ?Time)
                               (Value-At (Ke-Rate-In ?Self) ?T))))))))

(=> (Inlets $X $Y) (2d-Stream $Y))

(=> (Inlets $X $Y) (Control-Volume $X))

(Forall 
    (?Self ?Time)
    (=> (Active ?Time
                Control-Volume-Inlet-Stream-Ideal-Gas-Law
                ?Self)
        (Forall 
            (?X)
            (=> (Inlets (Cv-Involved ?Self) ?X)
                (= (* (Lambda (?T)
                              (If (= ?T ?Time)
                                  (Value-At (Stream-Pressure ?X) ?T)))
                      (Lambda (?T)
                              (If (= ?T ?Time)
                                  (Value-At (Specific-Volume ?X) ?T))))
                   (* (Lambda 
                          (?T)
                          (If (= ?T ?Time)
                              (Value-At 
                                  (Ideal-Gas-Constant 
                                      (Substance-In (Cv-Involved ?Self)))
                                  ?T)))
                      (Lambda (?T)
                              (If (= ?T ?Time)
                                  (Value-At (Stream-Temperature ?X)
                                            ?T)))))))))

(Forall 
    (?Self ?Time)
    (=> (Active ?Time
                Control-Volume-Inlet-Stream-Thermodynamic-State
                ?Self)
        (Forall 
            (?X)
            (=> (Inlets (Cv-Involved ?Self) ?X)
                (= (Lambda (?T)
                           (If (= ?T ?Time)
                               (Value-At (Specific-Enthalpy ?X) ?T)))
                   (Compute-Air-Thermodynamic-State 
                       (Lambda (?T)
                               (If (= ?T ?Time)
                                   (Value-At (Stream-Temperature ?X)
                                             ?T)))))))))