module Record.Algo.Sizes where

open import Record.Prelude hiding (_≤?_) renaming (_≤_ to _≤n_)

open ≤-Reasoning

sz-case-1 :  {m n o k}  m + suc (n + o) < k  n + 0 < k
sz-case-1 {m} {n} {o} {k} m+1+n+o<k = begin-strict
  n + 0               ≤⟨ m≤m+n (n + 0) (suc m + o)  
  n + 0 + (suc m + o) ≡⟨ solve (n  m  o  []) 
  m + suc (n + o)     <⟨ m+1+n+o<k 
  k                   
  
sz-case-2 :  {m n o k}
   suc (m + n + o) < k
   m + suc (n + o) < k
sz-case-2 {m} {n} {o} {k} sz = begin-strict
  m + suc (n + o)     ≡⟨ solve  n , m , o  
  suc (m + n + o)     <⟨ sz 
  k                   

sz-case-3' :  {m n o k}
   m + (1 + n + o) < k
   m + o < k
sz-case-3' {m} {n} {o} {k} sz = begin-strict
  m + o              <⟨ m<m+n (m + o) (s≤s z≤n) 
  m + o + (1 + n)    ≡⟨ solve  n , m , o  
  m + (1 + n + o)    <⟨ sz 
  k                    

sz-case-4 :  n {m o k}
   n + m + o < k
   n + o < k
sz-case-4 n {m} {o} {k} sz = begin-strict
  n + o         ≤⟨ m≤m+n (n + o) m 
  n + o + m     ≡⟨ solve  n , m , o  
  n + m + o     <⟨ sz 
  k             

sz-case-5 :  m {n o k}
   n + m + o < k
   m + o < k
sz-case-5 m {n} {o} {k} sz = begin-strict
  m + o         ≤⟨ m≤m+n (m + o) n 
  m + o + n     ≡⟨ solve  n , m , o  
  n + m + o     <⟨ sz 
  k             

sz-case-6 :  {m n o k}
   m + (1 + (n + o)) ≤n k
   m + n < k
sz-case-6 {m} {n} {o} {k} sz = begin-strict
  m + n              <⟨ m<m+n (m + n) (s≤s z≤n) 
  m + n + (1 + o)    ≡⟨ solve  n , m , o  
  m + (1 + (n + o))  ≤⟨ sz 
  k                  
  
sz-case-7 :  {m n o k}
   m + (1 + (n + o)) ≤n k
   m + o < k
sz-case-7 {m} {n} {o} {k} sz = begin-strict
  m + o              <⟨ m<m+n (m + o) (s≤s z≤n) 
  m + o + (1 + n)    ≡⟨ solve  n , m , o  
  m + (1 + (n + o))  ≤⟨ sz 
  k                  

sz-case-8 :  o m{n p k}
   m + n + (1 + (o + p)) < k
   o + m < k
sz-case-8 o m {n} {p} {k} sz = begin-strict
  o + m                 <⟨ m<m+n (o + m) (s≤s z≤n) 
  o + m + (1 + n + p)   ≡⟨ solve  n , m , p , o  
  m + n + (1 + (o + p)) <⟨ sz 
  k                     

sz-case-9 :  n p {m o  k}
   m + n + (1 + (o + p)) < k
   n + p < k
sz-case-9 n p {m} {o} {k} sz = begin-strict
  n + p                 <⟨ m<m+n (n + p) (s≤s z≤n) 
  n + p + (1 + m + o)   ≡⟨ solve  n , m , p , o  
  m + n + (1 + (o + p)) <⟨ sz 
  k                     
                                
sz-case-10 :  {m o k}
   o + m < k
   m < 1 + k
sz-case-10 {m} {o} {k} sz = ≤-trans (s≤s (m≤n+m m o)) (<-trans sz (s≤s m≤m))

sz-case-11 :  {m o k}
   m + o < k
   m + 0 < k
sz-case-11 {m} {o} {k} sz rewrite +-comm m 0 = ≤-trans (s≤s (m≤m+n m o)) sz

sz-case-12 :  {m n k}
   1 + (m + (1 + (1 + n))) < k
   m + n < k
sz-case-12 {m} {n} {k} sz = begin-strict
  m + n                   <⟨ m<m+n (m + n) (s≤s z≤n) 
  m + n + (1 + 1 + 1)     ≡⟨ solve  m , n  
  1 + (m + (1 + (1 + n))) <⟨ sz 
  k                       

sz-case-13 :  {m n k}
   1 + (m + (1 + n)) < k
   m + n < k
sz-case-13 {m} {n} {k} sz rewrite +-comm 1 n | sym (+-assoc m n 1) = ≤-trans (s≤s (m≤n⇒m≤1+n (m≤m+n (m + n) 1))) sz

sz-case-14 :  {m n k}
   1 + (m + n) < k
   m + (1 + n) < k
sz-case-14 {m} {n} {k} sz rewrite +-comm 1 n | sym (+-assoc m n 1) | +-comm (m + n) 1 | +-comm m n = sz  

sz-case-15 :  {m k}
   m + 1 < k
   m + 0 < k
sz-case-15 {m} {k} sz rewrite +-comm m 0 = ≤-trans (s≤s (m≤m+n m 1)) sz

sz-case-16 :  m n {o k}
   m + (1 + (n + o)) < k
   m + 0 < k
sz-case-16 m n {o} {k} sz rewrite +-comm m 0 = ≤-trans (s≤s (m≤m+n m (1 + (n + o)))) sz

sz-case-17 :  {m n o k}
   m + (1 + (n + o)) < k
   (1 + (n + o)) < k
sz-case-17 {m} {n} {o} {k} sz = ≤-trans (s≤s (m≤n+m (1 + (n + o)) m)) sz