Interactions of ConstantMappings with Obsoleteness

For MFA-like conditions, we want to make an additional assumption on ObsoletenessCondition that we did not demand before. Namely, we want that the condition propagates_under_constant_mapping, meaning that of a trigger is obsolete for a fact set, then the version of the trigger where a ConstantMapping is composed with the original substitution is also obsolete for the version of the fact set where the ConstantMapping was applied. At least this shall be the case if the ConstantMapping does not touch the head constants of the rule in the trigger.

We briefly demonstrate that this property holds for both SkolemObsoleteness and RestrictedObsoleteness.

def ObsoletenessCondition.propagates_under_constant_mapping {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (obs : ObsoletenessCondition sig) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem SkolemObsoleteness.propagates_under_constant_mapping {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] : (SkolemObsoleteness sig).propagates_under_constant_mapping

theorem RestrictedObsoleteness.propagates_under_constant_mapping {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] : (RestrictedObsoleteness sig).propagates_under_constant_mapping