Conservative definition
Parameters: x, wb, wc, tb, tc, K
∀ y. ∀ z. ∀ n. ∀ m. S y ≤ K → S z ≤ S (S y · wc) ∧ (∃ k. wb = k · S (S y · wc) + z) → (∃ k. ∃ i. (∀ j. S j ≤ y → S x ≤ S (S j · i) ∧ (∃ u. k = u · S (S j · i) + x)) ∧ (∃ j. ∃ u. 2 ≤ S (1 · u) ∧ (∃ v. j = v · S (1 · u) + 1) ∧ (S n ≤ S (S y · u) ∧ (∃ v. j = v · S (S y · u) + n) ∧ (∀ v. S v ≤ y → ∃ w. ∃ x0. ∃ x1. S w ≤ S (S v · i) ∧ (∃ x2. k = x2 · S (S v · i) + w) ∧ (S x0 ≤ S (S v · u) ∧ (∃ x2. j = x2 · S (S v · u) + x0) ∧ (S x1 ≤ S (S S v · u) ∧ (∃ x2. j = x2 · S (S S v · u) + x1) ∧ x1 = x0 · w)))))) → S m ≤ S (S y · tc) ∧ (∃ k. tb = k · S (S y · tc) + m) → m = z · nDefinition prerequisites
Theorem uses (notation, not proof premises)
AP026 · AP044 · AP047 · AP050 · AP058 · AP066 · AP067 · AP086 · AP091 · AP092 · CV069 · CV070 · CV071