Fix "assumptions before steps" in subproof

• Clarify in document that it's not allowed to issue an (assume...) command after a the first (step..) at the beginning of the proof or after an (anchor...).
• Make sure veriT follows this rule (it doesn't currently)

added clarification format veriT labels

marked the checklist item Clarify in document that it's not allowed to issue an (assume...) command after a the first (step..) at the beginning of the proof or after an (anchor...). as completed

changed milestone to %Release 0.4

Can you point where this is clarified in the document? I tried to find it looking quickly but did not find it. Moreover, I believe the grammar would have to be changed to rule out the possibility of having assume after step?

In the paragraph about Subproofs it says:

After the anchor command, the proof uses assume commands to list the assumptions of the subproof. Subsequently, the subproof is a list of step commands that can use prior steps in the subproofs as premises.

However, it is really not obvious that this implies that you cannot have assumes after step. I added a sentence there now.

Furthermore, the state machine (Figure 3) also enforces that.

I see, thanks. Since the subproof requires this anyway, I guess it's fine to require it also for the initial ones.

closed

marked the checklist item Make sure veriT follows this rule (it doesn't currently) as completed