25.19 레이터(Reiter)의 후계 상태 공리 형식화와 완전성 증명