Theorem: LocalRule.Decreases (Pdl/LocalTableau.lean)

State before:
X : TNode
ress : List TNode
rule : LocalRule X ress
⊢ ∀ Y ∈ ress, ∀ y ∈ node_to_multiset Y, ∃ x ∈ node_to_multiset X, y < x
Tactic:
intro Y Y_in_ress y y_in_Y
State after:
X : TNode
ress : List TNode
rule : LocalRule X ress
Y : TNode
Y_in_ress : Y ∈ ress
y : Formula
y_in_Y : y ∈ node_to_multiset Y
⊢ ∃ x ∈ node_to_multiset X, y < x

State before:
X : TNode
ress : List TNode
rule : LocalRule X ress
Y : TNode
Y_in_ress : Y ∈ ress
y : Formula
y_in_Y : y ∈ node_to_multiset Y
⊢ ∃ x ∈ node_to_multiset X, y < x
Tactic:
cases rule
State after:
case oneSidedL
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
precond✝ : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule precond✝ ress✝
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) ress✝
⊢ ∃ x ∈ node_to_multiset (precond✝, ∅, none), y < x

case oneSidedR
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
precond✝ : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule precond✝ ress✝
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ress✝
⊢ ∃ x ∈ node_to_multiset (∅, precond✝, none), y < x

case LRnegL
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([ϕ✝], [~ϕ✝], none), y < x

case LRnegR
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([~ϕ✝], [ϕ✝], none), y < x

case loadedL
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))), y < x

case loadedR
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))), y < x

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([ϕ✝], [~ϕ✝], none), y < x
Tactic:
case LRnegL => simp at *
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([~ϕ✝], [ϕ✝], none), y < x
Tactic:
case LRnegR => simp at *
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
precond✝ : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule precond✝ ress✝
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) ress✝
⊢ ∃ x ∈ node_to_multiset (precond✝, ∅, none), y < x
Tactic:
case oneSidedL orule =>
  cases orule
  all_goals
    simp [node_to_multiset] at *
    try subst_eqs
    try simp at *
    try subst_eqs
  case neg.refl => linarith
  case con.refl => cases y_in_Y <;> (subst_eqs; linarith)
  case nCo => cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *); linarith
  case dia α φ =>
    rcases Y_in_ress with ⟨E, E_in, E_def⟩
    subst E_def
    simp_all only [List.append_nil, Multiset.mem_coe]
    rw [← add_assoc]
    exact unfoldDiamond.decreases_lmOf E_in y_in_Y
  case box α φ =>
    rcases Y_in_ress with ⟨E, E_in, E_def⟩
    subst E_def
    simp_all only [List.append_nil, Multiset.mem_coe]
    exact unfoldBox.decreases_lmOf E_in y_in_Y
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
precond✝ : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule precond✝ ress✝
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ress✝
⊢ ∃ x ∈ node_to_multiset (∅, precond✝, none), y < x
Tactic:
case oneSidedR orule =>
  cases orule
  all_goals
    simp [node_to_multiset] at *
    try subst_eqs
    try simp at *
    try subst_eqs
  case neg.refl => linarith
  case con.refl => cases y_in_Y <;> (subst_eqs; linarith)
  case nCo => cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *); linarith
  case dia α φ =>
    rcases Y_in_ress with ⟨E, E_in, E_def⟩
    subst E_def
    simp_all only [List.append_nil, Multiset.mem_coe]
    rw [← add_assoc]
    exact unfoldDiamond.decreases_lmOf E_in y_in_Y
  case box α φ =>
    rcases Y_in_ress with ⟨E, E_in, E_def⟩
    subst E_def
    simp_all only [List.append_nil, Multiset.mem_coe]
    exact unfoldBox.decreases_lmOf E_in y_in_Y
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))), y < x
Tactic:
case loadedL lrule =>
  simp [node_to_multiset]
  cases lrule
  all_goals
    simp [node_to_multiset] at *
    try subst_eqs
    try simp at *
    try subst_eqs
  case dia α χ =>
    sorry
  case dia' α φ =>
    sorry
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))), y < x
Tactic:
case loadedR lrule =>
  simp [node_to_multiset]
  cases lrule
  all_goals
    simp [node_to_multiset] at *
    try subst_eqs
    try simp at *
    try subst_eqs
  case dia α χ =>
    sorry
  case dia' α φ =>
    sorry
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([ϕ✝], [~ϕ✝], none), y < x
Tactic:
simp at *
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ϕ✝ : Formula
Y_in_ress : Y ∈ ∅
⊢ ∃ x ∈ node_to_multiset ([~ϕ✝], [ϕ✝], none), y < x
Tactic:
simp at *
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
precond✝ : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule precond✝ ress✝
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) ress✝
⊢ ∃ x ∈ node_to_multiset (precond✝, ∅, none), y < x
Tactic:
cases orule
State after:
case bot
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) ∅
⊢ ∃ x ∈ node_to_multiset ([⊥], ∅, none), y < x

