diff --git a/Pdl/Completeness.lean b/Pdl/Completeness.lean index b114400..76dba60 100644 --- a/Pdl/Completeness.lean +++ b/Pdl/Completeness.lean @@ -1,6 +1,7 @@ -- COMPLETENESS import Pdl.Soundness +import Pdl.TableauGame import Pdl.Modelgraphs open HasSat diff --git a/Pdl/LoadSplit.lean b/Pdl/LoadSplit.lean index 1f31029..783576b 100644 --- a/Pdl/LoadSplit.lean +++ b/Pdl/LoadSplit.lean @@ -1,6 +1,8 @@ import Pdl.Syntax import Mathlib.Tactic.Use +-- TODO: move all this into Pdl.Syntax + /-! ## Spliting of loaded formulas -/ mutual @@ -85,7 +87,7 @@ theorem LoadFormula.split_eq_loadMulti_nonEmpty' {δ φ} (lf : LoadFormula) rw [this] theorem loadMulti_nonEmpty_eq_loadMulti : - loadMulti_nonEmpty (δ ++ [α]) h φ = loadMulti δ α φ := by -- wrong ? + loadMulti_nonEmpty (δ ++ [α]) h φ = loadMulti δ α φ := by induction δ · simp case cons IH => diff --git a/dependencies.svg b/dependencies.svg index 5a71739..a1a55e4 100644 --- a/dependencies.svg +++ b/dependencies.svg @@ -4,370 +4,400 @@ - + %3 - + Soundness - -Soundness + +Soundness Completeness - -Completeness + +Completeness Soundness->Completeness - - + + - + PartInterpolation - -PartInterpolation + +PartInterpolation - + Completeness->PartInterpolation - - + + - + +TableauGame + +TableauGame + + + +TableauGame->Completeness + + + + + Modelgraphs - -Modelgraphs + +Modelgraphs - + Modelgraphs->Completeness - - + + - + Semantics - -Semantics + +Semantics - + Semantics->Modelgraphs - - + + - + Discon - -Discon + +Discon - + Semantics->Discon - - + + - + Examples - -Examples + +Examples - + Semantics->Examples - - + + - + SemQuot - -SemQuot + +SemQuot - + Semantics->SemQuot - - + + - + Substitution - -Substitution + +Substitution - + Semantics->Substitution - - + + - + Discon->Substitution - - + + - + Vocab - -Vocab + +Vocab - + Vocab->Discon - - + + - + Fresh - -Fresh + +Fresh - + Vocab->Fresh - - + + - + UnfoldDia - -UnfoldDia + +UnfoldDia - + UnfoldDia->Modelgraphs - - + + - + Distance - -Distance + +Distance - + UnfoldDia->Distance - - + + - + LocalTableau - -LocalTableau + +LocalTableau - + UnfoldDia->LocalTableau - - + + - + Distance->PartInterpolation - - + + - + Star - -Star + +Star - + Star->UnfoldDia - - + + - + Star->Examples - - + + - + UnfoldBox - -UnfoldBox + +UnfoldBox - + Star->UnfoldBox - - + + - + UnfoldBox->Modelgraphs - - + + - + UnfoldBox->Examples - - + + - + UnfoldBox->LocalTableau - - + + - + Syntax - -Syntax + +Syntax - + Syntax->Semantics - - + + - + Syntax->Vocab - - + + - + FischerLadner - -FischerLadner + +FischerLadner - + Syntax->FischerLadner - - + + - + LoadSplit - -LoadSplit + +LoadSplit - + Syntax->LoadSplit - - + + - + Measures - -Measures + +Measures - + Syntax->Measures - - + + - + FischerLadner->UnfoldBox - - + + - + Fresh->UnfoldDia - - + + - + Fresh->UnfoldBox - - + + - + Interpolation - -Interpolation + +Interpolation - + PartInterpolation->Interpolation - - + + - + LoadSplit->Soundness - - + + - + Tableau - -Tableau + +Tableau - + LocalTableau->Tableau - - + + - + MultisetOrder - -MultisetOrder + +MultisetOrder - + MultisetOrder->LocalTableau - - + + - + Measures->Semantics - - + + - + Tableau->Soundness - - + + + + + +Tableau->TableauGame + + - + Substitution->UnfoldDia - - + + - + Substitution->UnfoldBox - - + + + + + +Game + +Game + + + +Game->TableauGame + +