Theorem: loadRuleTruth (Pdl/LocalTableau.lean)

State before:
χ : LoadFormula
B : List (List Formula × Option NegLoadFormula)
lr : LoadRule (~'χ) B
⊢ (~unload χ)≡dis
      (List.map
        (fun x =>
          match x with
          | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
        B)
Tactic:
intro W M w
State after:
χ : LoadFormula
B : List (List Formula × Option NegLoadFormula)
lr : LoadRule (~'χ) B
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~unload χ) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          B))

State before:
χ : LoadFormula
B : List (List Formula × Option NegLoadFormula)
lr : LoadRule (~'χ) B
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~unload χ) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          B))
Tactic:
cases lr
State after:
case dia
W : Type
M : KripkeModel W
w : W
α✝ : Program
χ✝ : LoadFormula
⊢ evaluate M w (~unload (⌊α✝⌋χ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad α✝ χ✝)))

case dia'
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (~unload (⌊α✝⌋φ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad' α✝ φ✝)))

State before:
W : Type
M : KripkeModel W
w : W
α✝ : Program
χ✝ : LoadFormula
⊢ evaluate M w (~unload (⌊α✝⌋χ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad α✝ χ✝)))
Tactic:
case dia =>
  sorry
State after:
no goals

State before:
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (~unload (⌊α✝⌋φ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad' α✝ φ✝)))
Tactic:
case dia' =>
  sorry
State after:
no goals

State before:
W : Type
M : KripkeModel W
w : W
α✝ : Program
χ✝ : LoadFormula
⊢ evaluate M w (~unload (⌊α✝⌋χ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad α✝ χ✝)))
Tactic:
sorry
State after:
no goals

State before:
W : Type
M : KripkeModel W
w : W
α✝ : Program
φ✝ : Formula
⊢ evaluate M w (~unload (⌊α✝⌋φ✝)) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          (unfoldDiamondLoad' α✝ φ✝)))
Tactic:
sorry
State after:
no goals