Conservative definition
Parameters: ab, ac, bb, bc, cb, cc, db, dc, ub, uc, vb, vc, wb, wc, xb, xc, i
∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ j. ∃ u. ∃ v. ∃ w. ∃ x0. ∃ x1. S m ≤ S (S i · ac) ∧ (∃ x2. ab = x2 · S (S i · ac) + m) ∧ (S k ≤ S (S i · bc) ∧ (∃ x2. bb = x2 · S (S i · bc) + k) ∧ (S j ≤ S (S i · cc) ∧ (∃ x2. cb = x2 · S (S i · cc) + j) ∧ (S u ≤ S (S i · dc) ∧ (∃ x2. db = x2 · S (S i · dc) + u)))) ∧ (S x ≤ S (S i · uc) ∧ (∃ x2. ub = x2 · S (S i · uc) + x) ∧ (S y ≤ S (S i · vc) ∧ (∃ x2. vb = x2 · S (S i · vc) + y) ∧ (S z ≤ S (S i · wc) ∧ (∃ x2. wb = x2 · S (S i · wc) + z) ∧ (S n ≤ S (S i · xc) ∧ (∃ x2. xb = x2 · S (S i · xc) + n)))) ∧ (S v ≤ S (S S i · uc) ∧ (∃ x2. ub = x2 · S (S S i · uc) + v) ∧ (S w ≤ S (S S i · vc) ∧ (∃ x2. vb = x2 · S (S S i · vc) + w) ∧ (S x0 ≤ S (S S i · wc) ∧ (∃ x2. wb = x2 · S (S S i · wc) + x0) ∧ (S x1 ≤ S (S S i · xc) ∧ (∃ x2. xb = x2 · S (S S i · xc) + x1)))) ∧ (v + (x · k + y · m + 2 · (z · u + n · j)) = x · m + y · k + 2 · (z · j + n · u) + w ∧ x0 + (x · u + y · j + (z · k + n · m)) = x · j + y · u + (z · m + n · k) + x1)))