Better approximation of boxed contexts

[muenchnerkindl]

Temporal reasoning usually requires assumptions to be "boxed" where a formula F is boxed if it is equivalent with []F. The PM performs a syntactic approximation of when a formula is boxed, but this could be improved. In particular, a formula F is boxed if

• it is of the form []G, for some formula G,
• it is of the form G /\ H where both G and H are boxed,
• it is of the form \A x : G or \A x \in S : G if G is boxed (and S is a constant),
• it is of the form <>G and G is boxed,
• it is of the form WF_x(A) or SF_x(A).

The following is an example of a context that is not recognized as being boxed.

CONSTANT S
VARIABLE x

A(m,n) == TRUE

THEOREM
  ASSUME \A m,n \in S : WF_x(A(m,n))
  PROVE  [](x=x)
<1>1. x = x
  OBVIOUS
<1>. QED
  BY <1>1, PTL  \* fails