theory Invariants imports SCL_FOL begin text ‹The following lemma restate existing invariants in a compact, paper-friendly way.› lemma (in scl_fol_calculus) scl_state_invariants: shows inv_trail_lits_ground: "trail_lits_ground initial_state" "scl N β S S' ⟹ trail_lits_ground S ⟹ trail_lits_ground S'" and inv_trail_atoms_lt: "trail_atoms_lt β initial_state" "scl N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'" and inv_undefined_trail_lits: "∀Γ' Ln Γ''. state_trail initial_state = Γ'' @ Ln # Γ' ⟶ ¬ trail_defined_lit Γ' (fst Ln)" "scl N β S S' ⟹ (∀Γ' Ln Γ''. state_trail S = Γ'' @ Ln # Γ' ⟶ ¬ trail_defined_lit Γ' (fst Ln)) ⟹ (∀Γ' Ln Γ''. state_trail S' = Γ'' @ Ln # Γ' ⟶ ¬ trail_defined_lit Γ' (fst Ln))" and inv_ground_closures: "ground_closures initial_state" "scl N β S S' ⟹ ground_closures S ⟹ ground_closures S'" and inv_ground_false_closures: "ground_false_closures initial_state" "scl N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'" and inv_trail_propagated_lits_wf: "∀𝒦∈set (state_trail initial_state). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ" "scl N β S S' ⟹ (∀𝒦∈set (state_trail S). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ) ⟹ (∀𝒦∈set (state_trail S'). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ)" and inv_trail_resolved_lits_pol: "trail_resolved_lits_pol initial_state" "scl N β S S' ⟹ trail_resolved_lits_pol S ⟹ trail_resolved_lits_pol S'" and inv_initial_lits_generalize_learned_trail_conflict: "initial_lits_generalize_learned_trail_conflict N initial_state" "scl N β S S' ⟹ initial_lits_generalize_learned_trail_conflict N S ⟹ initial_lits_generalize_learned_trail_conflict N S'" and inv_trail_lits_from_clauses: "trail_lits_from_clauses N initial_state" "scl N β S S' ⟹ trail_lits_from_clauses N S ⟹ trail_lits_from_clauses N S'" and inv_sound_state: "sound_state N β initial_state" "scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'" using trail_lits_ground_initial_state scl_preserves_trail_lits_ground using trail_atoms_lt_initial_state scl_preserves_trail_atoms_lt using trail_lits_consistent_initial_state[unfolded trail_lits_consistent_def trail_consistent_iff] scl_preserves_trail_lits_consistent[unfolded trail_lits_consistent_def trail_consistent_iff] using ground_closures_initial_state scl_preserves_ground_closures using ground_false_closures_initial_state scl_preserves_ground_false_closures using trail_propagated_lit_wf_initial_state scl_preserves_trail_propagated_lit_wf using trail_resolved_lits_pol_initial_state scl_preserves_trail_resolved_lits_pol using initial_lits_generalize_learned_trail_conflict_initial_state scl_preserves_initial_lits_generalize_learned_trail_conflict using trail_lits_from_clauses_initial_state scl_preserves_trail_lits_from_clauses using sound_initial_state scl_preserves_sound_state by metis+ end