Theorem: Execution.State.target_not_mem_indep_output
Proof 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
Proof 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