Interactions of ConstantMappings with Obsolescence

For MFA-like conditions, we want to make an additional assumption on ObsolescenceCondition 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 SkolemObsolescence and RestrictedObsolescence.

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

Equations

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

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

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