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