Theorem: Dependency.same_con_needOrderedPriority
Proof state before:
case pos
α : Type
inst✝ : Proper α
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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case neg
α : Type
inst✝ : Proper α
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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case pos
α : Type
inst✝ : Proper α
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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case neg
α : Type
inst✝ : Proper α
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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁
Tactic:
rotate_left
Proof state after:
case neg
α : Type
inst✝ : Proper α
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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case pos
α : Type
inst✝ : Proper α
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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case neg
α : Type
inst✝ : Proper α
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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : ¬Reaction.Mutates rcn₁
hm₂ : ¬Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁

case pos
α : Type
inst✝ : Proper α
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
hc : rtr[Component.rtr][c] = some con
h₁ : con{Component.rcn}{i₁} = some rcn₁
h₂ : con{Component.rcn}{i₂} = some rcn₂
hn : i₁ ≠ i₂
hp : Wellformed.NeedOrderedPriority rcn₁ rcn₂
hm₁ : Reaction.Mutates rcn₁
hm₂ : Reaction.Mutates rcn₂
⊢ (i₁ <[rtr] i₂) ∨ i₂ <[rtr] i₁