Theorem: Execution.State.Allows.iff_record_indep (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
⊢ Allows s i₂ ↔ Allows (record s i₁) i₂
Tactic:
simp [record, Allows.def]
State after:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
⊢ i₂ ∈ s.rtr[Component.rcn] →
    (dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress ↔
      dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
⊢ i₂ ∈ s.rtr[Component.rcn] →
    (dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress ↔
      dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress)
Tactic:
intro _
State after:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
⊢ dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress ↔
    dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
⊢ dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress ↔
    dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress
Tactic:
constructor <;> intro ⟨hd, hp⟩
State after:
case mp
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress

case mpr
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
hp : i₂ ∉ Set.insert i₁ s.progress
⊢ dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress ∧ i₂ ∉ Set.insert i₁ s.progress
Tactic:
constructor
State after:
case left
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress

case right
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ i₂ ∉ Set.insert i₁ s.progress

State before:
case left
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
Tactic:
exact hd.trans $ Set.subset_insert i₁ s.progress
State after:
no goals

State before:
case right
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ s.progress
hp : i₂ ∉ s.progress
⊢ i₂ ∉ Set.insert i₁ s.progress
Tactic:
exact Set.mem_insert_iff.not.mpr $ not_or.mpr ⟨hi.not_eq.symm, hp⟩
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
hp : i₂ ∉ Set.insert i₁ s.progress
⊢ dependencies s.rtr i₂ ⊆ s.progress ∧ i₂ ∉ s.progress
Tactic:
constructor
State after:
case left
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
hp : i₂ ∉ Set.insert i₁ s.progress
⊢ dependencies s.rtr i₂ ⊆ s.progress

case right
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
hp : i₂ ∉ Set.insert i₁ s.progress
⊢ i₂ ∉ s.progress

State before:
case right
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i₁ i₂ : ID
hi : i₁ ≮[s.rtr]≯ i₂
a✝ : i₂ ∈ s.rtr[Component.rcn]
hd : dependencies s.rtr i₂ ⊆ Set.insert i₁ s.progress
hp : i₂ ∉ Set.insert i₁ s.progress
⊢ i₂ ∉ s.progress
Tactic:
exact not_or.mp (Set.mem_insert_iff.not.mp hp) |>.right
State after:
no goals