Open
Description
I've been developing a proof, one of its steps would not unify and I finally realized that I had a syntax error in definition. Original .mm file:
$( We build upon all known math theory. $)
$[ metamath/set.mm $]
$( A sequence of type ~ S has type ` Word S `. $)
$( Extend class notation to include the set of increasing sequences. $)
$c UpWord $.
cupword $a class UpWord S $.
${
df-upword $a |- UpWord S = { w | ( w e. Word S /\ A. k e. ( 0 ..^ ( # ` w - 1 ) ) ( w ` k < w ` ( k + 1 ) ) ) } $.
upwordnul $p |- (/) e. UpWord S $= $.
$}
(the syntax error itself: # \ w` should've been surrounded by parentheses)
After developing most of the proof, I noticed the problem and tried to locally rewrite the definition. The bug appeared.
MM-PA> sh new /lemmon
17 wrd0 $p |- (/) e. Word S
21 elsb1 $p |- ( [ (/) / $35 ] $35 e. Word S <-> (/) e. Word S )
22 17,21 mpbir $p |- [ (/) / $35 ] $35 e. Word S
50 ? $? |- ( $35 = (/) -> ( # ` $35 - 1 ) <_ 0 )
64 nn0ssz $p |- NN0 C_ ZZ
68 ? $? |- ( $35 = (/) -> $35 e. Word S )
69 ? $? |- ( $35 e. Word S -> # ` $35 e. NN0 )
70 68,69 syl $p |- ( $35 = (/) -> # ` $35 e. NN0 )
71 64,70 sselid $p |- ( $35 = (/) -> # ` $35 e. ZZ )
73 1zzd $p |- ( $35 = (/) -> 1 e. ZZ )
74 71,73 zsubcld $p |- ( $35 = (/) -> ( # ` $35 - 1 ) e. ZZ )
75 0z $p |- 0 e. ZZ
76 74,75 jctil $p |- ( $35 = (/) -> ( 0 e. ZZ /\ ( # ` $35 - 1 ) e. ZZ ) )
79 fzon $p |- ( ( 0 e. ZZ /\ ( # ` $35 - 1 ) e. ZZ ) -> ( ( # ` $35 - 1 ) <_ 0 <-> ( 0 ..^ ( # ` $35 - 1 ) ) = (/) ) )
80 76,79 syl $p |- ( $35 = (/) -> ( ( # ` $35 - 1 ) <_ 0 <-> ( 0 ..^ ( # ` $35 - 1 ) ) = (/) ) )
81 50,80 mpbid $p |- ( $35 = (/) -> ( 0 ..^ ( # ` $35 - 1 ) ) = (/) )
90 neq0 $p |- ( -. ( 0 ..^ ( # ` $35 - 1 ) ) = (/) <-> E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) )
91 90 bicomi $p |- ( E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) <-> -. ( 0 ..^ ( # ` $35 - 1 ) ) = (/) )
92 91 con2bii $p |- ( ( 0 ..^ ( # ` $35 - 1 ) ) = (/) <-> -. E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) )
93 92 biimpi $p |- ( ( 0 ..^ ( # ` $35 - 1 ) ) = (/) -> -. E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) )
94 81,93 syl $p |- ( $35 = (/) -> -. E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) )
97 imnan $p |- ( ( $35 = (/) -> -. E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ) <-> -. ( $35 = (/) /\ E. $110 $110 e. ( 0 ..^ ( # `
$35 - 1 ) ) ) )
98 94,97 mpbi $p |- -. ( $35 = (/) /\ E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) )
99 98 bifal $p |- ( ( $35 = (/) /\ E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ) <-> F. )
100 99 biimpi $p |- ( ( $35 = (/) /\ E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ) -> F. )
102 falim $p |- ( F. -> A. $110 ( $35 ` $110 < $35 ` ( $110 + 1 ) ) )
103 100,102 syl $p |- ( ( $35 = (/) /\ E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ) -> A. $110 ( $35 ` $110 < $35 ` ( $110 + 1 ) ) )
104 103 ex $p |- ( $35 = (/) -> ( E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) -> A. $110 ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) )
108 19.38 $p |- ( ( E. $110 $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) -> A. $110 ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) -> A. $110 ( $110 e. (
0 ..^ ( # ` $35 - 1 ) ) -> ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) )
109 104,108 syl $p |- ( $35 = (/) -> A. $110 ( $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) -> ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) )
113 df-ral $a |- ( A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) <-> A. $110 ( $110 e. ( 0 ..^ ( # ` $35 -
1 ) ) -> ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) )
114 109,113 sylibr $p |- ( $35 = (/) -> A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) )
115 114 ax-gen $a |- A. $35 ( $35 = (/) -> A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) )
119 sb6 $p |- ( [ (/) / $35 ] A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) <-> A. $35 ( $35 = (/) -> A.
$110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) )
120 115,119 mpbir $p |- [ (/) / $35 ] A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) )
121 22,120 pm3.2i $p |- ( [ (/) / $35 ] $35 e. Word S /\ [ (/) / $35 ] A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1
) ) )
126 sban $p |- ( [ (/) / $35 ] ( $35 e. Word S /\ A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) <-> ( [
(/) / $35 ] $35 e. Word S /\ [ (/) / $35 ] A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) )
127 121,126 mpbir $p |- [ (/) / $35 ] ( $35 e. Word S /\ A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) )
131 df-clab $a |- ( (/) e. { $35 | ( $35 e. Word S /\ A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) } <->
[ (/) / $35 ] ( $35 e. Word S /\ A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) )
132 127,131 mpbir $p |- (/) e. { $35 | ( $35 e. Word S /\ A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) }
136 df-upword $a |- UpWord S = { $35 | ( $35 e. Word S /\ A. $110 e. ( 0 ..^ ( # ` $35 - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) }
137 132,136 eleqtrri $p |- (/) e. UpWord S
MM-PA> le st 136
With what math symbol string? $a |- UpWord S = { $35 | ( $35 e. Word S /\ A. $110 e. ( 0 ..^ ( ( # ` $35 ) - 1 ) ) ( $35 ` $110 < $35 ` ( $110 + 1 ) ) ) }
?BUG CHECK: *** DETECTED BUG 1901
To get technical support, please open an issue
(https://github.com/metamath/metamath-exe/issues) with the
detailed command sequence or a command file that reproduces this bug,
along with the source file that was used. See HELP OPEN LOG for help on
recording a session. See HELP SUBMIT for help on command files. Search
for "bug(1901)" in the m*.c source code to find its origin.
If earlier errors were reported, try fixing them first, because they
may occasionally lead to false bug detection
Metadata
Metadata
Assignees
Labels
No labels