Theorem: liftedCIA.GSN_IA'_correct (Var/liftedCIA.lean)

State before:
⊢ ∀ (S S' : Sys') (A : GSN') (R : TraceRel') (D : Delta') (ρ : Config F),
    (GSN_IA' S S' A R D | ρ) = GSN_IA (S | ρ) (S' | ρ) (A | ρ) (R | ρ) (D | ρ)
Tactic:
intros S S' A R D ρ
State after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (GSN_IA' S S' A R D | ρ) = GSN_IA (S | ρ) (S' | ρ) (A | ρ) (R | ρ) (D | ρ)

State before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (GSN_IA' S S' A R D | ρ) = GSN_IA (S | ρ) (S' | ρ) (A | ρ) (R | ρ) (D | ρ)
Tactic:
simp [GSN_IA', GSN_IA]
State after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys (S | ρ) ((D | ρ).delete ∪ (D | ρ).modify)) ∪
            trace (restrict (R | ρ) (D | ρ)) (sliceSys (S' | ρ) ((D | ρ).add ∪ (D | ρ).modify)) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D | ρ).delete)))
      (trace (R | ρ) (D | ρ).delete)

State before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys (S | ρ) ((D | ρ).delete ∪ (D | ρ).modify)) ∪
            trace (restrict (R | ρ) (D | ρ)) (sliceSys (S' | ρ) ((D | ρ).add ∪ (D | ρ).modify)) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D | ρ).delete)))
      (trace (R | ρ) (D | ρ).delete)
Tactic:
simp [←restrict_correct]
State after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys (S | ρ) ((D | ρ).delete ∪ (D | ρ).modify)) ∪
            trace (restrict' R D | ρ) (sliceSys (S' | ρ) ((D | ρ).add ∪ (D | ρ).modify)) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D | ρ).delete)))
      (trace (R | ρ) (D | ρ).delete)

State before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys (S | ρ) ((D | ρ).delete ∪ (D | ρ).modify)) ∪
            trace (restrict' R D | ρ) (sliceSys (S' | ρ) ((D | ρ).add ∪ (D | ρ).modify)) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D | ρ).delete)))
      (trace (R | ρ) (D | ρ).delete)
Tactic:
simp [Delta_Variational, indexDelta, index_union, ←sliceSys_correct]
State after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys' S (D.delete ∪ D.modify) | ρ) ∪
            trace (restrict' R D | ρ) (sliceSys' S' (D.add ∪ D.modify) | ρ) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D.delete | ρ))))
      (trace (R | ρ) (D.delete | ρ))

State before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (trace (R | ρ) (sliceSys' S (D.delete ∪ D.modify) | ρ) ∪
            trace (restrict' R D | ρ) (sliceSys' S' (D.add ∪ D.modify) | ρ) ∪
          sliceGSN_V (A | ρ) (trace (R | ρ) (D.delete | ρ))))
      (trace (R | ρ) (D.delete | ρ))
Tactic:
simp [←trace_correct]
State after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (((trace' R (sliceSys' S (D.delete ∪ D.modify)) | ρ) ∪
            trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) | ρ) ∪
          sliceGSN_V (A | ρ) (trace' R D.delete | ρ)))
      (trace' R D.delete | ρ)

State before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        (((trace' R (sliceSys' S (D.delete ∪ D.modify)) | ρ) ∪
            trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) | ρ) ∪
          sliceGSN_V (A | ρ) (trace' R D.delete | ρ)))
      (trace' R D.delete | ρ)
Tactic:
simp [←sliceGSNV_correct, index_union]
State after:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        ((trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)) |
          ρ))
      (trace' R D.delete | ρ)

State before:
S S' : Sys'
A : GSN'
R : TraceRel'
D : Delta'
ρ : Config F
⊢ (createAnnotation' A
        (sliceGSN_R' A
          (trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)))
        (trace' R D.delete) |
      ρ) =
    createAnnotation (A | ρ)
      (sliceGSN_R (A | ρ)
        ((trace' R (sliceSys' S (D.delete ∪ D.modify)) ∪ trace' (restrict' R D) (sliceSys' S' (D.add ∪ D.modify)) ∪
            sliceGSN_V' A (trace' R D.delete)) |
          ρ))
      (trace' R D.delete | ρ)
Tactic:
simp [←sliceGSNR_correct, ←createAnnotation_correct]
State after:
no goals