Theorem: Execution.Step.Apply.RTC.preserves_unchanged (ReactorModel/Execution/Theorems/Step/Apply.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ -[out]→ s₂
h : List.Forall (fun x => ¬Change.Targets x cpt i) out
⊢ s₁.rtr[Component.val cpt][i] = s₂.rtr[Component.val cpt][i]
Tactic:
induction e
State after:
case refl
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
s✝ : State α
h : List.Forall (fun x => ¬Change.Targets x cpt i) []
⊢ s✝.rtr[Component.val cpt][i] = s✝.rtr[Component.val cpt][i]

case trans
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
a✝¹ : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
a_ih✝ :
  List.Forall (fun x => ¬Change.Targets x cpt i) tl✝ → s₂✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
h : List.Forall (fun x => ¬Change.Targets x cpt i) (hd✝ :: tl✝)
⊢ s₁✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
s✝ : State α
h : List.Forall (fun x => ¬Change.Targets x cpt i) []
⊢ s✝.rtr[Component.val cpt][i] = s✝.rtr[Component.val cpt][i]
Tactic:
case refl => rfl
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝ → s₂✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
h : List.Forall (fun x => ¬Change.Targets x cpt i) (hd✝ :: tl✝)
⊢ s₁✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
Tactic:
case trans e _ hi =>
  have ⟨hh, ht⟩ := List.forall_cons _ _ _ |>.mp h
  exact e.preserves_unchanged hh ▸ hi ht
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
s✝ : State α
h : List.Forall (fun x => ¬Change.Targets x cpt i) []
⊢ s✝.rtr[Component.val cpt][i] = s✝.rtr[Component.val cpt][i]
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝ → s₂✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
h : List.Forall (fun x => ¬Change.Targets x cpt i) (hd✝ :: tl✝)
⊢ s₁✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
Tactic:
have ⟨hh, ht⟩ := List.forall_cons _ _ _ |>.mp h
State after:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝ → s₂✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
h : List.Forall (fun x => ¬Change.Targets x cpt i) (hd✝ :: tl✝)
hh : ¬Change.Targets hd✝ cpt i
ht : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝
⊢ s₁✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
out : Reaction.Output
s₂ : State α
i : ID
cpt : Component.Valued
hd✝ : Change
s₁✝ s₂✝ : State α
tl✝ : Reaction.Output
s₃✝ : State α
e : s₁✝ -[hd✝]→ s₂✝
a✝ : s₂✝ -[tl✝]→ s₃✝
hi : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝ → s₂✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
h : List.Forall (fun x => ¬Change.Targets x cpt i) (hd✝ :: tl✝)
hh : ¬Change.Targets hd✝ cpt i
ht : List.Forall (fun x => ¬Change.Targets x cpt i) tl✝
⊢ s₁✝.rtr[Component.val cpt][i] = s₃✝.rtr[Component.val cpt][i]
Tactic:
exact e.preserves_unchanged hh ▸ hi ht
State after:
no goals