forked from metamath/metamath-exe
-
Notifications
You must be signed in to change notification settings - Fork 0
/
mmhlpb.c
1451 lines (1340 loc) · 73.6 KB
/
mmhlpb.c
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
/*****************************************************************************/
/* Copyright (C) 2019 NORMAN MEGILL nm at alum.mit.edu */
/* License terms: GNU General Public License */
/*****************************************************************************/
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/
/* Part 2 of help file for Metamath */
/* To add a new help entry, you must add the command syntax to mmcmdl.c
as well as adding it here. */
#include <string.h>
#include <stdio.h>
#include "mmvstr.h"
#include "mmdata.h"
#include "mmcmds.h"
#include "mmhlpb.h"
void help2(vstring helpCmd)
{
/* 5-Sep-2012 nm */
vstring saveHelpCmd = "";
/* help2() may be called with a temporarily allocated argument (left(),
cat(), etc.), and the let()s in the eventual print2() calls will
deallocate and possibly corrupt helpCmd. So, we grab a non-temporarily
allocated copy here. (And after this let(), helpCmd will become invalid
for the same reason.) */
let(&saveHelpCmd, helpCmd);
printHelp = !strcmp(saveHelpCmd, "HELP");
H("Welcome to Metamath. Here are some general guidelines.");
H("");
H("To make the most effective use of Metamath, you should become familiar");
H("with the Metamath book. In particular, you will need to learn");
H("the syntax of the Metamath language.");
H("");
H("For help using the command line, type HELP CLI.");
H("For help invoking Metamath, type HELP INVOKE.");
H("For a summary of the Metamath language, type HELP LANGUAGE.");
H("For a summary of comment markup, type HELP VERIFY MARKUP.");
H("For help getting started, type HELP DEMO.");
H("For help exploring the data base, type HELP EXPLORE.");
H("For help creating a LaTeX file, type HELP TEX.");
H("For help creating Web pages, type HELP HTML.");
H("For help proving new theorems, type HELP PROOF_ASSISTANT.");
H("For a list of help topics, type HELP ? (to force an error message).");
H("For current program settings, type SHOW SETTINGS.");
H("For a simple but general-purpose ASCII file manipulator, type TOOLS.");
H("To exit Metamath, type EXIT (or its synonym QUIT).");
H("");
H(cat("If you need technical support, contact Norman Megill at nm",
"@", "alum.mit.edu.", NULL));
H("Copyright (C) 2018 Norman Megill License terms: GPL 2.0 or later");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP COMMENTS");
H("Comment markup is described near the end of HELP LANGUAGE. See also");
H("HELP HTML for the $t comment and HTML definitions.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP INVOKE");
H("To invoke Metamath from a Unix/Linux/MacOSX prompt, assuming that the");
H("Metamath program is in the current directory, type");
H("");
H(" bash$ ./metamath");
H("");
H("To invoke Metamath from a Windows DOS or Command Prompt, assuming that");
H("the Metamath program is in the current directory (or in a directory");
H("included in the Path system environment variable), type");
H("");
H(" C:\\metamath>metamath");
H("");
H("To use command-line arguments at invocation, the command-line arguments");
H("should be a list of Metamath commands, surrounded by quotes if they");
H("contain spaces. In Windows DOS, the surrounding quotes must be double");
H("(not single) quotes. For example, to read the database set.mm, verify");
H("all proofs, and exit the program, type (under Unix)");
H("");
H(" bash$ ./metamath 'read set.mm' 'verify proof *' exit");
H("");
H("Note that in Unix, any directory path with /'s must be surrounded by");
H("quotes so Metamath will not interpret the / as a command qualifier. So");
H("if set.mm is in the /tmp directory, use for the above example");
H("");
H(" bash$ ./metamath 'read \"/tmp/set.mm\"' 'verify proof *' exit");
H("");
H("For convenience, if the command-line has one argument and no spaces in");
H("the argument, the command is implicitly assumed to be READ. In this one");
H("special case, /'s are not interpreted as command qualifiers, so you don't");
H("need quotes around a Unix file name. Thus");
H("");
H(" bash$ ./metamath /tmp/set.mm");
H("");
H("and");
H("");
H(" bash$ ./metamath \"read '/tmp/set.mm'\"");
H("");
H("are equivalent.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SHOW MEMORY");
H("Syntax: SHOW MEMORY");
H("");
H("This command shows the available memory left. It is not meaningful");
H("on modern machines with virtual memory.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SHOW SETTINGS");
H("Syntax: SHOW SETTINGS");
H("");
H("This command shows the state of various parameters.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SHOW ELAPSED_TIME");
H("Syntax: SHOW ELAPSED_TIME");
H("");
H("This command shows the time elapsed in the session and from any");
H("previous use of SHOW ELAPSED_TIME.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SHOW LABELS");
H("Syntax: SHOW LABELS <label-match> [/ ALL] [/ LINEAR]");
H("");
H("This command shows the labels of $a and $p statements that match");
H("<label-match>. <label-match> may contain * and ? wildcard characters;");
H("see HELP SEARCH for wildcard matching rules.");
H("");
H("Optional qualifier:");
H(" / ALL - Include matches for $e and $f statement labels.");
H(" / LINEAR - Display only one label per line. This can be useful for");
H(" building scripts in conjunction with the TOOLS utility.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SHOW DISCOURAGED");
H("Syntax: SHOW DISCOURAGED");
H("");
H("This command shows the usage and proof statistics for statements with");
H("\"(Proof modification is discouraged.)\" and \"(New usage is");
H("discouraged.)\" markup tags in their description comments. The output");
H("is intended to be used by scripts that compare a modified .mm file");
H("to a previous version.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SHOW SOURCE");
H("Syntax: SHOW SOURCE <label>");
H("");
H("This command shows the ASCII source code associated with a statement.");
H("Normally you should use SHOW STATEMENT for a more meaningful display,");
H("but SHOW SOURCE can be used to see statements with multiple comments");
H("and to see the exact content of the Metamath database.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SHOW STATEMENT");
/* 14-Sep-2010 nm Added OLD_TEX */
H(
"Syntax: SHOW STATEMENT <label-match> [/ COMMENT] [/ FULL] [/ TEX]");
H(" [/ OLD_TEX] [/ HTML] [/ ALT_HTML] [/ BRIEF_HTML]");
H(" [/ BRIEF_ALT_HTML] [/ NO_VERSIONING] [/ MNEMONICS]");
H("");
H("This command provides information about a statement. Only statements");
H("that have labels ($f, $e, $a, and $p) may be specified. <label-match>");
H("may contain * and ? wildcard characters; see HELP SEARCH for wildcard");
H("matching rules.");
H("");
H("In Proof Assistant mode (MM-PA prompt), the symbol \"=\" is a synomym");
H("for the label of the statement being proved. Thus SHOW STATEMENT = will");
H("display the statement being proved.");
H("");
H("By default, only the statement and its $e hypotheses are shown, and if");
H("the label has wildcards, only $a and $p statements are shown.");
H("");
H("Optional qualifiers (only one qualifier at a time is allowed):");
H(" / COMMENT - This qualifier includes the comment that immediately");
H(" precedes the statement.");
H(" / FULL - Show complete information about each statement, and show all");
H(" statements matching <label> (including $e and $f statements).");
H(" / TEX - This qualifier will write the statement information to the");
H(" LaTeX file previously opened with OPEN TEX.");
/* 14-Sep-2010 nm Added OLD_TEX */
H(" / OLD_TEX - Same as / TEX, except that LaTeX macros are used to fit");
H(" equations into line. This mode is obsolete and will be");
H(" removed eventually.");
H(" / HTML - This qualifier invokes a special mode of SHOW STATEMENT which");
H(" creates a Web page for the statement. It may not be used with");
H(" any other qualifier. See HELP HTML for more information.");
H(" / ALT_HTML, / BRIEF_HTML, / BRIEF_ALT_HTML - See HELP HTML for more");
H(" information on these.");
H(" / NO_VERSIONING - When used with / HTML or the 3 HTML qualifiers");
H(" above, a backup file suffixed with ~1 is not created (i.e. the");
H(" previous version is overwritten).");
H(" / TIME - When used with / HTML or the 3 HTML qualifiers, prints");
H(" the run time used by each statement.");
/* 12-May-2009 nm Added MNEMONICS */
H(" / MNEMONICS - Produces the output file mnemosyne.txt for use with");
H(" Mnemosyne http://www.mnemosyne-proj.org/principles.php. Should");
H(" not be used with any other qualifier.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SHOW PROOF");
H("Syntax: SHOW PROOF <label-match> [<qualifiers (see below)>]");
H("");
H("This command displays the proof of the specified $p statement various");
H("formats. The <label-match> may contain \"*\" (0-or-more-character match) and");
H("\"?\" (single-character match) wildcard characters to match multiple");
H("statements. See HELP SEARCH for other label matching conventions.");
H("Without any qualifiers, only the logical steps will be shown (i.e.");
H("syntax construction steps will be omitted), in indented format.");
H("");
H("Note that a compressed proof will have references to repeated parts of");
H("the proof with \"local labels\" prefixed with \"@\". To show all steps");
H("in the original RPN proof, you must SAVE PROOF <label-match> / NORMAL before");
H("using SHOW PROOF.");
H("");
H("Most of the time, you will use");
H(" SHOW PROOF <label-match>");
H("to see just the proof steps corresponding to logical deduction.");
H("");
H("Optional qualifiers:");
H(" / ESSENTIAL - the proof tree is trimmed of all $f hypotheses before");
H(" being displayed. (This is the default, and it is redundant to");
H(" specify it.)");
H(" / ALL - the proof tree is not trimmed of all $f hypotheses before");
H(" being displayed. / ESSENTIAL and / ALL are mutually exclusive.");
H(" / FROM_STEP <step> - the display starts at the specified step. If");
H(" this qualifier is omitted, the display starts at the first step.");
H(" / TO_STEP <step> - the display ends at the specified step. If this");
H(" qualifier is omitted, the display ends at the last step.");
H(" / DEPTH <number> - Only steps at less than the specified proof");
H(" tree depth are displayed. Useful for obtaining an overview of");
H(" the proof.");
H(" / REVERSE - the steps are displayed in reverse order.");
H(" / RENUMBER - when used with / ESSENTIAL, the steps are renumbered");
H(" to correspond only to the essential steps.");
H(" / TEX - the proof is converted to LaTeX and stored in the file opened");
H(" with OPEN TEX. Tip: SET WIDTH 120 (or so) to to fit equations");
H(" to LaTeX line. Then use SHOW PROOF / TEX / LEMMON / RENUMBER.");
H(" / OLD_TEX - same as TEX but uses macros to fit line. Obsolete and");
H(" will be removed eventually.");
H(" / LEMMON - The proof is displayed in a non-indented format known");
H(" as Lemmon style, with explicit previous step number references.");
H(" If this qualifier is omitted, steps are indented in a tree format.");
H(" / START_COLUMN <number> - Overrides the default column at which");
H(" the formula display starts in a Lemmon style display. Affects");
H(" only displays using the / LEMMON qualifier.");
H(" / NO_REPEATED_STEPS - When a proof step is identical to an earlier");
H(" step, it will not be repeated. Instead, a reference to it will be");
H(" changed to a reference to the earlier step. In particular,");
H(" SHOW PROOF <label-match> / LEMMON / RENUMBER / NO_REPEATED_STEPS");
H(" will have the same proof step numbering as the web page proof");
H(" generated by SHOW STATEMENT <label-match> / HTML, rather than");
H(" the proof step numbering of the indented format");
H(" SHOW PROOF <label-match> / RENUMBER. This qualifier affects only");
H(" displays also using the / LEMMON qualifier.");
H(" / STATEMENT_SUMMARY - Summarizes all statements (like a brief SHOW");
H(" STATEMENT) used by the proof. May not be used with any other");
H(" qualifier except / ESSENTIAL.");
H(" / SIZE - Shows size of the proof in the source. The size depends on");
H(" how it was last SAVEd (compressed or normal).");
H(" / DETAILED_STEP <step> - Shows the details of what is happening at");
H(" a specific proof step. May not be used with any other qualifier.");
H(" / NORMAL, / COMPRESSED, / EXPLICIT, / PACKED, / FAST,");
H(" / OLD_COMPRESSION - These qualifiers are the same as for");
H(" SAVE PROOF except that the proof is displayed on the screen in");
H(" a format suitable for manual inclusion in a source file. See");
H(" HELP SAVE PROOF.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP MIDI");
H("Syntax: MIDI <label> [/ PARAMETER \"<parameter string>\"]");
H("");
H("This will create a MIDI sound file for the proof of <label>, where <label>");
H("is one of the $p statement labels shown with SHOW LABELS. The <label> may");
H("contain \"*\" (0-or-more-character match) and \"?\" (single-character");
H("match) wildcard characters to match multiple statements. For each matched");
H("label, a file will be created called <label>.txt which is a MIDI source");
H("file that can be converted to a MIDI binary file with the \"t2mf\" utility");
H("that can be obtained at:");
H(" http://www.hitsquad.com/smm/programs/mf2t/download.shtml");
H("Note: the MS-DOS version t2mf.exe only handles old-style 8.3 file names,");
H("so files such as pm2.11.txt are rejected and must be renamed to");
H("e.g. pm2_11.txt.");
H("");
H("The parameters are:");
H("");
H(" f = make the tempo fast (default is slow).");
H(" m = make the tempo medium (default is slow).");
H(" Both \"f\" and \"m\" should not be specified simultaneously.");
H(" s = syncopate the melody by silencing repeated notes, using");
H(" a method selected by whether the \"h\" parameter below is also");
H(" present (default is no syncopation).");
H(" h = allow syncopation to hesitate i.e. all notes in a");
H(" sequence of repeated notes are silenced except the first (default");
H(" is no hesitation, which means that every other note in a repeated");
H(" sequence is silenced - this makes it sound slightly more rhythmic).");
H(" The \"h\" parameter is meaningful only if the \"s\" parameter above");
H(" is also present.");
H(" w = use only the white keys on the piano keyboard (default");
H(" is potentially to use all keys).");
H(" b = use only the black keys on the piano keyboard (default");
H(" is all keys). Both \"w\" and \"b\" should not be specified");
H(" simultaneously.");
H(" i = use an increment of one keyboard note per proof");
H(" indentation level. The default is to use an automatic increment of");
H(" up to four notes per level based on the dynamic range of the whole");
H(" song.");
H("");
H("Quotes around the parameter string are optional if it has no spaces.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SHOW NEW_PROOF");
H("Syntax: SHOW NEW_PROOF [<qualifiers (see below)]");
H("");
H("This command (available only in Proof Assistant mode) displays the proof");
H("in progress. It is identical to the SHOW PROOF command, except that the");
H("statement is not specified (since it is the statement being proved) and");
H("following qualifiers are not available:");
H(" / STATEMENT_SUMMARY");
H(" / DETAILED_STEP");
H(" / FAST");
H("");
H("Also, the following additional qualifiers are available:");
H(" / UNKNOWN - Shows only steps that have no statement assigned.");
H(" / NOT_UNIFIED - Shows only steps that have not been unified.");
H("");
H("Note that / ALL, / DEPTH, / UNKNOWN, and / NOT_UNIFIED may");
H("be used in any combination; each of them effectively filters out (or");
H("\"unfilters\" in the case of / ALL) additional steps from the proof");
H("display.");
H("");
H("See also: SHOW PROOF");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SHOW USAGE");
H("Syntax: SHOW USAGE <label-match> [/ RECURSIVE]");
H("");
H("This command lists the statements whose proofs make direct reference to");
H("the statement(s) specified by <label-match>. <label-match> may contain *");
H("and ? wildcard characters; see HELP SEARCH for wildcard matching rules.");
H("");
H("Optional qualifiers:");
H(" / RECURSIVE - Also include include statements whose proof ultimately");
H(" depend on the statement specified.");
H(" / ALL - Include $e and $f statements. Without / ALL, $e and $f");
H(" statements are excluded when <label-match> contains wildcard");
H(" characters.");
H("");
let(&saveHelpCmd, ""); /* Deallocate memory */
return;
} /* help2 */
/* 18-Jul-2015 nm Split up help2 into help2 and help3 so lcc
optimizer wouldn't overflow */
void help3(vstring helpCmd)
{
/* 5-Sep-2012 nm */
vstring saveHelpCmd = "";
/* help3() may be called with a temporarily allocated argument (left(),
cat(), etc.), and the let()s in the eventual print2() calls will
deallocate and possibly corrupt helpCmd. So, we grab a non-temporarily
allocated copy here. (And after this let(), helpCmd will become invalid
for the same reason.) */
let(&saveHelpCmd, helpCmd);
printHelp = !strcmp(saveHelpCmd, "HELP SHOW TRACE_BACK");
H("Syntax: SHOW TRACE_BACK <label-match> [/ ESSENTIAL] [/ AXIOMS] [/ TREE]");
H(" [/ DEPTH <number>] [/ COUNT_STEPS] [/MATCH <label-match>]");
H(" [/TO <label-match>]");
H("");
H("This command lists all statements that the proof of the $p statement(s)");
H("specified by <label-match> depends on. <label-match> may contain *");
H("and ? wildcard characters; see HELP SEARCH for wildcard matching rules.");
H("");
H("Optional qualifiers:");
H(" / ESSENTIAL - Restrict the trace-back to $e hypotheses of proof");
H(" trees.");
H(" / AXIOMS - List only the axioms that the proof ultimately depends on.");
H(" / TREE - Display the trace-back in an indented tree format.");
H(" / DEPTH - Restrict the / TREE traceback to the specified indentation");
H(" depth.");
H(" / COUNT_STEPS - Counts the number of steps the proof would have if");
H(" fully expanded back to axioms. If / ESSENTIAL is specified,");
H(" expansions of floating hypotheses are not counted. The steps are");
H(" counted based on how the proof is stored (compressed or normal).");
H(" / MATCH <label-match> - include only statements matching <label-match>");
H(" in the output display. Undisplayed statements are still used to");
H(" compute the list. For example, / MATCH ax-* will show set.mm");
H(" axioms but not definitions.");
H(" / TO <label-match> - include only statements that depend on the");
H(" <label-match> statement(s). For example,");
H(" SHOW TRACE_BACK ac6s / TO ax-reg will list all statements");
H(" requiring ax-reg that ac6s depends on. In case there are");
H(" multiple paths from ac6s back to ax-reg, all statements involved");
H(" in all paths are listed.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SEARCH");
H("Syntax: SEARCH <label-match> \"<symbol-match>\" [/ ALL] [/ COMMENTS]");
H(" [/ JOIN]");
H("");
H("This command searches all $a and $p statements matching <label-match>");
H("for occurrences of <symbol-match>.");
H("");
H("A * in <label-match> matches any zero or more characters in a label.");
H("A ? in <label-match> matches any single character. For example,");
H("SEARCH p?4* \"ph <-> ph\" will check statements whose labels have p and 4");
H("in their first and third character positions, and display them when their");
H("math strings contain \"ph <-> ph\".");
H("A ~ in <label-match> divides the match into two labels, <from>~<to>, and");
H("matches statements located in the source file range between <from> and");
H("<to> inclusive; <from> and <to> may not have * or ? wildcards.");
H("If <label-match> is % (percent sign), it will match all statements with");
H("proofs that were changed in the current session; cannot be used with");
H("wildcards.");
H("If <label-match> is = (equals sign), it will match the statement being");
H("proved the Proof Assistant (MM-PA); cannot be used with wildcards.");
H("If <label-match> is #nnn e.g. #1234, it will match the numeric statement");
H("number nnn; primarily useful for debugging purposes; cannot be used with");
H("wildcards.");
H("");
H("A $* in <symbol-match> matches any sequence of zero or more characters");
H("in the statement's math string. A $? in <symbol-match> matches any");
H("single non-space character in the statement's math string. The quotes");
H("surrounding <symbol-match> may be single or double quotes. For example,");
H("SEARCH * 'E. $? A. $? $?$? -> $* E.' using the set.mm database will find");
H("\"E. x A. y ph -> A. y E. x ph\". As this example shows, $? is");
H("particularly useful when you don't know the variable names used in a");
H("theorem of interest.");
H("");
H("Note 1. Multiple wildcard patterns and ranges may be specified");
H("using a comma-separated list for <label-match>, with no spaces around");
H("the commas. Example: SEARCH df-*,ax-ext~ax-ac 'E. x'.");
H("");
H("Note 2. The first and last characters of <label-match>, if they are not");
H("wildcards, will be matched against the first and last characters of the");
H("label. In contrast, <symbol-match> is a substring match, i.e. it has");
H("implicit $* wildcards before and after it.");
H("");
H("Note 3. An \"unofficial\" <symbol-match> feature is that $ and ? can be");
H("used instead of $* and $? for brevity. The drawback is that matching a");
H("math symbol containing a ? character may yield additional unwanted");
H("matches, but this was felt to be a minor nuisance outweighed by the");
H("convenience of this feature. (Note that $ is not a legal math symbol");
H("character, which is the reason for its use in the official $* and $?");
H("wildcards.) The official wildcards are processed before the unofficial");
H("ones, so that $? will not be interpreted as $ followed by ?.");
H("");
H("Optional qualifiers:");
H(" / ALL - Also search $e and $f statements.");
H(" / COMMENTS - Search the comment that immediately precedes each");
H(" label-matched statement for <symbol-match>, instead of searching");
H(" the statement's math string. In this mode, <symbol-match> is an");
H(" arbitrary, non-case-sensitive character string. Wildcards in");
H(" <symbol-match> are not implemented in this mode.");
H(" / JOIN - In the case of a $a or $p statement, prepend its $e");
H(" hypotheses for searching. / JOIN has no effect in / COMMENTS");
H(" mode.");
H("");
H("See the last section of HELP LET for how to handle quotes and special");
H("characters.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SET ECHO");
H("Syntax: SET ECHO ON or SET ECHO OFF");
H("");
H("The SET ECHO ON command will cause command lines to be echoed with any");
H("abbreviations expanded. While learning the Metamath commands, this");
H("feature will show you the exact command that your abbreviated input");
H("corresponds to. This is also useful to assist creating robust command");
H("files (see HELP SUBMIT) from your log file (see HELP OPEN LOG). To make");
H("it easier to extract these lines, \"!\" (which you will discard) is");
H("prepended to each echoed command line.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SET SCROLL");
H("Syntax: SET SCROLL PROMPTED or SET SCROLL CONTINUOUS");
H("");
H("The Metamath command line interface starts off in the PROMPTED mode,");
H("which means that you will prompted to continue or quit after each");
H("screenful of a long listing. In CONTINUOUS mode, long listings will be");
H("scrolled without pausing.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SET WIDTH"); /* 18-Nov-05 nm Revised */
H("Syntax: SET WIDTH <number>");
H("");
H("Metamath assumes the width of your screen is 79 characters. If your");
H("screen is wider or narrower, this command lets you to change the screen");
H("width. A larger width is advantageous for logging proofs to an output");
H("file to be printed on a wide printer. A smaller width may be necessary");
H("on some terminals; in this case, the wrapping of the information");
H("messages may sometimes seem somewhat unnatural, however. In LaTeX, there");
H("is normally a maximum of 61 characters per line with typewriter font.");
H("");
H("Note: The default width is 79 because Windows Command Prompt issues a");
H("spurious blank line after an 80-character line (try it!).");
H("");
H("Note: This command was SET SCREEN_WIDTH prior to Version 0.07.9.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SET HEIGHT"); /* 18-Nov-05 nm New */
H("Syntax: SET HEIGHT <number>");
H("");
H("Metamath assumes your screen height is 24 lines of characters. If your");
H("screen is taller or shorter, this command lets you to change the number");
H("of lines at which the display pauses and prompts you to continue.");
H("");
/* 10-Jul-2015 nm */
printHelp = !strcmp(saveHelpCmd, "HELP SET DISCOURAGEMENT");
H("Syntax: SET DISCOURAGEMENT OFF or SET DISCOURAGEMENT ON");
H("");
H("By default this is set to ON, which means that statements whose");
H("description comments have the markup tags \"(New usage is discouraged.)\"");
H("or \"(Proof modification is discouraged.)\" will be blocked from usage");
H("or proof modification. When this setting is OFF, those actions are no");
H("longer blocked. This setting is intended only for the convenience of");
H("advanced users who are intimately familiar with the database, for use");
H("when maintaining \"discouraged\" statements. SHOW SETTINGS will show you");
H("the current value.");
H("");
/* 14-May-2017 nm */
printHelp = !strcmp(saveHelpCmd, "HELP SET CONTRIBUTOR");
H("Syntax: SET CONTRIBUTOR <name>");
H("");
H("Specify the contributor name for new \"(Contributed by...\" comment");
H("markup added by SAVE PROOF or SAVE NEW_PROOF. Use quotes (' or \")");
H("around <name> if it contains spaces. The current contributor is");
H("displayed by SHOW SETTINGS.");
H("");
/* 31-Dec-2017 nm */
printHelp = !strcmp(saveHelpCmd, "HELP SET ROOT_DIRECTORY");
H("Syntax: SET ROOT_DIRECTORY <directory path>");
H("");
H("Specify the directory path (relative to the working directory i.e. the");
H("directory from which the Metamath program was launched) which will be");
H("prepended to READ, WRITE SOURCE, and files included with $[...$].");
H("Enclose <directory path> in single or double quotes if the path contains");
H("\"/\". A trailing \"/\" will be added automatically if missing. The");
H("current directory path is displayed by SHOW SETTINGS.");
H("");
H("Use a quoted space (' ' or \" \") for <directory path> if you want to");
H("reset it to be the working directory.");
printHelp = !strcmp(saveHelpCmd, "HELP SET UNIFICATION_TIMEOUT");
H("Syntax: SET UNIFICATION_TIMEOUT <number>");
H("");
H("(This command affects the Proof Assistant only.)");
H("");
H("Sometimes the Proof Assistant will inform you that a unification timeout");
H("occurred. This may happen when you try to UNIFY formulas with many");
H("unknown variables, since the time to compute unifications may grow");
H("exponentially with the number of variables. If you want Metamath to try");
H("harder (and you're willing to wait longer) you may increase this");
H("parameter. SHOW SETTINGS will show you the current value.");
H("");
H("Often, a better solution to resolve a unification timeout is to manually");
H("assign some or all of the unknowns (see HELP LET) then try to unify");
H("again.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SET EMPTY_SUBSTITUTION");
H("Syntax: SET EMPTY_SUBSTITUTION ON or SET EMPTY_SUBSTITUTION OFF");
H("");
H("(This command affects the Proof Assistant only. It may be issued");
H("outside of the Proof Assistant.)");
H("");
H("The Metamath language allows variables to be substituted with empty");
H("symbol sequences. However, in most formal systems this will never happen");
H("in a valid proof. Allowing for this possibility increases the likelihood");
H("of ambiguous unifications during proof creation. The default is that");
H("empty substitutions are not allowed; for formal systems requiring them,");
H("you must SET EMPTY_SUBSTITUTION ON. Note that empty substitutions are");
H("always permissable in proof verification (VERIFY PROOF...) outside the");
H("Proof Assistant. (See the MIU system in the Metamath book for an example");
H("of a system needing empty substitutions; another example would be a");
H("system that implements a Deduction Rule and in which deductions from");
H("empty assumption lists would be permissable.)");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SET SEARCH_LIMIT");
H("Syntax: SET SEARCH_LIMIT <number>");
H("");
H("(This command affects the Proof Assistant only.)");
H("");
H("This command sets a parameter that determines when the IMPROVE command");
H("in Proof Assistant mode gives up. If you want IMPROVE to search harder,");
H("you may increase it. The SHOW SETTINGS command tells you its current");
H("value.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SET JEREMY_HENTY_FILTER");
H("Syntax: SET JEREMY_HENTY_FILTER ON or SET JEREMY_HENTY_FILTER OFF");
H("");
H("(This command affects the Proof Assistant only.)");
H("");
H("The \"Henty filter\" is an ingenious algorithm suggested by Jeremy Henty");
H("that reduces the number of ambiguous unifications by eliminating");
H("\"equivalent\" ones in a sense defined by Henty. Normally this filter");
H("is ON, and the only reason to turn it off would be for debugging.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP VERIFY PROOF");
H("Syntax: VERIFY PROOF <label-match> [/ SYNTAX_ONLY]");
H("");
H("This command verifies the proofs of the specified statements.");
H("<label-match> may contain * and ? wildcard characters to verify more than");
H("one proof; for example \"abc?def*\" will match all labels beginning with");
H("\"abc\" followed by any single character followed by \"def\".");
H("VERIFY PROOF * will verify all proofs in the database.");
H("See HELP SEARCH for complete wildcard matching rules.");
H("");
H("Optional qualifier:");
H(" / SYNTAX_ONLY - This qualifier will perform a check of syntax and RPN");
H(" stack violations only. It will not verify that the proof is");
H(" correct.");
H("");
H("Note: READ, followed by VERIFY PROOF *, will ensure the database is free");
H("from errors in Metamath language but will not check the markup language");
H("in comments. See HELP VERIFY MARKUP.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP VERIFY MARKUP");
H("Syntax: VERIFY MARKUP <label-match> [/ DATE_SKIP] [/ TOP_DATE_SKIP]");
H(" [/ FILE_SKIP] [/VERBOSE]");
H("");
H("This command checks comment markup and other informal conventions we have");
H("adopted. It error-checks the latexdef, htmldef, and althtmldef statements");
H("in the $t statement of a Metamath source file. It error-checks any `...`,");
H("~ <label>, and [bibref] markups in statement descriptions. It checks that");
H("$p and $a statements have the same content when their labels start with");
H("\"ax\" and \"ax-\" respectively but are otherwise identical, for example");
H("ax4 and ax-4. It verifies the date consistency of \"(Contributed by...)\",");
H("\"(Revised by...)\", and \"(Proof shortened by...)\" tags in the comment");
H("above each $a and $p statement. See HELP SEARCH for <label-match> rules.");
H("");
H("Optional qualifiers:");
H(" / DATE_SKIP - This qualifier will skip date consistency checking,");
H(" which is usually not required for databases other than set.mm");
H(" / TOP_DATE_SKIP - This qualifier will check date consistency except");
H(" that the version date at the top of the database file will not");
H(" be checked. Only one of / DATE_SKIP and / TOP_DATE_SKIP may be");
H(" specified.");
H(" / FILE_SKIP - This qualifier will skip checks that require");
H(" external files to be present, such as checking GIF existence and");
H(" bibliographic links to mmset.html or equivalent. It is useful");
H(" for doing a quick check from a directory without these files");
H(" / VERBOSE - Provides more information. Currently it provides a list");
H(" of axXXX vs. ax-XXX matches.");
H("");
H("See also HELP LANGUAGE, HELP HTML, HELP WRITE THEOREM_LIST, and");
H("HELP SET DISCOURAGEMENT for more details on the markup syntax.");
H("See the 11-May-2016 (\"is discouraged\"), 14-May-2017 (date format), and");
H("21-Dec-2017 (file inclusion) entries in");
H("http://us.metamath.org/mpeuni/mmnotes.txt for further details on several");
H("kinds of markup. See HELP WRITE THEOREM_LIST for format of section headers.");
H("");
H("For help with modularization tags such as \"$( Begin $[ set-header.mm $] $)\",");
H("see the 21-Dec-2017 entry in http://us.metamath.org/mpeuni/mmnotes.txt .");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SUBMIT");
H("Syntax: SUBMIT <filename> [/ SILENT]");
H("");
H("This command causes further command lines to be taken from the specified");
H("command file. Note that any line beginning with an exclamation point (!)");
H("is treated as a comment (i.e. ignored). Also note that the scrolling");
H("of the screen output is continuous, so you may want to open a log file");
H("(see HELP OPEN LOG) to record the results that fly by on the screen.");
H("After the lines in the command file are exhausted, Metamath returns to");
H("its normal user interface mode.");
H("");
H("SUBMIT commands can occur inside of a SUBMIT command file, up to 10 levels");
H("deep (determined by MAX_COMMAND_FILE_NESTING in mminou.h.");
H("");
H("Optional qualifier:");
H(" / SILENT - This qualifier suppresses the screen output of the SUBMIT");
H(" command. The output will still be recorded in any log file that");
H(" has been opened with OPEN LOG (or is opened inside the command");
H(" file itself). The screen output of any operating system commands");
H(" inside the command file (see HELP SYSTEM) is not suppressed.");
printHelp = !strcmp(saveHelpCmd, "HELP SYSTEM");
H("A line enclosed in single or double quotes will be executed by your");
H("computer's operating system, if it has such a feature. For example, on a");
H("GNU/Linux system,");
H(" MM> 'ls | less -EX'");
H("will list disk directory contents. Note that this feature will not work");
H("on the pre-OSX Macintosh, which does not have a command line interface.");
H("");
H("For your convenience, the trailing quote is optional, for example:");
H(" MM> 'ls | less -EX");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP MM-PA");
H("See HELP PROOF_ASSISTANT");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP MORE");
H("Syntax: MORE <filename>");
H("");
H("This command will type (i.e. display) the contents of an ASCII file on");
H("your screen. (This command is provided for convenience but is not very");
H("powerful. See HELP SYSTEM to invoke your operating system's command to");
H("do this, such as \"less -EX\" in Linux.)");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP FILE SEARCH");
H("Syntax: FILE SEARCH <filename> \"<search string>\" [/ FROM_LINE");
H(" <number>] [/ TO_LINE <number>]");
H("");
H("This command will search an ASCII file for the specified string in");
H("quotes, within an optional range of line numbers, and display the result");
H("on your screen. The search is case-insensitive. (This command is");
H("deprecated. See HELP SYSTEM to invoke your operating system's");
H("equivalent command, such as \"grep\" in Linux.)");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP PROVE");
H("Syntax: PROVE <label> [/ OVERRIDE]");
H("");
H("This command will enter the Proof Assistant, which will allow you to");
H("create or edit the proof of the specified statement.");
H("");
H("Optional qualifier:");
H(" / OVERRIDE - By default, PROVE will refuse to enter the Proof");
H(" Assistant if \"(Proof modification is discouraged.)\" is present");
H(" in the statement's description comment. This qualifier will");
H(" allow the Proof Assistant to be entered.");
H("");
H("See also: HELP PROOF_ASSISTANT and HELP EXIT");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP PROOF_ASSISTANT");
H("Before using the Proof Assistant, you must add a $p to your source file");
H("(using a text editor) containing the statement you want to prove. Its");
H("proof should consist of a single ?, meaning \"unknown step.\" Example:");
H(" eqid $p x = x $= ? $.");
H("");
H("To enter the Proof Assistant, type PROVE <label>, e.g. PROVE eqid.");
H("Metamath will respond with the MM-PA> prompt.");
H("");
H("Proofs are created working backwards from the statement being proved,");
H("primarily using a series of ASSIGN commands. A proof is complete when");
H("all steps are assigned to statements and all steps are unified and");
H("completely known. During the creation of a proof, Metamath will allow");
H("only operations that are legal based on what is known up to that point.");
H("For example, it will not allow an ASSIGN of a statement that cannot be");
H("unified with the unknown proof step being assigned.");
H("");
H("IMPORTANT: You should figure out your first few proofs completely and");
H("write them down by hand, before using the Proof Assistant. Otherwise you");
H("will become extremely frustrated. The Proof Assistant is NOT a tool to");
H("help you discover proofs. It is just a tool to help you add them to the");
H("database. For a tutorial read Section 2.4 of the Metamath book. To");
H("practice using the Proof Assistant, you may want to PROVE an existing");
H("theorem, then delete all steps with DELETE ALL, then re-create it with");
H("the Proof Assistant while looking at its proof display (before deletion).");
H("");
H("The commands available to help you create a proof are the following.");
H("See the help for the individual commands for more detail.");
H(" SHOW NEW_PROOF [/ ALL,...] - Displays the proof in progress.");
H(" You will use this command a lot; see HELP SHOW NEW_PROOF to");
H(" become familiar with its qualifiers. The qualifiers / UNKNOWN");
H(" and / NOT_UNIFIED are useful for seeing the work remaining to be");
H(" done. The combination / ALL / UNKNOWN is useful identifying");
H(" dummy variables that must be assigned, or attempts to use illegal");
H(" syntax, when IMPROVE ALL is unable to complete the syntax");
H(" constructions. Unknown variables are shown as $1, $2,...");
H(" ASSIGN <step> <label> - Assigns an unknown step with the statement");
H(" specified by <label>. This will normally be your most frequently");
H(" used command for creating proofs. The usual proof entry process");
H(" consists of successively ASSIGNing labels to unknown steps shown");
H(" by SHOW NEW_PROOF / UNKNOWN.");
H(" LET VARIABLE <variable> = \"<symbol sequence>\" - Forces a symbol");
H(" sequence to replace an unknown variable in a proof. It is useful");
H(" for helping difficult unifications, and is necessary when you");
H(" have dummy variables that must be specified.");
H(" LET STEP <step> = \"<symbol sequence>\" - Forces a symbol sequence");
H(" to replace the contents of a proof step, provided it can be");
H(" unified with the existing step contents. (Rarely useful.)");
H(" UNIFY STEP <step> (or UNIFY ALL) - Unifies the source and target of");
H(" a step. If you specify a specific step, you will be prompted");
H(" to select among the unifications that are possible. If you");
H(" specify ALL, only those steps with unique unifications will be");
H(" unified. UNIFY ALL / INTERACTIVE goes through all non-unified");
H(" steps.");
H(" INITIALIZE <step> (or ALL) - De-unifies the target and source of");
H(" a step (or all steps), as well as the hypotheses of the source,");
H(" and makes all variables in the source unknown. Useful after");
H(" an ASSIGN or LET mistake resulted in incorrect unifications.");
H(" DELETE <step> (or ALL or FLOATING_HYPOTHESES) - Deletes the specified");
H(" step(s). DELETE FLOATING_HYPOTHESES then INITIALIZE ALL then");
H(" UNIFY ALL / INTERACTIVE is useful for recovering from mistakes");
H(" where incorrect unifications assigned wrong math symbol strings to");
H(" variables.");
H(" IMPROVE <step> (or ALL) - Automatically creates a proof for steps");
H(" (with no unknown variables) whose proof requires no statements");
H(" with $e hypotheses. Useful for filling in proofs of $f");
H(" hypotheses. The / DEPTH qualifier will also try statements");
H(" whose $e hypotheses contain no new variables. WARNING: Save your");
H(" work (SAVE NEW_PROOF, WRITE SOURCE) before using / DEPTH = 2 or");
H(" greater, since the search time grows exponentially and may never");
H(" terminate in a reasonable time, and you cannot interrupt the");
H(" search. I have rarely found / DEPTH = 3 or greater to be useful.");
H(" SAVE NEW_PROOF - Saves the proof in progress internally in the");
H(" database buffer. To save it permanently, use WRITE SOURCE after");
H(" SAVE NEW_PROOF. To revert to the last SAVE NEW_PROOF,");
H(" EXIT / FORCE from the Proof Assistant then re-enter the Proof");
H(" Assistant.");
H(" SHOW NEW_PROOF / COMPRESSED - Displays the proof in progress on the");
H(" screen in a format that can be copied and pasted into the");
H(" database source, as an alternative to a SAVE NEW_PROOF.");
H(" MATCH STEP <step> (or MATCH ALL) - Shows what statements are");
H(" possibilities for the ASSIGN statement. (This command is not very");
H(" useful in its present form and hopefully will be improved");
H(" eventually. In the meantime, use the SEARCH statement for");
H(" candidates matching specific math token combinations.)");
H(" MINIMIZE_WITH - After a proof is complete, this command will attempt");
H(" to match other database theorems to the proof to see if the proof");
H(" size can be reduced as a result.");
H(" UNDO - Undo the effect of a proof-changing command (all but the SHOW");
H(" and SAVE commands above).");
H(" REDO - Reverse the previous UNDO.");
H("");
H("The following commands set parameters that may be relevant to your proof:");
H(" SET UNIFICATION_TIMEOUT");
H(" SET SEARCH_LIMIT");
H(" SET EMPTY_SUBSTITUTION - note that default is OFF (contrary to book)");
H("");
H("Type EXIT to exit the MM-PA> prompt and get back to the MM> prompt.");
H("Another EXIT will then get you out of Metamath.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP UNDO");
H("Syntax: UNDO");
H("");
H("This command, available in the Proof Assistant only, allows any command");
H("(such as ASSIGN, DELETE, IMPROVE) that affects the proof to be reversed.");
H("See also HELP REDO and HELP SET UNDO.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP REDO");
H("Syntax: REDO");
H("");
H("This command, available in the Proof Assistant only, reverses the");
H("effect of the last UNDO command. Note that REDO can be issued only");
H("if no proof-changing commands (such as ASSIGN, DELETE, IMPROVE)");
H("were issued after the last UNDO. A sequence of REDOs will reverse as");
H("many UNDOs as were issued since the last proof-changing command.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP SET UNDO"); /* 1-Nov-2013 nm */
H("Syntax: SET UNDO <number>");
H("");
H("(This command affects the Proof Assistant only.)");
H("");
H("This command changes the maximum number of UNDOs. The current maximum");
H("can be seen with SHOW SETTINGS. Making it larger uses more memory,");
H("especially for large proofs. See also HELP UNDO.");
H("");
H("If this command is issued while inside of the Proof Assistant, the");
H("UNDO stack is reset (i.e. previous possible UNDOs will be lost).");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP ASSIGN");
H("Syntax: ASSIGN <step> <label> [/ NO_UNIFY] [/ OVERRIDE]");
H(" ASSIGN FIRST <label> [/ NO_UNIFY] [/ OVERRIDE]"); /* 11-Dec-05 nm */
H(" ASSIGN LAST <label> [/ NO_UNIFY] [/ OVERRIDE]");
H("");
H("This command, available in the Proof Assistant only, assigns an unknown");
H("step (one with ? in the SHOW NEW_PROOF listing) with the statement");
H("specified by <label>. The assignment will not be allowed if the");
H("statement cannot be unified with the step.");
H("");
H("If <step> starts with \"-\", the -<step>th from last unknown step,");
H("as shown by SHOW NEW_PROOF / UNKNOWN, will be used. ASSIGN -0 will");
H("assign the last unknown step, ASSIGN -1 <label> will assign the");
H("penultimate unknown step, etc. If <step> starts with \"+\", the <step>th");
H("from the first unknown step will be used. Otherwise, when the step is");
H("a positive integer (with no \"+\" sign), ASSIGN assumes it is the actual");
H("step number shown by SHOW NEW_PROOF / UNKNOWN.");
H("");
H("ASSIGN FIRST and ASSIGN LAST mean ASSIGN +0 and ASSIGN -0 respectively,");
H("in other words the first and last steps shown by SHOW NEW_PROOF / UNKNOWN.");
H("");
H("Optional qualifiers:");
H(" / NO_UNIFY - do not prompt user to select a unification if there is");
H(" more than one possibility. This is useful for noninteractive");
H(" command files. Later, the user can UNIFY ALL / INTERACTIVE.");
H(" (The assignment will still be automatically unified if there is");
H(" only one possibility.)");
H(" / OVERRIDE - By default, ASSIGN will refuse to assign a statement");
H(" if \"(New usage is discouraged.)\" is present in the statement's");
H(" description comment. This qualifier will allow the assignment.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP REPLACE");
H("Syntax: REPLACE <step> <label> [/ OVERRIDE]");
H("Syntax: REPLACE FIRST <label> [/ OVERRIDE]");
H("Syntax: REPLACE LAST <label> [/ OVERRIDE]");
H("");
H("This command, available in the Proof Assistant only, replaces the");
H("current subproof ending at <step> with a new complete subproof (if one");
H("can be found) ending with statement <label>. The replacement will be");
H("done only if complete subproofs can be found that match all of the");
H("hypotheses of <label>. REPLACE is equivalent to IMPROVE with the");
H("qualifiers / 3 / DEPTH 1 / SUBPROOFS (see HELP IMPROVE), except that");
H("it considers only statement <label> rather than scanning all preceding");
H("statements in the database, and it does somewhat more aggressive");
H("guessing of assignments to work ($nn) variables.");
H("");
H("REPLACE will also assign a complete subproof to a currently unknown");
H("(unassigned) step if a complete subproof can be found. In many cases,");
H("REPLACE provides an alternative to ASSIGN (with the same command syntax)");
H("that will fill in more missing steps when it is successful. It is often");
H("useful to try REPLACE first and, if not successful, revert to ASSIGN.");
H("Note that REPLACE may take a long time to run compared to ASSIGN.");
H("");
H("Currently, REPLACE does not allow a $e or $f statement for <label>. Use");
H("ASSIGN instead. (These may be allowed in a future version.)");
H("");
H("Occasionally, REPLACE may be too aggressive in guessing assignments to");
H("work ($nn) variables, and a message with recovery instructions is");
H("provided when this could be the case. Recovery can also be attempted with");
H("DELETE FLOATING_HYPOTHESES then INITIALIZE ALL then");
H("UNIFY ALL / INTERACTIVE; this will usually work and will salvage the");
H("subproof found by REPLACE. (The too-aggressive guessing behavior may be");
H("improved in a future version.)");
H("");
H("If <step> starts with \"-\", the -<step>th from last unknown step,");
H("as shown by SHOW NEW_PROOF / UNKNOWN, will be used. REPLACE -0 will");
H("assign the last unknown step, REPLACE -1 <label> will assign the");
H("penultimate unknown step, etc. If <step> starts with \"+\", the <step>th");
H("from the first unknown step will be used. Otherwise, when the step is");
H("a positive integer (with no \"+\" sign), REPLACE assumes it is the actual");
H("step number shown by SHOW NEW_PROOF (and can be used whether the step is");
H("known or not).");
H("");
H("REPLACE FIRST and REPLACE LAST mean REPLACE +0 and REPLACE -0");
H("respectively, in other words the first and last steps shown by");
H("SHOW NEW_PROOF / UNKNOWN.");
H("");
H("Optional qualifier:");
H(" / OVERRIDE - By default, REPLACE will refuse to assign a statement");
H(" if \"(New usage is discouraged.)\" is present in the statement's");
H(" description comment. This qualifier will allow the assignment.");
H("");
printHelp = !strcmp(saveHelpCmd, "HELP MATCH");
H("Syntax: MATCH STEP <step> [/ MAX_ESSENTIAL_HYP <number>]");
H(" or: MATCH ALL [/ ESSENTIAL_ONLY] [/ MAX_ESSENTIAL_HYP <number>]");
H("");
H("This command, available in the Proof Assistant only, shows what");
H("statements can be unified with the specified step(s).");
H("");
H("Optional qualifiers:");
H(" / MAX_ESSENTIAL_HYP <number> - filters out of the list any statements");
H(" with more than the specified number of $e hypotheses");