书接上文，此时，AlphaProof关注的目的如下：    接着，AlphaProof使用了simp_all与have策略，如下：    此前已对上述两策略进行讲解，这里就不再赘述了。    在第二个simp_all策略完成后，目的被改写为：    此时，AlphaProof使用c

     书接上文，AlphaProof通过suffices和have策略，产生其需要的假设后，使用了一系列的norm_num与rw策略，进行简化，如下：    使得目的被改写为：    此后，再通过连续使用两次zify策略，如下    其中，at*，意思是，作用于当前目的的所有假设