You can't use $d to ensure that constants don't appear in a formula. I
don't have all the context needed to understand why you need to do this,
but one way to express it would be to have a predicate "|- ^.-free A" and
have rules like "|- ( ^.-free A -> ( ^.-free B -> ^.-free ( A /\ B ) ) )"
for
In the process of cleaning-up my theorems for possible addition to set.mm I
found a fundamental inconsistency in the definition of my discrete time
operator ^. which is defined in terms of my continuous time operator @.
p@t says evaluate p at time t which is restricted to time the machine
