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.