🎯 증명 대상 명제

모든 명령문 S와 상태 s에 대해,

만약 <S, s> → s' 가 성립한다면,

<S, s> ⇒* s' 도 성립한다.

즉, big-step semantics로 s'에 도달할 수 있다면,

small-step semantics로도 여러 단계를 거쳐 s'에 도달할 수 있다는 것.

✅ 전략: Induction on the derivation of <S, s> → s'

즉, <S, s> → s' 라는 도출 트리의 구조에 대해 귀납한다.

각 경우는 big-step 규칙의 각 inference rule에 해당하며, 각각을 따져야 한다.

📌 Base Case: (SKIP)

─────────────── (B-Skip)
<skip, s> → s

• 여기서 small-step 규칙에서는 <skip, s> ⇒* s (0단계) 이므로 바로 성립 ✅

📌 Case: (SEQ)

<S1, s> → s''    <S2, s''> → s'
───────────────────────────── (B-Seq)
<S1; S2, s> → s'

귀납 가정 (IH):

• <S1, s> → s'' 이므로 IH에 따라 <S1, s> ⇒* s''
• <S2, s''> → s' 이므로 IH에 따라 <S2, s''> ⇒* s'

small-step에서는:

1. <S1; S2, s> ⇒* <S2, s''> (→ S1이 skip 될 때까지 reduction 진행)