I have a strange problem with mmj2's file "PA301.mmp" - anyone have
any idea what's up?
Background:
I'm doing a dry run of the mmj2 "PATutorial" files. However, when I try to
unify (control-U) file PA301.mmp, I get the following error instead of a
unification:
E-PA-0348 Theorem sylClone Step 3: Invalid Ref = 200 on derivation proof step.
Does not specify a valid statement in the Metamath file that was loaded. You
can leave Ref blank to allow Unify to figure it out for you. Proof Text input
reader last position: Source Id: Proof Text Line: 21 Column: 3
The error is on this line:
3:200 |- ( ph -> ( ps -> ch ) )
which refers back to this hypothesis:
h200 |- ( ps -> ch )
That should work, but it doesn't. Changing "3:200" to "3:h200" doesn't work
either
(though that shouldn't be needed).
Anyone else seen this? Full file contents below.
--- David A. Wheeler
=======================================
$( <MM> <PROOF_ASST> THEOREM=sylClone LOC_AFTER=a2i
* Page301.mmp
Have a careful look at the "Step:Hyp:Ref" field at the start of each
proof step below. Notice especially how:
- Hypothesis Step Numbers are prefixed with 'h'
- Step Numbers are not in numeric order(!), but are unique
- Ref Labels are blank
- Trailing ":"s are optional, for your convenience
- Blanks are not permitted inside a "Step:Hyp:Ref" (making things
easier for the programmers)
- the final step "number" is "qed" (also for the convenience of
the programmer...)
OK, now press Ctrl-U and see what happens to the Step:Hyp:Ref fields.
(Use Edit/Undo -- twice -- to retry and look again.)
h1000 |- ( ph -> ps )
h200 |- ( ps -> ch )
h30 |- ( ch -> th )
3:200 |- ( ph -> ( ps -> ch ) )
4:3 |- ( ( ph -> ps ) -> ( ph -> ch ) )
qed:1000,4 |- ( ph -> ch )
*OK, proceed to the next Tutorial page (Page302.mmp)!
$)
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/E1ikeuB-0007Zn-I1%40rmmprod07.runbox.
