Theorem: Execution.Progress.to_deps_acyclic (ReactorModel/Execution/Theorems/Progress.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
⊢ Dependency.Acyclic rtr
Tactic:
simp [Dependency.Acyclic.iff_mem_acyclic]
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
⊢ ∀ i ∈ rtr[Component.rcn], ¬i <[rtr] i

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
⊢ ∀ i ∈ rtr[Component.rcn], ¬i <[rtr] i
Tactic:
intro rcn hm
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
⊢ ¬rcn <[rtr] rcn

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
⊢ ¬rcn <[rtr] rcn
Tactic:
have ⟨_, e⟩ := p _ $ State.Over.forcing_not_terminal hm
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ w✝
⊢ ¬rcn <[rtr] rcn

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
cases e
State after:
case skip
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
s✝ : (State.Over.forcing rtr rcn).toState ↓ₛ w✝
⊢ ¬rcn <[rtr] rcn

case exec
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e✝ : (State.Over.forcing rtr rcn).toState ↓ₑ w✝
⊢ ¬rcn <[rtr] rcn

case time
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
t✝ : (State.Over.forcing rtr rcn).toState ↓ₜ w✝
⊢ ¬rcn <[rtr] rcn

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₜ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
case time e => exact State.Over.forcing_not_time_step e hm |>.elim
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₛ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
case skip e => exact State.Over.forcing_skip_step_rcn_eq e ▸ e.allows_rcn.acyclic
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₑ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
case exec e => exact State.Over.forcing_exec_step_rcn_eq e ▸ e.allows_rcn.acyclic
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₜ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
exact State.Over.forcing_not_time_step e hm |>.elim
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₛ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
exact State.Over.forcing_skip_step_rcn_eq e ▸ e.allows_rcn.acyclic
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
p : Progress rtr
rcn : Component.idType Component.rcn
hm : rcn ∈ rtr[Component.rcn]
w✝ : State α
e : (State.Over.forcing rtr rcn).toState ↓ₑ w✝
⊢ ¬rcn <[rtr] rcn
Tactic:
exact State.Over.forcing_exec_step_rcn_eq e ▸ e.allows_rcn.acyclic
State after:
no goals