[opentheory-users] the Unwanted namespace

[Ramana Kumar]

> Unfortunately I can see other ways that terms like these could enter
> the state, such as
>
> appThm (|- (\f. f x) = t) (|- Unwanted.id = u)
>
> followed by betaConv of the LHS at a later point.

So we would need to consider betaConv too...
Anything else?

> I'd really like a scheme that eliminates all occurrences of the
> Unwanted.id constant from a proof, if that was possible. And by this I
> mean that grepping the resulting article for occurrences of the
> "Unwanted" namespace will not turn up any results.

OK.

I think your current treatment of appTerm is fine - it won't fail, and
it removes those occurrences of Unwanted.id from the article file.

So let's consider appThm and betaConv.
These are the general forms I see introducing unwanted terms:

appThm (|- Unwanted.id = f) (|- x = y)
appThm (|- f = Unwanted.id) (|- x = y)
betaConv (|- (\f. t[f x]) Unwanted.id)

What happens if you just change the semantics of all of these commands
to replace any resulting (Unwanted.id t) terms by (t), and also
prevent Unwanted.id from being defined (to stop an obvious soundness
problem)?