Z3证明：假设和引理规则总是干净地嵌套？

Question

快速提问：在Z3证明（例如4.3.2）中，“假设”规则引入了局部假设，最终通过“引理”规则解除。是“假设”和“引理”规则总是干净嵌套，这意味着人们可以Z3证明映射到与嵌套证明块的语言，或者一个可以有一个序列

hypothesis 1 
hypothesis 2 
lemma 1 
lemma 2 

？谢谢。

Answer 1

你说得对，文档不清楚。 我正在更新到：

\nicebox{ 
     T1: false 
     [lemma T1]: (or (not l_1) ... (not l_n)) 
     } 
     This proof object has one antecedent: a hypothetical proof for false. 
     It converts the proof in a proof for (or (not l_1) ... (not l_n)), 
     when T1 contains the open hypotheses: l_1, ..., l_n. 
     The hypotheses are closed after an application of a lemma. 
     Furthermore, there are no other open hypotheses in the subtree covered by 
     the lemma.