Prove2Me

KRF.reducible_trans

Proved
KRF.reducible_trans

by jario · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Reducibility between knowledge representation formalisms is transitive.

Preamble
import Definitions.Def_KRF_Data
import Definitions.Def_KRF_Machinery
import Definitions.Def_KRF_RenamingProps
noncomputable section
open KRFCore
open KRFCore.FStruct
open KRF
variable {σD σQ σ : Sig}
Formal statement
theorem KRF.reducible_trans {σD σQ : Sig} {Q : QueryLanguage σQ}
    (Γ₁ Γ₂ Γ₃ : Krf σD σQ Q) :
    ReducibleTo Γ₁ Γ₂ → ReducibleTo Γ₂ Γ₃ → ReducibleTo Γ₁ Γ₃ :=
  sorry
Source
arXiv 2412.11855v2

View graph