CompositeNDP                                                                                                                         
│    provides   f_1   SB(≥0) │ requires   r_1   SB(≥0)                                                                               
│  8 nodes, 7 edges                                                                                                                  
│   connected rec: ✓                                                                                                                 
│  _op required by _RuleFunFloor_NWU ≤ required r_1                          equiv id                                                
│  _res required by _RuleResCeil_NWU ≤ _op provided by _mult                 equiv id                                                
│  provided f_1                      ≤ _op provided by _RuleResCeil_NWU      equiv id                                                
│  _op required by _invmultvalue     ≤ _res4 provided by _RuleFunFloor_NWU   equiv id                                                
│  _op required by _invplusop        ≤ _result provided by _invmultvalue     equiv id                                                
│  _res2 required by _mult           ≤ _op provided by _plus                 equiv id                                                
│  _res3 required by _plus           ≤ _res4 provided by _invplusop          diff  AmbientConversion SB(≥3::5)  ⇸  SB(≥10::1.2)  > D 
│                                                                                   𝒇 ≤ 𝒓                                            
├ _RuleFunFloor_NWU: SimpleWrap                                                                                                      
│                    │  provides   _res4   SB(≥0::1) │ requires   _op   SB(≥0)                                                       
│                    └ DP_L_LME SB(≥0::1)  ⇸  SB(≥0)                                                                                 
│                       𝒇 ≤ floor(𝒓)                                                                                                 
│                      └ M_C_WrapUnits   dimensionless → dimensionless                                                               
│                        M_A_RoundDown   SB(≥0)  →  SB(≥0::1) x ⟼ floor(x)                                                           
├  _RuleResCeil_NWU: SimpleWrap                                                                                                      
│                    │  provides   _op   SB(≥0) │ requires   _res   SB(≥0::1)                                                        
│                    └ DP_L_UME SB(≥0)  ⇸  SB(≥0::1)                                                                                 
│                       ceil(𝒇) ≤ 𝒓                                                                                                  
│                      └ M_C_WrapUnits   dimensionless → dimensionless                                                               
│                        M_A_RoundUp   SB(≥0)  →  SB(≥0::1) x ⟼ ceil(x)                                                              
├     _invmultvalue: SimpleWrap                                                                                                      
│                    │  provides   _result   SB(≥0::1.2) │ requires   _op   SB(≥0::1)                                                
│                    └ DP_L_LME SB(≥0::1.2)  ⇸  SB(≥0::1)                                                                            
│                       𝒇 ≤ 𝒓 ⋅ 1.2                                                                                                  
│                      └ M_C_WrapUnits   dimensionless → dimensionless                                                               
│                        M_A_Mult1_Lower   SB(≥0::1)  →  SB(≥0::1.2) x ⟼ x ⋅ 1.2                                                     
├        _invplusop: SimpleWrap                                                                                                      
│                    │  provides   _res4   SB(≥10::1.2) │ requires   _op   SB(≥0::1.2)                                               
│                    └ DP_L_LME SB(≥10::1.2)  ⇸  SB(≥0::1.2)                                                                         
│                       𝒇 ≤ 𝒓 + 10                                                                                                   
│                      └ M_C_WrapUnits   dimensionless → dimensionless                                                               
│                        M_A_Add1_Lower   SB(≥0::1.2)  →  SB(≥10::1.2) x ⟼ x + 10                                                    
├             _mult: SimpleWrap                                                                                                      
│                    │  provides   _op   SB(≥0::1) │ requires   _res2   SB(≥0::5)                                                    
│                    └ DP_L_UME SB(≥0::1)  ⇸  SB(≥0::5)                                                                              
│                       𝒇 ⋅ 5 ≤ 𝒓                                                                                                    
│                      └ M_C_WrapUnits   dimensionless → dimensionless                                                               
│                        M_A_Mult1_Upper   SB(≥0::1)  →  SB(≥0::5) x ⟼ x ⋅ 5                                                         
└             _plus: SimpleWrap                                                                                                      
                     │  provides   _op   SB(≥0::5) │ requires   _res3   SB(≥3::5)                                                    
                     └ DP_L_UME SB(≥0::5)  ⇸  SB(≥3::5)                                                                              
                        𝒇 + 3 ≤ 𝒓                                                                                                    
                       └ M_C_WrapUnits   dimensionless → dimensionless                                                               
                         M_A_Add1_Upper   SB(≥0::5)  →  SB(≥3::5) x ⟼ x + 3