Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
812 B · 22 lines
at dev
1234567891011121314151617181920212223import PackageCalculus.Versions.Lifting.Definitionimport PackageCalculus.Versions.Lifting.Retractionimport PackageCalculus.Versions.Reduction.Correctness
set_option linter.unusedSectionVars false
namespace PackageCalculus
variable {V : Type*} [DecidableEq V]variable {N : Type*} [DecidableEq N]
/-- If `S` is a VF-resolution for the lifted deps, it is a resolution for the original concrete `Δ`. -/theorem liftResolution_completeness [LinearOrder V] (R : Real N V) (Δ : DepRel N V) (r : Package N V) (S : Finset (Package N V)) (hres : IsVFResolution R (liftVFDeps R Δ) r S) : IsResolution R Δ r S := by have h := (version_formula_correct R (liftVFDeps R Δ) r S).mpr hres rw [liftVFDeps_vfReduce R Δ] at h exact (restrictReal_resolution_iff R Δ r S).mp h
end PackageCalculus