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