🎯 증명하려는 명제

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

만약 <S, s> → s' (big-step)이 성립하면,

<S, s> ⇒* s' (small-step의 multi-step closure)도 성립한다.

이걸 Structural Induction on S로 증명하려고 시도하되, **S = while b do S1**일 때 실패하게 될 거야.

🔧 Structural Induction으로 시도

귀납의 기준: S의 구조

Base case: S = skip

• <skip, s> → s (big-step)
• small-step 규칙: <skip, s> ⇒* s (0단계)
• 성립함 ✅

Case: S = S1; S2

• 귀납 가정:
  • <S1, s> → s'' → <S1, s> ⇒* s''
  • <S2, s''> → s' → <S2, s''> ⇒* s'
• big-step 도출:<S1, s> → s'', <S2, s''> → s' ⟹ <S1; S2, s> → s'
• small-step에서는:<S1; S2, s> ⇒* <S2, s''> ⇒* s'
• 귀납 가정 사용해서 성립함 ✅

❌ 문제 Case: S = while b do S1

big-step 규칙: