Theorem: Execution.State.target_not_mem_indep_output (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
⊢ List.Forall (fun x => ¬Change.Targets x cpt i) (output s i₁)
Tactic:
apply List.forall_iff_forall_mem.mpr
State after:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
⊢ ∀ x ∈ output s i₁, ¬Change.Targets x cpt i

State before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
⊢ ∀ x ∈ output s i₁, ¬Change.Targets x cpt i
Tactic:
intro c hc
State after:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
hc : c ∈ output s i₁
⊢ ¬Change.Targets c cpt i

State before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
hc : c ∈ output s i₁
⊢ ¬Change.Targets c cpt i
Tactic:
simp [output] at hc
State after:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
hc :
  c ∈
    match s.rtr[Component.rcn][i₁], [], fun x => x.body (input s i₁) with
    | some x, x_1, f => f x
    | none, y, x => y
⊢ ¬Change.Targets c cpt i

State before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
hc :
  c ∈
    match s.rtr[Component.rcn][i₁], [], fun x => x.body (input s i₁) with
    | some x, x_1, f => f x
    | none, y, x => y
⊢ ¬Change.Targets c cpt i
Tactic:
split at hc <;> try contradiction
State after:
case h_1
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
x✝³ : Option (Component.type α Component.rcn)
x✝² : Reaction.Output
x✝¹ : Component.type α Component.rcn → Reaction.Output
x✝ : Component.type α Component.rcn
heq✝ : s.rtr[Component.rcn][i₁] = some x✝
hc : c ∈ (fun x => x.body (input s i₁)) x✝
⊢ ¬Change.Targets c cpt i

State before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ ¬Change.Targets c cpt i
Tactic:
case _ rcn₁ h₁ =>
  cases cpt
  all_goals
    intro ⟨⟩
    apply absurd hd
  case stv =>
    exact hi.no_shared_state_deps h₁ h₂ hc
  all_goals
    exact hi.left.deps_disjoint h₁ h₂ (rcn₁.target_mem_deps hc) $ by simp [Change.Normal.target]
State after:
no goals

State before:
case h_2
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
heq✝ : s.rtr[Component.rcn][i₁] = none
hc : c ∈ []
⊢ ¬Change.Targets c cpt i
Tactic:
contradiction
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ : ID
cpt : Component.Valued
i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
hd : { cpt := cpt, id := i } ∈ rcn₂.deps Kind.in
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ ¬Change.Targets c cpt i
Tactic:
cases cpt
State after:
case inp
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.inp, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.inp i

case out
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.out, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.out i

case stv
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.stv, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.stv i

case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.act i

State before:
case inp
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.inp, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.inp i

case out
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.out, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.out i

case stv
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.stv, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.stv i

case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.act i
Tactic:
all_goals
  intro ⟨⟩
  apply absurd hd
State after:
case inp
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.inp, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.inp
hc : Change.norm { cpt := Component.Valued.inp, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.inp, id := i } ∉ rcn₂.deps Kind.in

case out
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.out, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.out
hc : Change.norm { cpt := Component.Valued.out, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.out, id := i } ∉ rcn₂.deps Kind.in

case stv
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.stv, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.stv
hc : Change.norm { cpt := Component.Valued.stv, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.stv, id := i } ∉ rcn₂.deps Kind.in

case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.act, id := i } ∉ rcn₂.deps Kind.in

State before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.stv, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.stv
hc : Change.norm { cpt := Component.Valued.stv, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.stv, id := i } ∉ rcn₂.deps Kind.in
Tactic:
case stv =>
  exact hi.no_shared_state_deps h₁ h₂ hc
State after:
no goals

State before:
case inp
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.inp, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.inp
hc : Change.norm { cpt := Component.Valued.inp, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.inp, id := i } ∉ rcn₂.deps Kind.in

case out
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.out, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.out
hc : Change.norm { cpt := Component.Valued.out, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.out, id := i } ∉ rcn₂.deps Kind.in

case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.act, id := i } ∉ rcn₂.deps Kind.in
Tactic:
all_goals
  exact hi.left.deps_disjoint h₁ h₂ (rcn₁.target_mem_deps hc) $ by simp [Change.Normal.target]
State after:
no goals

State before:
case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hc : c ∈ (fun x => x.body (input s i₁)) rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
⊢ ¬Change.Targets c Component.Valued.act i
Tactic:
intro ⟨⟩
State after:
case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ False

State before:
case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ False
Tactic:
apply absurd hd
State after:
case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.act, id := i } ∉ rcn₂.deps Kind.in

State before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.stv, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.stv
hc : Change.norm { cpt := Component.Valued.stv, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.stv, id := i } ∉ rcn₂.deps Kind.in
Tactic:
exact hi.no_shared_state_deps h₁ h₂ hc
State after:
no goals

State before:
case act
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.act, id := i } ∉ rcn₂.deps Kind.in
Tactic:
exact hi.left.deps_disjoint h₁ h₂ (rcn₁.target_mem_deps hc) $ by simp [Change.Normal.target]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i₂ : Component.idType Component.rcn
rcn₂ : Component.type α Component.rcn
i₁ i : ID
h₂ : s.rtr[Component.rcn][i₂] = some rcn₂
hi : i₁ ≮[s.rtr]≯ i₂
c : Change
x✝² : Option (Component.type α Component.rcn)
x✝¹ : Reaction.Output
x✝ : Component.type α Component.rcn → Reaction.Output
rcn₁ : Component.type α Component.rcn
h₁ : s.rtr[Component.rcn][i₁] = some rcn₁
hd : { cpt := Component.Valued.act, id := i } ∈ rcn₂.deps Kind.in
v✝ : Component.Valued.changeType Component.Valued.act
hc : Change.norm { cpt := Component.Valued.act, id := i, value := v✝ } ∈ (fun x => x.body (input s i₁)) rcn₁
⊢ { cpt := Component.Valued.act, id := i }.cpt ≠ Component.Valued.stv
Tactic:
simp [Change.Normal.target]
State after:
no goals