Theorem: Reactor.Wellformed.shared_state_local
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
⊢ c₁ = c₂
Tactic:
cases hk₁ : rcn₁.kind <;> cases hk₂ : rcn₂.kind <;> cases hk₁ ▸ hv₁ <;> cases hk₂ ▸ hv₂
Proof state after:
case mut.mut.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.mut
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.mut
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂

case mut.norm.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.mut
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂

case norm.mut.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.mut
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂

case norm.norm.stv.stv
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
wf : Wellformed rtr
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
i₁ : ID
rcn₁ : Component.type (Component.type α Component.rtr) Component.rcn
i₂ : ID
rcn₂ : Component.type (Component.type α Component.rtr) Component.rcn
k₁ k₂ : Kind
j : ID
hc₁ : rtr[Component.rtr][c₁] = some con₁
hc₂ : rtr[Component.rtr][c₂] = some con₂
hr₁ : con₁{Component.rcn}{i₁} = some rcn₁
hr₂ : con₂{Component.rcn}{i₂} = some rcn₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps k₁
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps k₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k₁ { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k₂ { cpt := Component.Valued.stv, id := j }
hk₁ : Reaction.kind rcn₁ = Reaction.Kind.norm
hk₂ : Reaction.kind rcn₂ = Reaction.Kind.norm
a✝¹ : j ∈ con₁{Component.stv}
a✝ : j ∈ con₂{Component.stv}
⊢ c₁ = c₂