1. Even( Nat ).
  2. / Even( 'z' ).
  3. Even( n ) / Even( 'ss' n ).
여기서 "Even( a )?"라고 질의가 오면 뭐라고 답해야 될까요?

제 1 안)
모든 a를 열거한다:
a = 'z', 'ssz', 'ssssz', ....
원래 어떤 변수 배정에서 식을 유도할 수 있는지를 답해야하기 때문에 이렇게 답하는 게 맞다. 
하지만 유한 시간 안에 모든 a를 열거할 수 없기 때문에 아름답지 못한 해법이다.

제 2 안)
형식 문법에서 힌트를 얻어 이렇게 응답한다:
a → 'z'.
a → 'ss' a.
비슷한 의미로 변수 Nat1을 도입하여
1) a → 'z'. - Answer
2) a → 'ss' Nat1.
2.1) Nat1 = a. - Answer
로 답하게 할 수 있다.

어떻게 설계해야 이렇게 답할까?

귀납법을 사용하게끔 해야한다.

그건 어떻게 할까? 나도 모르겠다.