Relation-renaming proofs

Environment pullback commutes with binding a relation. Structural induction then proves satisfaction, size, and fragment preservation under relation renaming.

theorem Complexity.DescriptiveComplexity.relRenaming_ext_internal {rctx sctx : List Nat} (f g : RelRenaming rctx sctx) (h : f.index = g.index) : f = g

theorem Complexity.DescriptiveComplexity.lift_id_internal (rctx : List Nat) (k : Nat) : (RelRenaming.id rctx).lift k = RelRenaming.id (k :: rctx)

theorem Complexity.DescriptiveComplexity.lift_comp_internal {rctx sctx tctx : List Nat} (g : RelRenaming sctx tctx) (f : RelRenaming rctx sctx) (k : Nat) : (g.comp f).lift k = (g.lift k).comp (f.lift k)

theorem Complexity.DescriptiveComplexity.pull_lift_internal {rctx sctx : List Nat} (f : RelRenaming rctx sctx) {card k : Nat} (S : (Fin k → Fin card) → Prop) (ρ : REnv card sctx) : (f.lift k).pull (rCons S ρ) = rCons S (f.pull ρ)

theorem Complexity.DescriptiveComplexity.pull_weaken_internal {rctx : List Nat} {card k : Nat} (S : (Fin k → Fin card) → Prop) (ρ : REnv card rctx) : (RelRenaming.weaken rctx k).pull (rCons S ρ) = ρ

theorem Complexity.DescriptiveComplexity.renameRel_sat_internal {V : Vocabulary} {rctx sctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (f : RelRenaming rctx sctx) (A : FinStruct V) (σ : Env A.card n) (ρ : REnv A.card sctx) : SOFormula.Sat A σ ρ (SOFormula.renameRel f φ) ↔ SOFormula.Sat A σ (f.pull ρ) φ

theorem Complexity.DescriptiveComplexity.size_renameRel_internal {V : Vocabulary} {rctx sctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (f : RelRenaming rctx sctx) : (SOFormula.renameRel f φ).size = φ.size

theorem Complexity.DescriptiveComplexity.isFOMatrix_renameRel_internal {V : Vocabulary} {rctx sctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (f : RelRenaming rctx sctx) : (SOFormula.renameRel f φ).IsFOMatrix ↔ φ.IsFOMatrix

theorem Complexity.DescriptiveComplexity.isExistSO_renameRel_internal {V : Vocabulary} {rctx sctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (f : RelRenaming rctx sctx) : (SOFormula.renameRel f φ).IsExistSO ↔ φ.IsExistSO

theorem Complexity.DescriptiveComplexity.renameRel_id_internal {V : Vocabulary} {rctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) : SOFormula.renameRel (RelRenaming.id rctx) φ = φ

theorem Complexity.DescriptiveComplexity.renameRel_comp_internal {V : Vocabulary} {rctx sctx tctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (f : RelRenaming rctx sctx) (g : RelRenaming sctx tctx) : SOFormula.renameRel g (SOFormula.renameRel f φ) = SOFormula.renameRel (g.comp f) φ