plusinvnat5

Editor GitHub co-design-modelslibraries example_plusinv specs models thingsplusinvnat5
Editor
Visualization
	`mcdp { variable x, y [ℕ] provides z [ℕ] x + y ≥ ceil(sqrt(x)) + ceil(sqrt(y)) + provided z requires x, y }`
Diagramremove
Other informationremove
Internal representation details
CompositeNDP                                                                                         
│    provides   z   SB(≥0::1) │ 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                
│  provided z                          ≤ z provided by _sum                  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                
│  _result required by _sum            ≤ _result2 provided by _invplus       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 
└              _sum: SimpleWrap                                                                      
                     │  provides   _res2   SB(≥0::1) │ requires   _result   SB(≥0::1)                
                     │  provides   _res4   SB(≥0::1) │                                               
                     │  provides   z       SB(≥0::1) │                                               
                     └ M_Res_AddMany_DP WU ⟨dimensionless,dimensionless,dimensionless⟩  ⇸  SB(≥0::1) 
                                        └ Π<3>                                                       
                                          ├ SB(≥0::1)                                                
                                          ├ SB(≥0::1)                                                
                                          └ SB(≥0::1)                                                
                        𝒇₁ + 𝒇₂ + 𝒇₃ ≤ 𝒓                                                             
                       ├      Fs: ├ SB(≥0::1)                                                        
                       │          ├ SB(≥0::1)                                                        
                       │          └ SB(≥0::1)                                                        
                       ├ opspace: SB(≥0::1)                                                          
                       └    algo: ApproximationAlgorithms - ApproximationAlgorithms.VAN_DER_CORPUT