StrictConstantMappings preserve Function Term Validity

Applying StrictConstantMappings does not alter validity of functional terms in any way since they only rename constants inside terms but do not change their structure. Recall that term validity is required for backtrackings.

theorem StrictConstantMapping.apply_pre_ground_term_preserves_ruleId_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (g : StrictConstantMapping sig) (term : FiniteTree (SkolemFS sig) sig.C) (rl : RuleList sig) : PreGroundTerm.skolem_ruleIds_valid rl term → PreGroundTerm.skolem_ruleIds_valid rl (g.toConstantMapping.apply_pre_ground_term term)

theorem StrictConstantMapping.apply_pre_ground_term_preserves_disjIdx_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (g : StrictConstantMapping sig) (term : FiniteTree (SkolemFS sig) sig.C) (rl : RuleList sig) (h : PreGroundTerm.skolem_ruleIds_valid rl term) : PreGroundTerm.skolem_disjIdx_valid rl term h → PreGroundTerm.skolem_disjIdx_valid rl (g.toConstantMapping.apply_pre_ground_term term) ⋯

theorem StrictConstantMapping.apply_pre_ground_term_preserves_rule_arity_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (g : StrictConstantMapping sig) (term : FiniteTree (SkolemFS sig) sig.C) (rl : RuleList sig) (h : PreGroundTerm.skolem_ruleIds_valid rl term) : PreGroundTerm.skolem_rule_arity_valid rl term h → PreGroundTerm.skolem_rule_arity_valid rl (g.toConstantMapping.apply_pre_ground_term term) ⋯

theorem StrictConstantMapping.apply_ground_term_preserves_ruleId_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (g : StrictConstantMapping sig) (term : GroundTerm sig) (rl : RuleList sig) : GroundTerm.skolem_ruleIds_valid rl term → GroundTerm.skolem_ruleIds_valid rl (g.toConstantMapping.apply_ground_term term)

theorem StrictConstantMapping.apply_ground_term_preserves_disjIdx_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (g : StrictConstantMapping sig) (term : GroundTerm sig) (rl : RuleList sig) (h : GroundTerm.skolem_ruleIds_valid rl term) : GroundTerm.skolem_disjIdx_valid rl term h → GroundTerm.skolem_disjIdx_valid rl (g.toConstantMapping.apply_ground_term term) ⋯

theorem StrictConstantMapping.apply_ground_term_preserves_rule_arity_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (g : StrictConstantMapping sig) (term : GroundTerm sig) (rl : RuleList sig) (h : GroundTerm.skolem_ruleIds_valid rl term) : GroundTerm.skolem_rule_arity_valid rl term h → GroundTerm.skolem_rule_arity_valid rl (g.toConstantMapping.apply_ground_term term) ⋯

theorem PreTrigger.compose_strict_constant_mapping_preserves_ruleId_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (trg : PreTrigger sig) (g : StrictConstantMapping sig) (rl : RuleList sig) : skolem_ruleIds_valid rl trg → skolem_ruleIds_valid rl { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs }

theorem PreTrigger.compose_strict_constant_mapping_preserves_disjIdx_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (trg : PreTrigger sig) (g : StrictConstantMapping sig) (rl : RuleList sig) (h : skolem_ruleIds_valid rl trg) : skolem_disjIdx_valid rl trg h → skolem_disjIdx_valid rl { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs } ⋯

theorem PreTrigger.compose_strict_constant_mapping_preserves_rule_arity_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (trg : PreTrigger sig) (g : StrictConstantMapping sig) (rl : RuleList sig) (h : skolem_ruleIds_valid rl trg) : skolem_rule_arity_valid rl trg h → skolem_rule_arity_valid rl { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs } ⋯