Backtracking Facts for a PreTrigger

We mainly lift the machinery around PreGroundTerm.backtrackFacts to PreTrigger. The interesting parts are PreTrigger.backtrackFacts and PreTrigger.backtrackFacts_eq_of_strong_equiv.

def PreTrigger.skolem_ruleIds_valid {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) : Prop

Equations

• PreTrigger.skolem_ruleIds_valid rl trg = ∀ (t : GroundTerm sig), t ∈ List.flatMap GeneralizedAtom.terms trg.mapped_body → GroundTerm.skolem_ruleIds_valid rl t

def PreTrigger.skolem_disjIdx_valid {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) : Prop

Equations

• PreTrigger.skolem_disjIdx_valid rl trg trg_ruleIds_valid = ∀ (t : GroundTerm sig) (h : t ∈ List.flatMap GeneralizedAtom.terms trg.mapped_body), GroundTerm.skolem_disjIdx_valid rl t ⋯

def PreTrigger.skolem_rule_arity_valid {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) : Prop

Equations

• PreTrigger.skolem_rule_arity_valid rl trg trg_ruleIds_valid = ∀ (t : GroundTerm sig) (h : t ∈ List.flatMap GeneralizedAtom.terms trg.mapped_body), GroundTerm.skolem_rule_arity_valid rl t ⋯

theorem PreTrigger.skolem_ruleIds_valid_of_strong_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rl : RuleList sig} {trg trg2 : PreTrigger sig} (strong_equiv : trg.strong_equiv trg2) (trg_valid : skolem_ruleIds_valid rl trg) : skolem_ruleIds_valid rl trg2

theorem PreTrigger.skolem_disjIdx_valid_of_strong_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rl : RuleList sig} {trg trg2 : PreTrigger sig} (strong_equiv : trg.strong_equiv trg2) (h : skolem_ruleIds_valid rl trg) (trg_valid : skolem_disjIdx_valid rl trg h) : skolem_disjIdx_valid rl trg2 ⋯

theorem PreTrigger.skolem_rule_arity_valid_of_strong_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rl : RuleList sig} {trg trg2 : PreTrigger sig} (strong_equiv : trg.strong_equiv trg2) (h : skolem_ruleIds_valid rl trg) (trg_valid : skolem_rule_arity_valid rl trg h) : skolem_rule_arity_valid rl trg2 ⋯

theorem PreTrigger.skolem_ruleIds_valid_for_functional_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) (rule_mem : trg.rule ∈ rl.rules) (body_valid : skolem_ruleIds_valid rl trg) (i : Nat) (v : sig.V) : GroundTerm.skolem_ruleIds_valid rl (trg.functional_term_for_var i v)

theorem PreTrigger.skolem_disjIdx_valid_for_functional_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) (rule_mem : trg.rule ∈ rl.rules) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) (body_valid : skolem_disjIdx_valid rl trg trg_ruleIds_valid) (i : Nat) (v : sig.V) : i < trg.rule.head.length → GroundTerm.skolem_disjIdx_valid rl (trg.functional_term_for_var i v) ⋯

theorem PreTrigger.skolem_rule_arity_valid_for_functional_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) (rule_mem : trg.rule ∈ rl.rules) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) (body_valid : skolem_rule_arity_valid rl trg trg_ruleIds_valid) (i : Nat) (v : sig.V) : GroundTerm.skolem_rule_arity_valid rl (trg.functional_term_for_var i v) ⋯

theorem PreTrigger.skolem_ruleIds_valid_for_fresh_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) (rule_mem : trg.rule ∈ rl.rules) (body_valid : skolem_ruleIds_valid rl trg) (i : Nat) (lt : i < trg.rule.head.length) (t : GroundTerm sig) : t ∈ trg.fresh_terms_for_head_disjunct i lt → GroundTerm.skolem_ruleIds_valid rl t

theorem PreTrigger.skolem_disjIdx_valid_for_fresh_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) (rule_mem : trg.rule ∈ rl.rules) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) (body_valid : skolem_disjIdx_valid rl trg trg_ruleIds_valid) (i : Nat) (lt : i < trg.rule.head.length) (t : GroundTerm sig) (t_mem : t ∈ trg.fresh_terms_for_head_disjunct i lt) : GroundTerm.skolem_disjIdx_valid rl t ⋯

