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

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

    在AlphaProof使用intro策略后，此时的目的（Goal）为：    这时，AlphaProof使用induction策略，对 n:ℕ进行，归纳证明：    induction策略，在假设中，增加了，在归纳证明中使用的，前值假设，即：    改写后的目的（Goal）的高亮部分，a:∀m<n,