plusinv5fixed

Editor GitHub co-design-modelslibraries example_plusinv specs models thingsplusinv5fixed
Editor
Visualization
	`mcdp { variable x, y [ℕ] x + y ≽ ceil(sqrt(x)) + ceil(sqrt(y)) + 10 # x + y >= ⌈√x⌉ + ⌈√y⌉ + 10 requires x, y }`
Diagramremove
Other informationremove
Internal representation details
CompositeNDP                                                                                                                       
│    - │ requires   x   SB(≥0::1)                                                                                                  
│      │ requires   y   SB(≥0::1)                                                                                                  
│  9 nodes, 10 edges                                                                                                               
│   connected rec: ✓                                                                                                               
│  _res2 required by _RuleResCeil_NWU  ≤ _res2 provided by _sum              equiv id                                              
│  _res4 required by _RuleResCeil_NWU1 ≤ _res4 provided by _sum              equiv id                                              
│  _res required by _RuleResSQRT_NWU   ≤ _op provided by _RuleResCeil_NWU    equiv id                                              
│  _res3 required by _RuleResSQRT_NWU1 ≤ _op provided by _RuleResCeil_NWU1   equiv id                                              
│  _x required by _invplus             ≤ _op provided by _RuleResSQRT_NWU    equiv id                                              
│  _x required by _invplus             ≤ required x                          equiv id                                              
│  _y required by _invplus             ≤ _op provided by _RuleResSQRT_NWU1   equiv id                                              
│  _y required by _invplus             ≤ required y                          equiv id                                              
│  _res5 required by _plus             ≤ _result2 provided by _invplus       diff  AmbientConversion SB(≥10::1)  ⇸  SB(≥0::1)  > D 
│                                                                                   𝒇 ≤ 𝒓                                          
│  _result required by _sum            ≤ _op provided by _plus               equiv id                                              
├  _RuleResCeil_NWU: SimpleWrap                                                                                                    
│                    │  provides   _op   SB(≥0) │ requires   _res2   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)                                                            
├ _RuleResCeil_NWU1: SimpleWrap                                                                                                    
│                    │  provides   _op   SB(≥0) │ requires   _res4   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)                                                            
├  _RuleResSQRT_NWU: SimpleWrap                                                                                                    
│                    │  provides   _op   SB(≥0::1) │ requires   _res   SB(≥0)                                                      
│                    └ DP_L_UME SB(≥0::1)  ⇸  SB(≥0)                                                                               
│                       𝒇^½ ≤ 𝒓                                                                                                    
│                      └ M_C_WrapUnits   dimensionless → dimensionless                                                             
│                        M_A_PowerFrac_Upper   SB(≥0::1)  →  SB(≥0) x ⟼ x^½                                                        
├ _RuleResSQRT_NWU1: SimpleWrap                                                                                                    
│                    │  provides   _op   SB(≥0::1) │ requires   _res3   SB(≥0)                                                     
│                    └ DP_L_UME SB(≥0::1)  ⇸  SB(≥0)                                                                               
│                       𝒇^½ ≤ 𝒓                                                                                                    
│                      └ M_C_WrapUnits   dimensionless → dimensionless                                                             
│                        M_A_PowerFrac_Upper   SB(≥0::1)  →  SB(≥0) x ⟼ x^½                                                        
├          _invplus: SimpleWrap                                                                                                    
│                    │  provides   _result2   SB(≥0::1) │ requires   _x   SB(≥0::1)                                                
│                    │                                  │ requires   _y   SB(≥0::1)                                                
│                    └ M_Fun_AddMany_DP SB(≥0::1)  ⇸  WU ⟨dimensionless,dimensionless⟩                                             
│                                                     └ Π<2>                                                                       
│                                                       ├ _x: SB(≥0::1)                                                            
│                                                       └ _y: SB(≥0::1)                                                            
│                       𝒇 ≤ 𝒓₁ + 𝒓₂                                                                                                
│                      ├   opspace: SB(≥0::1)                                                                                      
│                      ├        Rs: ├ SB(≥0::1)                                                                                    
│                      │            └ SB(≥0::1)                                                                                    
│                      ├ Rs_labels: ├ _x                                                                                           
│                      │            └ _y                                                                                           
│                      └      algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT                               
├             _plus: SimpleWrap                                                                                                    
│                    │  provides   _op   SB(≥0::1) │ requires   _res5   SB(≥10::1)                                                 
│                    └ DP_L_UME SB(≥0::1)  ⇸  SB(≥10::1)                                                                           
│                       𝒇 + 10 ≤ 𝒓                                                                                                 
│                      └ M_C_WrapUnits   dimensionless → dimensionless                                                             
│                        M_A_Add1_Upper   SB(≥0::1)  →  SB(≥10::1) x ⟼ x + 10                                                      
└              _sum: SimpleWrap                                                                                                    
                     │  provides   _res2   SB(≥0::1) │ requires   _result   SB(≥0::1)                                              
                     │  provides   _res4   SB(≥0::1) │                                                                             
                     └ M_Res_AddMany_DP WU ⟨dimensionless,dimensionless⟩  ⇸  SB(≥0::1)                                             
                                        └ Π<2>                                                                                     
                                          ├ SB(≥0::1)                                                                              
                                          └ SB(≥0::1)                                                                              
                        𝒇₁ + 𝒇₂ ≤ 𝒓                                                                                                
                       ├      Fs: ├ SB(≥0::1)                                                                                      
                       │          └ SB(≥0::1)                                                                                      
                       ├ opspace: SB(≥0::1)                                                                                        
                       └    algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT