It appears that the auto-prover can fail in certain situation, resulting in a technical error instead of an orange turnstile : example
Here is a documentation of cases for a similar error :
If you have a top followed by 17 ?0 it works, but with 18 or more it doesn't.
If the top is not at the beginning, you can have up to 18 ?0 : with 18 / with 19.
You can replace the ?0 with ?A for the same results, and with different why-not formulas too.
If you replace the top with a ?T or a !T, it's the same (except when every other formula is ?0, in which case the prover detects the possibility to reduce to an axiom even with many ?0).
If you add !A or A after the top, the rules are still the same : works until 17 ?A if top if before all the ?A, 18 if not. The place (as long as they are after the top) and number of !A and A doesn't matter.
If there is at least one !A or A before the top, no matter if there is one after, all the numerical limits are lowered by one : 16 ?A at most if top is before them, 17 otherwise.
The same holds if top is replaced with ?T (with !T, it is immediately detected as not being provable).
In the case of top (and not ?T) being before all the ?A, you are always allowed to have up to 17 ?A, and the proof is made in a single step : apply immediately the top rule, which is not what was done without the A / !A.
It appears that the auto-prover can fail in certain situation, resulting in a technical error instead of an orange turnstile : example Here is a documentation of cases for a similar error : If you have a top followed by 17 ?0 it works, but with 18 or more it doesn't. If the top is not at the beginning, you can have up to 18 ?0 : with 18 / with 19. You can replace the ?0 with ?A for the same results, and with different why-not formulas too.
If you replace the top with a ?T or a !T, it's the same (except when every other formula is ?0, in which case the prover detects the possibility to reduce to an axiom even with many ?0).
If you add !A or A after the top, the rules are still the same : works until 17 ?A if top if before all the ?A, 18 if not. The place (as long as they are after the top) and number of !A and A doesn't matter. If there is at least one !A or A before the top, no matter if there is one after, all the numerical limits are lowered by one : 16 ?A at most if top is before them, 17 otherwise. The same holds if top is replaced with ?T (with !T, it is immediately detected as not being provable). In the case of top (and not ?T) being before all the ?A, you are always allowed to have up to 17 ?A, and the proof is made in a single step : apply immediately the top rule, which is not what was done without the A / !A.