SHARE
TWEET

Untitled

a guest Oct 18th, 2019 74 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. Calculation:
  2.     (∑ i : ℕ ❙ i < k • m · i)[k ≔ 4]
  3.   =⟨ Substitution ⟩
  4.     ∑ i : ℕ ❙ (i < k)[k ≔ 4] • (m · i)[k ≔ 4]
  5.   =⟨ Substitution ⟩
  6.     ∑ i : ℕ ❙ i < 4 • m · i
  7.  
  8. Calculation:
  9.     (∑ i : ℕ ❙ i < m • n · i)[m, n ≔ 3, 8]
  10.   =⟨ Substitution ⟩
  11.     ∑ i : ℕ ❙ (i < m)[m, n ≔ 3, 8] • (n · i)[m, n ≔ 3, 8]
  12.   =⟨ Substitution ⟩
  13.     ∑ i : ℕ ❙ (i < 3) • (8 · i)
  14.  
  15. Calculation:
  16.     (∑ i : ℕ ❙ i < j • k · i)[i, j, k ≔ 2, 5, 8]
  17.   =⟨ “Reflexivity of =” ⟩
  18.     (∑ a : ℕ ❙ a < j • k · a)[i, j, k ≔ 2, 5, 8]
  19.   =⟨ Substitution ⟩
  20.     ∑ a : ℕ ❙ (a < j)[i, j, k ≔ 2, 5, 8] • (k · a)[i, j, k ≔ 2, 5, 8]
  21.   =⟨ Substitution ⟩
  22.     ∑ a : ℕ ❙ (a < 5) • (8 · a)
  23.  
  24.  
  25. Calculation:
  26.     (∑ i : ℕ ❙ i < k • m · i)[m ≔ i · j]
  27.   =⟨ “Reflexivity of =” ⟩
  28.     (∑ a : ℕ ❙ a < k • m · a)[m ≔ i · j]
  29.   =⟨ Substitution ⟩
  30.     ∑ a : ℕ ❙ (a < k)[m ≔ i · j] • (m · a)[m ≔ i · j]
  31.   =⟨ Substitution ⟩
  32.     ∑ a : ℕ ❙ (a < k) • (i · j · a)
  33.  
  34. Calculation:
  35.     (∑ i : ℕ ❙ i < k • (∑ j : ℕ ❙ j < i • m · j))[m ≔ j + k]
  36.   =⟨ “Reflexivity of =” ⟩
  37.     (∑ i : ℕ ❙ i < k • (∑ a : ℕ ❙ a < i • m · a))[m ≔ j + k]
  38.   =⟨ Substitution ⟩
  39.     ∑ i : ℕ ❙ (i < k)[m ≔ j + k] • (∑ a : ℕ ❙ a < i • m · a)[m ≔ j + k]
  40.   =⟨ Substitution ⟩
  41.     ∑ i : ℕ ❙ (i < k)[m ≔ j + k] • (∑ a : ℕ ❙ (a < i)[m ≔ j + k] • (m · a)[m ≔ j + k])
  42.   =⟨ Substitution ⟩
  43.     ∑ i : ℕ ❙ (i < k) • (∑ a : ℕ ❙ (a < i) • ((j + k) · a))
  44.  
  45.  
  46. Calculation:
  47.     (∑ i : ℕ ❙ i < k • (∑ j : ℕ ❙ j < i • m · j))[k ≔ 2 · i]
  48.   =⟨ “Reflexivity of =” ⟩
  49.     (∑ a : ℕ ❙ a < k • (∑ j : ℕ ❙ j < a • m · j))[k ≔ 2 · i]
  50.   =⟨ Substitution ⟩
  51.     (∑ a : ℕ ❙ (a < k)[k ≔ 2 · i] • (∑ j : ℕ ❙ j < a • m · j)[k ≔ 2 · i])
  52.   =⟨ Substitution ⟩
  53.     (∑ a : ℕ ❙ (a < k)[k ≔ 2 · i] • (∑ j : ℕ ❙ (j < a)[k ≔ 2 · i] • (m · j)[k ≔ 2 · i]))
  54.   =⟨ Substitution ⟩
  55.     (∑ a : ℕ ❙ (a < 2 · i) • (∑ j : ℕ ❙ (j < a) • (m · j)))
  56.  
  57.  
  58. Calculation:
  59.     (∑ i : ℕ ❙ i < k • (∑ j : ℕ ❙ j < i • m · j))[m ≔ i · j]
  60.   =⟨ “Reflexivity of =” ⟩
  61.     (∑ a : ℕ ❙ a < k • (∑ j : ℕ ❙ j < a • m · j))[m ≔ i · j]
  62.   =⟨ “Reflexivity of =” ⟩
  63.     (∑ a : ℕ ❙ a < k • (∑ b : ℕ ❙ b < a • m · b))[m ≔ i · j]
  64.   =⟨ Substitution ⟩
  65.     (∑ a : ℕ ❙ (a < k)[m ≔ i · j] • (∑ b : ℕ ❙ b < a • m · b)[m ≔ i · j])
  66.   =⟨ Substitution ⟩
  67.     (∑ a : ℕ ❙ (a < k)[m ≔ i · j] • (∑ b : ℕ ❙ (b < a)[m ≔ i · j] • (m · b)[m ≔ i · j]))
  68.   =⟨ Substitution ⟩
  69.     (∑ a : ℕ ❙ (a < k) • (∑ b : ℕ ❙ (b < a) • (i · j · b)))
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top