Доказательства 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.