Enumeration order of proofs is not specified, so we can construct pathological prover, that reorders proofs such that all proofs of “main()==1” require more steps than maxsteps.
You can’t influence the length of a proof by placing it at a different position in some list of proofs. Parameter ‘maxsteps’ specifies the maximum length (or Gödel number) of the proofs that get checked, not the maximum number of steps performed by the proof checker algorithm.
Enumeration order of proofs is not specified, so we can construct pathological prover, that reorders proofs such that all proofs of “main()==1” require more steps than maxsteps.
You can’t influence the length of a proof by placing it at a different position in some list of proofs. Parameter ‘maxsteps’ specifies the maximum length (or Gödel number) of the proofs that get checked, not the maximum number of steps performed by the proof checker algorithm.
Ouch. maxsteps means maxprooflenght. My inattention, sorry.