While working with some automatically generated proofs I found that top-level disjoint variable restrictions seem to apply also before the $d statement.
In this example metamath-knife --verify complains "Distinct variable violation" on R-id, as if the $d x y $. at the end of the file was active for R-any.
$c term |- R $.
$v x y $.
x-term $f term x $.
y-term $f term y $.
R-any $a |- x R y $.
R-id $p |- x R x $= x-term x-term R-any $.
$( The offending $d may come after multiple declarations $)
$v z $.
z-term $f term z $.
padding-lemma $a |- x R x $.
$d x y $.
metamath-exe accepts the proof. Within a block metamath-knife also respects ordering, after adding ${ before R-any and $} after the $d this example metamath-knife --verify accepts the file.
While working with some automatically generated proofs I found that top-level disjoint variable restrictions seem to apply also before the
$dstatement.In this example
metamath-knife --verifycomplains "Distinct variable violation" onR-id, as if the$d x y $.at the end of the file was active forR-any.metamath-exe accepts the proof. Within a block metamath-knife also respects ordering, after adding
${beforeR-anyand$}after the$dthis examplemetamath-knife --verifyaccepts the file.