Theorem: liftedCIA.trace_correct (Var/liftedCIA.lean)

State before:
⊢ ∀ (t : TraceRel') (es : vset F SysEl) (ρ : Config F), (trace' t es | ρ) = trace (t | ρ) (es | ρ)
Tactic:
intros t es ρ
State after:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (trace' t es | ρ) = trace (t | ρ) (es | ρ)

State before:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (trace' t es | ρ) = trace (t | ρ) (es | ρ)
Tactic:
simp [trace', Variational.index]
State after:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ vset.index ((fun x => (x.1.2, x.2)) '' {e | e ∈ t ∧ (e.1.1, e.2) ∈ es}) ρ = trace (vset.index t ρ) (vset.index es ρ)

State before:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ vset.index ((fun x => (x.1.2, x.2)) '' {e | e ∈ t ∧ (e.1.1, e.2) ∈ es}) ρ = trace (vset.index t ρ) (vset.index es ρ)
Tactic:
unfold vset.index
State after:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (fun x => ((fun x => (x.1.2, x.2)) '' {e | e ∈ t ∧ (e.1.1, e.2) ∈ es}) (x, ρ)) =
    trace (fun x => t (x, ρ)) fun x => es (x, ρ)

State before:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (fun x => ((fun x => (x.1.2, x.2)) '' {e | e ∈ t ∧ (e.1.1, e.2) ∈ es}) (x, ρ)) =
    trace (fun x => t (x, ρ)) fun x => es (x, ρ)
Tactic:
simp [trace, setOf]
State after:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (fun x => ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ)) =
    (fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)

State before:
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ (fun x => ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ)) =
    (fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)
Tactic:
apply funext
State after:
case h
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ ∀ (x : GSNEl),
    ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ) =
      ((fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)) x

State before:
case h
t : TraceRel'
es : vset F SysEl
ρ : Config F
⊢ ∀ (x : GSNEl),
    ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ) =
      ((fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)) x
Tactic:
intros x
State after:
case h
t : TraceRel'
es : vset F SysEl
ρ : Config F
x : GSNEl
⊢ ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ) =
    ((fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)) x

State before:
case h
t : TraceRel'
es : vset F SysEl
ρ : Config F
x : GSNEl
⊢ ((fun x => (x.1.2, x.2)) '' fun e => e ∈ t ∧ (e.1.1, e.2) ∈ es) (x, ρ) =
    ((fun x => x.2) '' fun e => (e ∈ fun x => t (x, ρ)) ∧ e.1 ∈ fun x => es (x, ρ)) x
Tactic:
simp[Set.image, setOf, Set.mem_def]
State after:
no goals