앞 장의 정리가 쓰이는 곳🔗

명제 1.4 (치환 정리)

대입 공리의 건전성. 1장 §1.4에서 포획을 피하는 치환을 애써 만든 것이 이 한 줄을 위해서였다.

명제 1.1 (일치 정리)

변수 선언 규칙의 세 신선함 조건, 상수 규칙, 유령 변수.

Scott 귀납법 (§2.4)

while 규칙의 건전성, 그리고 wlp가 최대 고정점이라는 정리.

명제 2.6 (명령의 일치 정리)

상수 규칙, ∃ 규칙, 전체 정확성 while 규칙.

연습 2.8 (약한 치환 정리)

치환 규칙. 2장에서 조건을 약화한 연습이 3장의 규칙 하나를 위한 준비였다.