Delayed Implication |
INTENTION |
This pattern is applicable if one phenomenon, represented by the formula
,
always depends in the positive case on another phenomenon,
represented by the formula ,
with a maximal time delay
. |
SIGNATURE |
,
,
,
|
FORMAL |
|
NATURAL LANGUAGE |
Whenever
holds continuously for at least
time units, then
eventually within this time span,
is true and remains true at
least as long as
holds. |
Examples |
EXAMPLE 1 |
|
FORMAL |
|
|
NATURAL
LANGUAGE |
Whenever a hazardous condition holds continuously for at least 30 seconds,
the eventually within this time span, the window is closed and remains
closed at least as long as the hazardous condition
continues. |
Theorem Part |
THEOREM SIGNATURE |
,
,
,
|
THEOREM 1 Transitivity |
|
FORMAL |
|
|
EXPLANATION |
This theorem expresses the transitivity of this pattern. |
THEOREM 2 Conclusion
Distributivity over |
|
FORMAL |
|
|
EXPLANATION |
This theorem expresses the distributivity over
of the conclusions of two
instantiations of this pattern. |