Conservative definition
Parameters: ab, ac, t, H, y
∃ x. ∃ z. 1 ≤ S (1 · z) ∧ (∃ n. x = n · S (1 · z) + 0) ∧ (∀ n. S n ≤ H → ∃ m. ∃ k. S m ≤ S (S n · z) ∧ (∃ i. x = i · S (S n · z) + m) ∧ (S k ≤ S (S n · ac) ∧ (∃ i. ab = i · S (S n · ac) + k) ∧ (S (t · m + k) ≤ S (S S n · z) ∧ (∃ i. x = i · S (S S n · z) + (t · m + k))))) ∧ (S y ≤ S (S H · z) ∧ (∃ n. x = n · S (S H · z) + y))Definition prerequisites
Theorem uses (notation, not proof premises)
AP017 · AP019 · AP020 · AP025 · AP032 · AP034 · AP047 · AP050 · AP082 · AP083 · AP084 · AP085 · AP086 · AP087 · AP088 · AP089 · AP090 · AP091 · AP092 · CV059 · CV060 · CV061 · CV062 · CV063 · CV064 · CV065 · CV066 · CV074 · CV075 · CV076 · CV077 · CV080 · CV081 · CV082 · CV084 · CV085 · CV086 · CV089 · CV090 · CV091 · CV092 · CV093