theorem PreTrigger.skolem_rule_arity_valid_for_fresh_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) (rule_mem : trg.rule ∈ rl.rules) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) (body_valid : skolem_rule_arity_valid rl trg trg_ruleIds_valid) (i : Nat) (lt : i < trg.rule.head.length) (t : GroundTerm sig) (t_mem : t ∈ trg.fresh_terms_for_head_disjunct i lt) : GroundTerm.skolem_rule_arity_valid rl t ⋯

theorem PreTrigger.skolem_ruleIds_remain_valid_in_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) (rule_mem : trg.rule ∈ rl.rules) (body_valid : skolem_ruleIds_valid rl trg) (t : GroundTerm sig) : t ∈ List.flatMap GeneralizedAtom.terms trg.mapped_head.flatten → GroundTerm.skolem_ruleIds_valid rl t

theorem PreTrigger.skolem_disjIdx_remains_valid_in_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) (rule_mem : trg.rule ∈ rl.rules) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) (body_valid : skolem_disjIdx_valid rl trg trg_ruleIds_valid) (t : GroundTerm sig) (t_mem : t ∈ List.flatMap GeneralizedAtom.terms trg.mapped_head.flatten) : GroundTerm.skolem_disjIdx_valid rl t ⋯

theorem PreTrigger.skolem_rule_arity_remains_valid_in_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (trg : PreTrigger sig) (rule_mem : trg.rule ∈ rl.rules) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) (body_valid : skolem_rule_arity_valid rl trg trg_ruleIds_valid) (t : GroundTerm sig) (t_mem : t ∈ List.flatMap GeneralizedAtom.terms trg.mapped_head.flatten) : GroundTerm.skolem_rule_arity_valid rl t ⋯

def PreTrigger.backtrackTrigger_for_functional_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rl : RuleList sig) (trg : PreTrigger sig) (trg_rule_mem : trg.rule ∈ rl.rules) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) (trg_rule_arity_valid : skolem_rule_arity_valid rl trg trg_ruleIds_valid) (forbidden_constants : List sig.C) (i : Nat) (v : sig.V) : PreTrigger sig

Equations

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

theorem PreTrigger.backtrackTrigger_for_functional_term_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rl : RuleList sig) (trg : PreTrigger sig) (trg_rule_mem : trg.rule ∈ rl.rules) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) (trg_rule_arity_valid : skolem_rule_arity_valid rl trg trg_ruleIds_valid) (forbidden_constants : List sig.C) (i : Nat) (v : sig.V) : (backtrackTrigger_for_functional_term rl trg trg_rule_mem trg_ruleIds_valid trg_rule_arity_valid forbidden_constants i v).equiv trg

def PreTrigger.backtrackFacts {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rl : RuleList sig) (trg : PreTrigger sig) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) (trg_disjIdx_valid : skolem_disjIdx_valid rl trg trg_ruleIds_valid) (trg_rule_arity_valid : skolem_rule_arity_valid rl trg trg_ruleIds_valid) : List (Fact sig) × List sig.C

The backtracking of a PreTrigger consists of its mapped body and the backtrackings of all GroundTerms that occur in its mapped body.

Equations

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

theorem PreTrigger.backtrackFacts_eq_of_strong_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rl : RuleList sig) (trg trg2 : PreTrigger sig) (trg_ruleIds_valid : skolem_ruleIds_valid rl trg) (trg_disjIdx_valid : skolem_disjIdx_valid rl trg trg_ruleIds_valid) (trg_rule_arity_valid : skolem_rule_arity_valid rl trg trg_ruleIds_valid) (strong_equiv : trg.strong_equiv trg2) : backtrackFacts rl trg trg_ruleIds_valid trg_disjIdx_valid trg_rule_arity_valid = backtrackFacts rl trg2 ⋯ ⋯ ⋯

The backtracking of two PreTriggers is the same if they are strongly equivalent, i.e. they have the same rule and the same mapped body.