Clarify proving bottom-up dialogue

[david-a-wheeler]

The "proving bottom-up" dialogue box options can be a little confusing. Here are suggestions, based on what I think it's doing. If my understanding is wrong, please change the text to make these confusions less likely in the future :-).

Change "Root statements" to "Required statements". I think the point is to tell metamath-lamp that it must use these statements. "Root" is confusing here.

Change "Label" to "Label of root justification" or "Root label" or something like that. Yes, it's a label, but what does the label select? It's the initial justification or root justification or something like that.

I think that "length restriction" controls how "Search depth" is interpreted, but that's not obvious. It should be more obvious that "length restriction" and "search depth" are related, and that they're not related to the "label" on the same line. If that's the right interpretation, I'd put a spacer before this pair (so it's clearly not related to "label"), and reverse their order like this:

• Search depth restriction: "<", "<=", "Unrestricted"
• Search depth: (Number) - grey this out when "Unrestricted" is selected and show "N/A"

[expln]

I think you created this issue before my explanations on this topic.

Change "Root statements" to "Required statements". I think the point is to tell metamath-lamp that it must use these statements. "Root" is confusing here.

I think "allowed statements" better suits its real meaning.

Change "Label" to "Label of root justification"

Ok.

I think that "length restriction" controls how "Search depth" is interpreted

You already know what "length restriction" does :) I think "length restriction" is quite a good name for this option. (for those who are reading this and don't know what "length restriction" controls - in short, it controls if new statements can be longer then existing or not)

"Unrestricted"

Ok, I will replace "No" with "Unrestricted"

[expln]

"<", "<="

I usually have troubles understanding those operators. For example, a < b could mean both a is less then b and b is greater than a. For me it is difficult to quickly infer what < means - greater or less. Probably for other users too. So I would not rename Less and LessEq options.

[david-a-wheeler]

I think you created this issue before my explanations on this topic.

You're correct, of course :-). So I think the goal now is "change the displayed text so future users won't have such absurd misunderstandings".

I think "allowed statements" better suits its real meaning.

Yes, that sounds great. That text would have eliminated my misunderstanding.

I think "length restriction" is quite a good name for this option.

Is there room for saying "statement length restriction" instead? It's not a restriction on the "length of the depth" - part of my confusion was that it was near "search depth".

"Less" and "LessEq" are fine. My bigger problem was misunderstanding what the "length restriction" was all about.

[expln]

All the requested changes are implemented on dev.