Theorem: Reactor.Wellformed.shared_dep_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 : Kind
cpt : Component.Valued
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 := cpt, id := j } ∈ rcn₁.deps k
hd₂ : { cpt := cpt, id := j } ∈ rcn₂.deps k
hi : ¬i₁ = i₂
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) k { cpt := cpt, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) k { cpt := cpt, id := j }
⊢ c₁ = c₂
Tactic:
cases k <;> cases cpt <;> try cases ‹Kind›
Proof state after:
case in.inp
α : 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
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₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.inp, id := j } ∈ rcn₁.deps Kind.in
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.in
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.in { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.in { cpt := Component.Valued.inp, id := j }
⊢ c₁ = c₂

case in.out
α : 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
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₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.out, id := j } ∈ rcn₁.deps Kind.in
hd₂ : { cpt := Component.Valued.out, id := j } ∈ rcn₂.deps Kind.in
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.in { cpt := Component.Valued.out, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.in { cpt := Component.Valued.out, id := j }
⊢ c₁ = c₂

case in.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
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₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.in
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps Kind.in
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.in { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.in { cpt := Component.Valued.stv, id := j }
⊢ c₁ = c₂

case in.act
α : 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
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₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.act, id := j } ∈ rcn₁.deps Kind.in
hd₂ : { cpt := Component.Valued.act, id := j } ∈ rcn₂.deps Kind.in
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.in { cpt := Component.Valued.act, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.in { cpt := Component.Valued.act, id := j }
⊢ c₁ = c₂

case out.inp
α : 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
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₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.inp, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.inp, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.inp, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.inp, id := j }
⊢ c₁ = c₂

case out.out
α : 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
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₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.out, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.out, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.out, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.out, id := j }
⊢ c₁ = c₂

case out.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
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₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.stv, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.stv, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.stv, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.stv, id := j }
⊢ c₁ = c₂

case out.act
α : 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
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₂
hi : ¬i₁ = i₂
hd₁ : { cpt := Component.Valued.act, id := j } ∈ rcn₁.deps Kind.out
hd₂ : { cpt := Component.Valued.act, id := j } ∈ rcn₂.deps Kind.out
hv₁ : ValidDependency con₁ (Reaction.kind rcn₁) Kind.out { cpt := Component.Valued.act, id := j }
hv₂ : ValidDependency con₂ (Reaction.kind rcn₂) Kind.out { cpt := Component.Valued.act, id := j }
⊢ c₁ = c₂