Theorem: correctness (Pdl/Soundness.lean)

State before:
⊢ ∀ (LR : TNode), satisfiable LR → consistent LR
Tactic:
intro LR
State after:
LR : TNode
⊢ satisfiable LR → consistent LR

State before:
LR : TNode
⊢ satisfiable LR → consistent LR
Tactic:
contrapose
State after:
LR : TNode
⊢ ¬consistent LR → ¬satisfiable LR

State before:
LR : TNode
⊢ ¬consistent LR → ¬satisfiable LR
Tactic:
unfold consistent
State after:
LR : TNode
⊢ (¬let LR := LR;
      ¬inconsistent LR) →
    ¬satisfiable LR

State before:
LR : TNode
⊢ (¬let LR := LR;
      ¬inconsistent LR) →
    ¬satisfiable LR
Tactic:
unfold inconsistent
State after:
LR : TNode
⊢ (¬let LR := LR;
      ¬let LR := LR;
        Nonempty (ClosedTableau LoadHistory.nil LR)) →
    ¬satisfiable LR

State before:
LR : TNode
⊢ (¬let LR := LR;
      ¬let LR := LR;
        Nonempty (ClosedTableau LoadHistory.nil LR)) →
    ¬satisfiable LR
Tactic:
simp only [not_nonempty_iff, not_isEmpty_iff, not_exists, not_forall, exists_prop, Nonempty.forall]
State after:
LR : TNode
⊢ ClosedTableau LoadHistory.nil LR → ¬satisfiable LR

State before:
LR : TNode
⊢ ClosedTableau LoadHistory.nil LR → ¬satisfiable LR
Tactic:
intro hyp
State after:
LR : TNode
hyp : ClosedTableau LoadHistory.nil LR
⊢ ¬satisfiable LR

State before:
LR : TNode
hyp : ClosedTableau LoadHistory.nil LR
⊢ ¬satisfiable LR
Tactic:
apply tableauThenNotSat LR hyp
State after:
no goals