& Y [[* *] ['* (* *)]]. & zero ^z ^s z. & suc ^n ^z ^s (s n). & plus (Y ^r ^n ^p (n p ^q (suc (r q p)))). & times (Y ^r ^n ^p (n zero ^q (plus p (r q p)))). & fact (Y ^r ^n (n (suc zero) ^q (times n (r q)))). -(fact zero). -(fact (suc zero)). -(fact (suc (suc zero))). -(fact (suc (suc (suc zero)))).