CompositeNDP
│ provides endurance SB(≥0) s │ requires total_cost {100 $}
│ provides extra_payload SB(≥0) kg │ requires total_mass SB(≥0) kg
│ provides extra_power SB(≥0) W │
│ 12 nodes, 13 edges
│ connected rec: ✓
│ provided endurance ≤ endurance provided by _prod equiv id
│ provided extra_payload ≤ extra_payload provided by _sum1 equiv id
│ provided extra_power ≤ extra_power provided by _sum equiv id
│ _res2 required by _mult ≤ lift provided by actuation diff (always satisfied)
│ _res required by _prod ≤ capacity provided by battery equiv id
│ _result required by _sum ≤ total_power provided by _prod equiv id
│ _result2 required by _sum1 ≤ _op provided by _mult equiv id
│ _result2 required by _sum1 ≤ required total_mass equiv id
│ _result3 required by _sum2 ≤ required total_cost equiv id
│ cost required by actuation ≤ actuation_cost provided by _sum2 equiv (always satisfied)
│ power required by actuation ≤ power provided by _sum equiv (always satisfied)
│ cost required by battery ≤ battery_cost provided by _sum2 equiv (always satisfied)
│ mass required by battery ≤ mass provided by _sum1 equiv id
├ _mult: SimpleWrap
│ │ provides _op SB(≥0) kg │ requires _res2 SB(≥0) N
│ └ DP_L_UME SB(≥0) kg ⇸ SB(≥0) N
│ 𝒇 ⋅ 9.81 ≤ 𝒓
│ M_C_WrapUnits kg → N > M_A_Mult1_Upper SB(≥0) → same x ⟼ x ⋅ 9.81
├ _prod: SimpleWrap
│ │ provides endurance SB(≥0) s │ requires _res SB(≥0) J
│ │ provides total_power SB(≥0) W │
│ └ M_Res_MultiplyMany_DP SB(≥0)×SB(≥0) ⟨s,W⟩ ⇸ SB(≥0) J
│ 𝒇₁⋅𝒇₂ ≤ 𝒓
│ ├ Fs: ├ SB(≥0) s
│ │ └ SB(≥0) W
│ └ algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT
├ _sum: SimpleWrap
│ │ provides power {0 W} │ requires _result SB(≥0) W
│ │ provides extra_power SB(≥0) W │
│ └ DP_Mux SB(0)×SB(≥0) ⟨W,W⟩ ⇸ SB(≥0) W
│ iso(𝒇, 𝒓) ⟨a,b⟩ ↦ b
│ ⟨0 W,α⟩ ↤ α
├ _sum1: SimpleWrap
│ │ provides mass SB(≥0) kg │ requires _result2 SB(≥0) kg
│ │ provides extra_payload SB(≥0) kg │
│ └ M_Res_AddMany_DP SB(≥0)×SB(≥0) ⟨kg,kg⟩ ⇸ SB(≥0) kg
│ 𝒇₁ + 𝒇₂ ≤ 𝒓
│ ├ Fs: ├ SB(≥0) kg
│ │ └ SB(≥0) kg
│ ├ opspace: SB(≥0) kg
│ └ algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT
├ _sum2: SimpleWrap
│ │ provides actuation_cost {0 USD} │ requires _result3 {100 USD}
│ │ provides battery_cost {100 USD} │
│ └ DP_True {⟨0,100⟩ ⟨USD,USD⟩} ⇸ {100 USD} val = * > ()
│ true
├ actuation: CompositeNDP
│ │ provides lift {∞ N} │ requires power {0 W}
│ │ │ requires cost {0 USD}
│ │ 6 nodes, 3 edges
│ │ connected rec: ✓
│ │ power required by _constant ≤ required power equiv (always satisfied)
│ │ cost required by _constant1 ≤ required cost equiv (always satisfied)
│ │ provided lift ≤ lift provided by _limit equiv (always satisfied)
│ ├ _constant: SimpleWrap
│ │ │ - │ requires power {0 W}
│ │ └ DP_Constant 𝟙 ⇸ {0 W}
│ │ 0 W ≤ 𝒓
│ ├ _constant1: SimpleWrap
│ │ │ - │ requires cost {0 USD}
│ │ └ DP_Constant 𝟙 ⇸ {0 USD}
│ │ 0 USD ≤ 𝒓
│ └ _limit: SimpleWrap
│ │ provides lift {∞ N} │ -
│ └ DP_Limit {∞ N} ⇸ 𝟙 > NVU:∞ N
│ 𝒇 ≤ ∞ N
└ battery: CompositeNDP
│ provides capacity SB(≥0) J │ requires mass SB(≥0) kg
│ │ requires cost {100 USD}
│ 6 nodes, 4 edges
│ connected rec: ✓
│ _c required by _c ≤ required cost equiv (always satisfied)
│ mass required by _conversion ≤ required mass equiv id
│ _res required by _divr ≤ _res provided by _conversion equiv id
│ provided capacity ≤ _op provided by _divr equiv id
├ _c: SimpleWrap
│ │ - │ requires _c {100 USD}
│ └ DP_Constant 𝟙 ⇸ {100 USD}
│ 100 USD ≤ 𝒓
├ _conversion: SimpleWrap
│ │ provides _res SB(≥0) J*kg/Wh │ requires mass SB(≥0) kg
│ └ UnitConversion SB(≥0) J*kg/Wh ⇸ SB(≥0) kg
│ 𝒇 [J*kg/Wh] ≤ 𝒓 [kg]
│ ├ F0: SB(≥0)
│ ├ factor: 1/3600
│ ├ F_units: SingleUnits J*kg/Wh
│ └ R_units: SingleUnits kg
└ _divr: SimpleWrap
│ provides _op SB(≥0) J │ requires _res SB(≥0) J*kg/Wh
└ DP_L_UME SB(≥0) J ⇸ SB(≥0) J*kg/Wh
𝒇 / 100 ≤ 𝒓
M_C_WrapUnits J → J*kg/Wh > M_A_Divide1_Upper SB(≥0) → same x ⟼ x / 100