z3 - 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.