case not
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) ∅
⊢ ∃ x ∈ node_to_multiset ([φ✝, ~φ✝], ∅, none), y < x

case neg
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) [[φ✝]]
⊢ ∃ x ∈ node_to_multiset ([~~φ✝], ∅, none), y < x

case con
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) [[φ✝, ψ✝]]
⊢ ∃ x ∈ node_to_multiset ([φ✝⋀ψ✝], ∅, none), y < x

case nCo
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) [[~φ✝], [~ψ✝]]
⊢ ∃ x ∈ node_to_multiset ([~φ✝⋀ψ✝], ∅, none), y < x

case box
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) (unfoldBox α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset ([⌈α✝⌉φ✝], ∅, none), y < x

case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset ([~⌈α✝⌉φ✝], ∅, none), y < x

State before:
case bot
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) ∅
⊢ ∃ x ∈ node_to_multiset ([⊥], ∅, none), y < x

case not
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) ∅
⊢ ∃ x ∈ node_to_multiset ([φ✝, ~φ✝], ∅, none), y < x

case neg
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) [[φ✝]]
⊢ ∃ x ∈ node_to_multiset ([~~φ✝], ∅, none), y < x

case con
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) [[φ✝, ψ✝]]
⊢ ∃ x ∈ node_to_multiset ([φ✝⋀ψ✝], ∅, none), y < x

case nCo
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) [[~φ✝], [~ψ✝]]
⊢ ∃ x ∈ node_to_multiset ([~φ✝⋀ψ✝], ∅, none), y < x

case box
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) (unfoldBox α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset ([⌈α✝⌉φ✝], ∅, none), y < x

case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset ([~⌈α✝⌉φ✝], ∅, none), y < x
Tactic:
all_goals
  simp [node_to_multiset] at *
  try subst_eqs
  try simp at *
  try subst_eqs
State after:
case neg.refl.refl
y : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)

case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

case nCo
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([~φ✝], [], none) ∨ Y = ([~ψ✝], [], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)

case box
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a ∈ unfoldBox α✝ φ✝, (a, [], none) = Y
⊢ lmOfFormula y < lmOfProgram α✝ + lmOfFormula φ✝

case dia
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α✝ φ✝, (a, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)

State before:
y : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)
Tactic:
case neg.refl => linarith
State after:
no goals

