Z3 proofs: Are hypothesis and lemma rules always cleanly nested?

Question

Quick question: In a Z3 proof (e.g. 4.3.2), a "hypothesis" rule introduces a local assumption, which is eventually discharged by a "lemma" rule. Are "hypothesis" and "lemma" rules always cleanly nested, meaning that one could map Z3 proofs to a language with nested proof blocks, or can one have a sequence

hypothesis 1
hypothesis 2
lemma 1
lemma 2

? Thanks.

Answer 1

You are right, the documentation isn't clear on this. I am updating it to:

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