Refined PVS Rule (after additional examples)

Plausible upper bound IF

Plausible lower bound IF

THEN