State before:
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
case con.refl => cases y_in_Y <;> (subst_eqs; linarith)
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([~φ✝], [], none) ∨ Y = ([~ψ✝], [], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
case nCo => cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *); linarith
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α φ, (a, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
case dia α φ =>
  rcases Y_in_ress with ⟨E, E_in, E_def⟩
  subst E_def
  simp_all only [List.append_nil, Multiset.mem_coe]
  rw [← add_assoc]
  exact unfoldDiamond.decreases_lmOf E_in y_in_Y
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldBox α φ, (a, [], none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
case box α φ =>
  rcases Y_in_ress with ⟨E, E_in, E_def⟩
  subst E_def
  simp_all only [List.append_nil, Multiset.mem_coe]
  exact unfoldBox.decreases_lmOf E_in y_in_Y
State after:
no goals

State before:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (res, ∅, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset ([~⌈α✝⌉φ✝], ∅, none), y < x
Tactic:
simp [node_to_multiset] at *
State after:
case dia
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α✝ φ✝, (a, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)

State before:
case con
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([φ✝, ψ✝], [], none)
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
try subst_eqs
State after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([φ✝, ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

State before:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([φ✝, ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
try simp at *
State after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

State before:
case neg.refl
y φ✝ : Formula
y_in_Y : y = φ✝
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝)
Tactic:
try subst_eqs
State after:
case neg.refl.refl
y : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)

State before:
case con
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([φ✝, ψ✝], [], none)
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
subst_eqs
State after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([φ✝, ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

State before:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([φ✝, ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
simp at *
State after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

State before:
case neg.refl
y φ✝ : Formula
y_in_Y : y = φ✝
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝)
Tactic:
subst_eqs
State after:
case neg.refl.refl
y : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)

State before:
y : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)
Tactic:
linarith
State after:
no goals

State before:
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
cases y_in_Y <;> (subst_eqs; linarith)
State after:
no goals

State before:
case inr
y φ✝ ψ✝ : Formula
h✝ : y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
subst_eqs
State after:
case inr.refl
y φ✝ : Formula
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula y

State before:
case inr.refl
y φ✝ : Formula
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula y
Tactic:
linarith
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([~φ✝], [], none) ∨ Y = ([~ψ✝], [], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *)
State after:
case inl.refl.refl
φ✝ ψ✝ : Formula
⊢ lmOfFormula φ✝ < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

State before:
case inl.refl.refl
φ✝ ψ✝ : Formula
⊢ lmOfFormula φ✝ < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
linarith
State after:
no goals

State before:
case inr
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
h✝ : Y = ([~ψ✝], [], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
subst_eqs
State after:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([~ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)

State before:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([~ψ✝], [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
simp at *
State after:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = (~ψ✝)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)

State before:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = (~ψ✝)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
subst_eqs
State after:
case inr.refl.refl
φ✝ ψ✝ : Formula
⊢ lmOfFormula (~ψ✝) < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)

State before:
case inr.refl.refl
φ✝ ψ✝ : Formula
⊢ lmOfFormula (~ψ✝) < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
simp at *
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α φ, (a, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
rcases Y_in_ress with ⟨E, E_in, E_def⟩
State after:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
E_def : (E, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)

State before:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
E_def : (E, [], none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
subst E_def
State after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y :
  y ∈
    match (E, [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)

State before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y :
  y ∈
    match (E, [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
simp_all only [List.append_nil, Multiset.mem_coe]
State after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)

State before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
rw [← add_assoc]
State after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < 1 + lmOfProgram α + lmOfFormula φ

State before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < 1 + lmOfProgram α + lmOfFormula φ
Tactic:
exact unfoldDiamond.decreases_lmOf E_in y_in_Y
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldBox α φ, (a, [], none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
rcases Y_in_ress with ⟨E, E_in, E_def⟩
State after:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
E_def : (E, [], none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ

State before:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
E_def : (E, [], none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
subst E_def
State after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y :
  y ∈
    match (E, [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ

State before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y :
  y ∈
    match (E, [], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
simp_all only [List.append_nil, Multiset.mem_coe]
State after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ

State before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y : y ∈ E
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
exact unfoldBox.decreases_lmOf E_in y_in_Y
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
precond✝ : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule precond✝ ress✝
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ress✝
⊢ ∃ x ∈ node_to_multiset (∅, precond✝, none), y < x
Tactic:
cases orule
State after:
case bot
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ∅
⊢ ∃ x ∈ node_to_multiset (∅, [⊥], none), y < x

case not
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ∅
⊢ ∃ x ∈ node_to_multiset (∅, [φ✝, ~φ✝], none), y < x

case neg
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[φ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [~~φ✝], none), y < x

case con
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[φ✝, ψ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [φ✝⋀ψ✝], none), y < x

case nCo
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[~φ✝], [~ψ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [~φ✝⋀ψ✝], none), y < x

case box
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) (unfoldBox α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset (∅, [⌈α✝⌉φ✝], none), y < x

case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset (∅, [~⌈α✝⌉φ✝], none), y < x

State before:
case bot
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ∅
⊢ ∃ x ∈ node_to_multiset (∅, [⊥], none), y < x

case not
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) ∅
⊢ ∃ x ∈ node_to_multiset (∅, [φ✝, ~φ✝], none), y < x

case neg
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[φ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [~~φ✝], none), y < x

case con
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[φ✝, ψ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [φ✝⋀ψ✝], none), y < x

case nCo
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
φ✝ ψ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) [[~φ✝], [~ψ✝]]
⊢ ∃ x ∈ node_to_multiset (∅, [~φ✝⋀ψ✝], none), y < x

case box
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) (unfoldBox α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset (∅, [⌈α✝⌉φ✝], none), y < x

case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset (∅, [~⌈α✝⌉φ✝], none), y < x
Tactic:
all_goals
  simp [node_to_multiset] at *
  try subst_eqs
  try simp at *
  try subst_eqs
State after:
case neg.refl.refl
y : Formula
⊢ lmOfFormula y < 1 + (1 + lmOfFormula y)

case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

case nCo
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([], [~φ✝], none) ∨ Y = ([], [~ψ✝], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)

case box
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a ∈ unfoldBox α✝ φ✝, ([], a, none) = Y
⊢ lmOfFormula y < lmOfProgram α✝ + lmOfFormula φ✝

case dia
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α✝ φ✝, ([], a, none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([], [~φ✝], none) ∨ Y = ([], [~ψ✝], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
case nCo => cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *); linarith
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α φ, ([], a, none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
case dia α φ =>
  rcases Y_in_ress with ⟨E, E_in, E_def⟩
  subst E_def
  simp_all only [List.append_nil, Multiset.mem_coe]
  rw [← add_assoc]
  exact unfoldDiamond.decreases_lmOf E_in y_in_Y
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldBox α φ, ([], a, none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
case box α φ =>
  rcases Y_in_ress with ⟨E, E_in, E_def⟩
  subst E_def
  simp_all only [List.append_nil, Multiset.mem_coe]
  exact unfoldBox.decreases_lmOf E_in y_in_Y
State after:
no goals

State before:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress : Y ∈ List.map (fun res => (∅, res, none)) (unfoldDiamond α✝ φ✝)
⊢ ∃ x ∈ node_to_multiset (∅, [~⌈α✝⌉φ✝], none), y < x
Tactic:
simp [node_to_multiset] at *
State after:
case dia
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α✝ φ✝, ([], a, none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)

State before:
case con
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([], [φ✝, ψ✝], none)
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
try subst_eqs
State after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([], [φ✝, ψ✝], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

State before:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([], [φ✝, ψ✝], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
try simp at *
State after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

State before:
case con
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([], [φ✝, ψ✝], none)
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
subst_eqs
State after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([], [φ✝, ψ✝], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

State before:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([], [φ✝, ψ✝], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝
Tactic:
simp at *
State after:
case con.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = φ✝ ∨ y = ψ✝
⊢ lmOfFormula y < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
Y_in_ress : Y = ([], [~φ✝], none) ∨ Y = ([], [~ψ✝], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
cases Y_in_ress <;> (subst_eqs; simp at * ; subst_eqs ; simp at *)
State after:
case inl.refl.refl
φ✝ ψ✝ : Formula
⊢ lmOfFormula φ✝ < 1 + lmOfFormula φ✝ + lmOfFormula ψ✝

State before:
case inr
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
φ✝ ψ✝ : Formula
h✝ : Y = ([], [~ψ✝], none)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
subst_eqs
State after:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([], [~ψ✝], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)

State before:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y :
  y ∈
    match ([], [~ψ✝], none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)
Tactic:
simp at *
State after:
case inr.refl
y φ✝ ψ✝ : Formula
y_in_Y : y = (~ψ✝)
⊢ lmOfFormula y < 1 + (1 + lmOfFormula φ✝ + lmOfFormula ψ✝)

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldDiamond α φ, ([], a, none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
rcases Y_in_ress with ⟨E, E_in, E_def⟩
State after:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
E_def : ([], E, none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)

State before:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
E_def : ([], E, none) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
subst E_def
State after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y :
  y ∈
    match ([], E, none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)

State before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y :
  y ∈
    match ([], E, none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
simp_all only [List.append_nil, Multiset.mem_coe]
State after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ [] ++ E
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)

State before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ [] ++ E
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
rw [← add_assoc]
State after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ [] ++ E
⊢ lmOfFormula y < 1 + lmOfProgram α + lmOfFormula φ

State before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldDiamond α φ
y_in_Y : y ∈ [] ++ E
⊢ lmOfFormula y < 1 + lmOfProgram α + lmOfFormula φ
Tactic:
exact unfoldDiamond.decreases_lmOf E_in y_in_Y
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a ∈ unfoldBox α φ, ([], a, none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
rcases Y_in_ress with ⟨E, E_in, E_def⟩
State after:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
E_def : ([], E, none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ

State before:
case intro.intro
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
E_def : ([], E, none) = Y
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
subst E_def
State after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y :
  y ∈
    match ([], E, none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ

State before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y :
  y ∈
    match ([], E, none) with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
simp_all only [List.append_nil, Multiset.mem_coe]
State after:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y : y ∈ [] ++ E
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ

State before:
case intro.intro
y : Formula
α : Program
φ : Formula
E : List Formula
E_in : E ∈ unfoldBox α φ
y_in_Y : y ∈ [] ++ E
⊢ lmOfFormula y < lmOfProgram α + lmOfFormula φ
Tactic:
exact unfoldBox.decreases_lmOf E_in y_in_Y
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))), y < x
Tactic:
simp [node_to_multiset]
State after:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      ress✝
⊢ lmOfFormula y < 1 + lmOfFormula (unload χ✝)

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      ress✝
⊢ lmOfFormula y < 1 + lmOfFormula (unload χ✝)
Tactic:
cases lrule
State after:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
χ✝ : LoadFormula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      (unfoldDiamondLoad α✝ χ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋χ✝))

case dia'
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))

State before:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
χ✝ : LoadFormula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      (unfoldDiamondLoad α✝ χ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋χ✝))

case dia'
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))
Tactic:
all_goals
  simp [node_to_multiset] at *
  try subst_eqs
  try simp at *
  try subst_eqs
State after:
case dia
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
χ✝ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α✝ χ✝ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula (unload χ✝))

case dia'
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad' α✝ φ✝ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
χ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α χ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula (unload χ))
Tactic:
case dia α χ =>
  sorry
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad' α φ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
case dia' α φ =>
  sorry
State after:
no goals

State before:
case dia'
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (X, ∅, Option.map Sum.inl o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))
Tactic:
simp [node_to_multiset] at *
State after:
case dia'
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad' α✝ φ✝ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
χ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α χ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula (unload χ))
Tactic:
sorry
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad' α φ ∧ (a, [], Option.map Sum.inl b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
sorry
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      ress✝
⊢ ∃ x ∈ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))), y < x
Tactic:
simp [node_to_multiset]
State after:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      ress✝
⊢ lmOfFormula y < 1 + lmOfFormula (unload χ✝)

State before:
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule : LoadRule (~'χ✝) ress✝
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      ress✝
⊢ lmOfFormula y < 1 + lmOfFormula (unload χ✝)
Tactic:
cases lrule
State after:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
χ✝ : LoadFormula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad α✝ χ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋χ✝))

case dia'
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))

State before:
case dia
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
χ✝ : LoadFormula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad α✝ χ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋χ✝))

case dia'
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))
Tactic:
all_goals
  simp [node_to_multiset] at *
  try subst_eqs
  try simp at *
  try subst_eqs
State after:
case dia
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
χ✝ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α✝ χ✝ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula (unload χ✝))

case dia'
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad' α✝ φ✝ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
χ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α χ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula (unload χ))
Tactic:
case dia α χ =>
  sorry
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad' α φ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
case dia' α φ =>
  sorry
State after:
no goals

State before:
case dia'
Y : TNode
y : Formula
y_in_Y : y ∈ node_to_multiset Y
α✝ : Program
φ✝ : Formula
Y_in_ress :
  Y ∈
    List.map
      (fun x =>
        match x with
        | (X, o) => (∅, X, Option.map Sum.inr o))
      (unfoldDiamondLoad' α✝ φ✝)
⊢ lmOfFormula y < 1 + lmOfFormula (unload (⌊α✝⌋φ✝))
Tactic:
simp [node_to_multiset] at *
State after:
case dia'
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α✝ : Program
φ✝ : Formula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad' α✝ φ✝ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α✝ + lmOfFormula φ✝)

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
χ : LoadFormula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad α χ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula (unload χ))
Tactic:
sorry
State after:
no goals

State before:
Y : TNode
y : Formula
y_in_Y :
  y ∈
    match Y with
    | (L, R, none) => ↑(L ++ R)
    | (L, R, some (Sum.inl (~'χ))) => ↑(L ++ R) + {~unload χ}
    | (L, R, some (Sum.inr (~'χ))) => ↑(L ++ R) + {~unload χ}
α : Program
φ : Formula
Y_in_ress : ∃ a b, (a, b) ∈ unfoldDiamondLoad' α φ ∧ ([], a, Option.map Sum.inr b) = Y
⊢ lmOfFormula y < 1 + (lmOfProgram α + lmOfFormula φ)
Tactic:
sorry
State after:
no goals