Equations
- instHasLengthConsTNode = { lengthOf := fun (x : ConsTNode) => match x with | ⟨LR, property⟩ => HasLength.lengthOf LR }
A Path ctn
is a maximal path of consistent TNodes starting with ctn
and connected by LocalRuleApp
s.
This does not have to be a path in any particular LocalTableau
.
- endNode {LR : TNode} {LR_cons : Consistent LR} (isSimple : Simple LR) : Path ⟨LR, LR_cons⟩
- interNode {LR : TNode} {C : List TNode} {c : TNode} {c_cons : Consistent c} {LR_cons : Consistent LR} : LocalRuleApp LR C → (c_in : c ∈ C) → (tail : Path ⟨c, c_cons⟩) → Path ⟨LR, LR_cons⟩
Instances For
@[irreducible]
Equations
- pathToFinset (Path.endNode isSimple) = L ∪ R
- pathToFinset (Path.interNode x_1 c_in tail) = L ∪ R ∪ pathToFinset tail
Instances For
@[simp]
theorem
LR_in_PathLR
{L R : Finset Formula}
{LR_cons : Consistent (L, R)}
(path : Path ⟨(L, R), LR_cons⟩)
:
L ∪ R ⊆ pathToFinset path
@[irreducible]
Equations
- endNodeOf (Path.endNode isSimple) = ⟨LR, LR_cons⟩
- endNodeOf (Path.interNode x_1 c_in tail) = endNodeOf tail
Instances For
theorem
consistentThenConsistentChild
{L R : Finset Formula}
{C : List TNode}
(lrApp : LocalRuleApp (L, R) C)
:
Consistent (L, R) → ∃ c ∈ C, Consistent c
theorem
consThenProjectLCons
{L : Finset Formula}
{α : Formula}
{R : Finset Formula}
(α_in : ~(□α) ∈ L)
(LR_simple : Simple (L, R))
:
Consistent (L, R) → Consistent (diamondProjectTNode (Sum.inl α) (L, R))
theorem
consThenProjectRCons
{R : Finset Formula}
{α : Formula}
{L : Finset Formula}
(α_in : ~(□α) ∈ R)
(LR_simple : Simple (L, R))
:
Consistent (L, R) → Consistent (diamondProjectTNode (Sum.inr α) (L, R))
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
pathConsistent
{TN : ConsTNode}
(path : Path TN)
:
⊥ ∉ pathToFinset path ∧ ∀ (pp : Char), (·pp) ∈ pathToFinset path → (~·pp) ∉ pathToFinset path
theorem
pathProjection
{consLR : ConsTNode}
(path : Path consLR)
:
projection (pathToFinset path) ⊆ projection (toFinset (endNodeOf path))
- base {T0 : ConsTNode} : M₀ T0 T0
- inductiveL {T0 : ConsTNode} {L R : Finset Formula} {LR_cons : Consistent (L, R)} (T : ConsTNode) : M₀ T0 T → ∀ (eq : ⟨(L, R), LR_cons⟩ = endNodeOf (aPathOf T)) (α : Formula) (h : ~(□α) ∈ L), M₀ T0 ⟨diamondProjectTNode (Sum.inl α) (L, R), ⋯⟩
- inductiveR {T0 : ConsTNode} {L R : Finset Formula} {LR_cons : Consistent (L, R)} (T : ConsTNode) : M₀ T0 T → ∀ (eq : ⟨(L, R), LR_cons⟩ = endNodeOf (aPathOf T)) (α : Formula) (h : ~(□α) ∈ R), M₀ T0 ⟨diamondProjectTNode (Sum.inr α) (L, R), ⋯⟩
Instances For
theorem
modelExistence
{L R : Finset Formula}
:
Consistent (L, R) → ∃ (WS : Set (Finset Formula)) (x : ModelGraph WS) (W : ↑WS), L ∪ R ⊆ ↑W