This appendix defines the full set of big-step operational semantics rules for all core constructs in the bounded arithmetic language. Each rule updates the resource state R = (steps, stack_depth, max_nat_depth).
A.1 Arithmetic Rules
(E-Sub-Zero) If ⟨e, R⟩ ⇓ ⟨v, R’⟩, then ⟨sub(e, 0), R⟩ ⇓ ⟨v, R’ + (1, 0, 0)⟩
(E-Sub-Succ) If ⟨e1, R⟩ ⇓ ⟨S(v1), R1⟩, ⟨e2, R1⟩ ⇓ ⟨S(v2), R2⟩, and ⟨sub(v1, v2), R2⟩ ⇓ ⟨v3, R3⟩, then ⟨sub(S(e1), S(e2)), R⟩ ⇓ ⟨v3, R3 + (1, 0, 0)⟩
(E-Sub-Under) If ⟨e2, R⟩ ⇓ ⟨S(v2), R’⟩, then ⟨sub(0, S(e2)), R⟩ ⇓ ⟨error(“E102”), R’⟩
(E-Mul-Zero) If ⟨e2, R⟩ ⇓ ⟨v2, R’⟩, then ⟨mul(0, e2), R⟩ ⇓ ⟨0, R’ + (1, 0, 0)⟩
(E-Mul-Succ) If ⟨e1, R⟩ ⇓ ⟨S(v1), R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, ⟨mul(v1, v2), R2⟩ ⇓ ⟨v3, R3⟩, ⟨add(v2, v3), R3⟩ ⇓ ⟨v4, R4⟩, then ⟨mul(S(e1), e2), R⟩ ⇓ ⟨v4, R4 + (1, 0, 0)⟩
A.2 Division Rules
(E-Div) If ⟨div_safe(e1, e2, 0), R⟩ ⇓ ⟨v, R’⟩, then ⟨div(e1, e2), R⟩ ⇓ ⟨v, R’ + (1, 0, 0)⟩
(E-Div-Guard) If steps ≥ max_div_steps, then ⟨div_safe(e1, e2, steps), R⟩ ⇓ ⟨error(“E004”), R⟩
(E-Div-Zero) If ⟨e2, R⟩ ⇓ ⟨0, R’⟩, then ⟨div_safe(e1, e2, steps), R⟩ ⇓ ⟨error(“E103”), R’⟩
(E-Div-Base) If ⟨e1, R⟩ ⇓ ⟨v1, R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, and lt(v1, v2) = B1, then ⟨div_safe(e1, e2, steps), R⟩ ⇓ ⟨0, R2 + (1, 0, 0)⟩
(E-Div-Rec) If ⟨e1, R⟩ ⇓ ⟨v1, R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, lt(v1, v2) = B0, v2 ≠ 0, steps < max_div_steps, ⟨sub(v1, v2), R2⟩ ⇓ ⟨v3, R3⟩, ⟨div_safe(v3, v2, S(steps)), R3⟩ ⇓ ⟨v4, R4⟩, then ⟨div_safe(e1, e2, steps), R⟩ ⇓ ⟨S(v4), R4 + (1, 0, 0)⟩
A.3 Boolean Logic Rules
(E-And-False) If ⟨e1, R⟩ ⇓ ⟨B0, R’⟩, then ⟨and(e1, e2), R⟩ ⇓ ⟨B0, R’ + (1, 0, 0)⟩
(E-And-True) If ⟨e1, R⟩ ⇓ ⟨B1, R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, then ⟨and(e1, e2), R⟩ ⇓ ⟨v2, R2 + (1, 0, 0)⟩
(E-Or-True) If ⟨e1, R⟩ ⇓ ⟨B1, R’⟩, then ⟨or(e1, e2), R⟩ ⇓ ⟨B1, R’ + (1, 0, 0)⟩
(E-Or-False) If ⟨e1, R⟩ ⇓ ⟨B0, R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, then ⟨or(e1, e2), R⟩ ⇓ ⟨v2, R2 + (1, 0, 0)⟩
(E-Not-True) If ⟨e, R⟩ ⇓ ⟨B1, R’⟩, then ⟨not(e), R⟩ ⇓ ⟨B0, R’ + (1, 0, 0)⟩
(E-Not-False) If ⟨e, R⟩ ⇓ ⟨B0, R’⟩, then ⟨not(e), R⟩ ⇓ ⟨B1, R’ + (1, 0, 0)⟩
A.4 Comparison Rules
(E-Eq-Zero) ⟨eq(0, 0), R⟩ ⇓ ⟨B1, R + (1, 0, 0)⟩
(E-Eq-Succ) If ⟨e1, R⟩ ⇓ ⟨S(v1), R1⟩, ⟨e2, R1⟩ ⇓ ⟨S(v2), R2⟩, ⟨eq(v1, v2), R2⟩ ⇓ ⟨v3, R3⟩, then ⟨eq(S(e1), S(e2)), R⟩ ⇓ ⟨v3, R3 + (1, 0, 0)⟩
(E-Eq-Diff) If ⟨e1, R⟩ ⇓ ⟨v1, R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, and structure(v1) ≠ structure(v2), then ⟨eq(e1, e2), R⟩ ⇓ ⟨B0, R2 + (1, 0, 0)⟩
[Rules for lt, le, gt, ge follow the same structure.]
A.5 Guard and Error Rules
(E-Guard-Steps) If R.steps ≥ max_steps, then ⟨e, R⟩ ⇓ ⟨error(“E003”), R⟩
(E-Guard-Stack) If R.stack_depth ≥ max_stack_depth, then ⟨e, R⟩ ⇓ ⟨error(“E002”), R⟩
(E-Guard-Nat) If depth(S(v)) > max_nat_size, then ⟨S(e), R⟩ ⇓ ⟨error(“E201”), R⟩
(E-Error-Prop) If ⟨e1, R⟩ ⇓ ⟨error(msg), R’⟩, then ⟨op(e1, e2), R⟩ ⇓ ⟨error(msg), R’⟩