Theorem: Execution.Grouped.deterministic (ReactorModel/Execution/Theorems/Grouped/Basic.lean)

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
n : State.Nontrivial s
ht : s₁.tag = s₂.tag
hp : s₁.progress = s₂.progress
tl₁ : State α
steps₁ : Steps s tl₁
tail₁ : Tail tl₁ s₁
tl₂ : State α
steps₂ : Steps s tl₂
tail₂ : Tail tl₂ s₂
⊢ s₁ = s₂
Tactic:
replace ht : tl₁.tag = tl₂.tag := tail₁.preserves_tag ▸ ht ▸ tail₂.preserves_tag.symm
State after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
n : State.Nontrivial s
hp : s₁.progress = s₂.progress
tl₁ : State α
steps₁ : Steps s tl₁
tail₁ : Tail tl₁ s₁
tl₂ : State α
steps₂ : Steps s tl₂
tail₂ : Tail tl₂ s₂
ht : tl₁.tag = tl₂.tag
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
n : State.Nontrivial s
hp : s₁.progress = s₂.progress
tl₁ : State α
steps₁ : Steps s tl₁
tail₁ : Tail tl₁ s₁
tl₂ : State α
steps₂ : Steps s tl₂
tail₂ : Tail tl₂ s₂
ht : tl₁.tag = tl₂.tag
⊢ s₁ = s₂
Tactic:
induction steps₁ <;> cases steps₂
State after:
case refl.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
n : State.Nontrivial tl₂
tail₁ : Tail tl₂ s₁
ht : tl₂.tag = tl₂.tag
⊢ s₁ = s₂

case refl.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Step s✝ s₂✝
a✝ : Steps s₂✝ tl₂
⊢ s₁ = s₂

case step.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
a✝ : Step tl₂ s₂✝
n : State.Nontrivial tl₂
⊢ s₁ = s₂

case step.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₁✝ s₂✝¹ s₃✝ : State α
a✝³ : Step s₁✝ s₂✝¹
a✝² : Steps s₂✝¹ s₃✝
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
n : State.Nontrivial s₁✝
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Step s₁✝ s₂✝
a✝ : Steps s₂✝ tl₂
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
n : State.Nontrivial tl₂
tail₁ : Tail tl₂ s₁
ht : tl₂.tag = tl₂.tag
⊢ s₁ = s₂
Tactic:
case refl.refl => exact tail₁.deterministic hp tail₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₁✝ s₂✝¹ s₃✝ : State α
e₁ : Step s₁✝ s₂✝¹
a✝ : Steps s₂✝¹ s₃✝
hi : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
n : State.Nontrivial s₁✝
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
s₂✝ : State α
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ tl₂
⊢ s₁ = s₂
Tactic:
case step.step e₁ _ hi _ e₂ e₂' => 
  cases e₁.deterministic e₂
  exact hi (e₁.preserves_nontrivial n) tail₁ e₂' ht
State after:
no goals

State before:
case refl.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Step s✝ s₂✝
a✝ : Steps s₂✝ tl₂
⊢ s₁ = s₂

case step.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
a✝ : Step tl₂ s₂✝
n : State.Nontrivial tl₂
⊢ s₁ = s₂
Tactic:
all_goals cases ‹Step _ _›
State after:
case refl.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Steps s₂✝ tl₂
a✝ : s✝ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case refl.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Steps s₂✝ tl₂
a✝ : s✝ ↓ₜ s₂✝
⊢ s₁ = s₂

case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case step.refl.time
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ₜ s₂✝
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
e' : Steps s₂✝ tl₂
e : s✝ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
case refl.step.time e' e   => exact absurd ht $ ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
e' : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
e : tl₂ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
case step.refl.time e' _ e => exact absurd ht.symm $ ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le
State after:
no goals

State before:
case refl.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
a✝¹ : Steps s₂✝ tl₂
a✝ : s✝ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ᵢ| s₂✝
⊢ s₁ = s₂
Tactic:
all_goals cases ‹Steps _ _›
State after:
case refl.step.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
a✝ : s✝ ↓ᵢ| tl₂
⊢ s₁ = s₂

case refl.step.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ tl₂
⊢ s₁ = s₂

case step.refl.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ : State α
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ᵢ| s₂✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₂✝ s₁ → Steps s₂✝ tl₂ → s₂✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₂✝ s₁
ht : s₂✝.tag = tl₂.tag
⊢ s₁ = s₂

case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₃✝
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
e : s✝ ↓ᵢ| tl₂
⊢ s₁ = s₂
Tactic:
case refl.step.inst.refl e =>
  cases tail₂.closed_to_none e.closed
  cases tail₁
  case none   => exact absurd hp $ ne_of_ssubset e.progress_ssubset
  case some f => exact f.deterministic e.exec hp
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ : State α
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₂✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₂✝ s₁ → Steps s₂✝ tl₂ → s₂✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₂✝ s₁
ht : s₂✝.tag = tl₂.tag
⊢ s₁ = s₂
Tactic:
case step.refl.inst.refl e _  =>
  cases tail₁.closed_to_none e.closed
  cases tail₂
  case none   => exact absurd hp.symm $ ne_of_ssubset e.progress_ssubset
  case some f => exact e.exec.deterministic f hp
State after:
no goals

State before:
case refl.step.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ tl₂
⊢ s₁ = s₂

case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₃✝
⊢ s₁ = s₂
Tactic:
all_goals cases ‹Step _ _›
State after:
case refl.step.inst.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ tl₂
a✝ : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case refl.step.inst.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
a✝² : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ tl₂
a✝ : s₂✝¹ ↓ₜ s₂✝
⊢ s₁ = s₂

case step.refl.inst.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case step.refl.inst.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ₜ s₂✝
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ tl₂
f : s₂✝¹ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
case refl.step.inst.step.time e _ f' f => exact absurd ht $ ne_of_lt $ e.preserves_tag ▸ lt_of_lt_of_le f.tag_lt f'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
case step.refl.inst.step.time e _ f' f => exact absurd ht.symm $ ne_of_lt $ e.preserves_tag ▸ lt_of_lt_of_le f.tag_lt f'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ tl₂
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂
Tactic:
case refl.step.inst.step.inst e _ f' f => exact e.nonrepeatable f |>.elim
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂
Tactic:
case step.refl.inst.step.inst e _ f' f => exact e.nonrepeatable f |>.elim
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
n : State.Nontrivial tl₂
tail₁ : Tail tl₂ s₁
ht : tl₂.tag = tl₂.tag
⊢ s₁ = s₂
Tactic:
exact tail₁.deterministic hp tail₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₁✝ s₂✝¹ s₃✝ : State α
e₁ : Step s₁✝ s₂✝¹
a✝ : Steps s₂✝¹ s₃✝
hi : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
n : State.Nontrivial s₁✝
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
s₂✝ : State α
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ tl₂
⊢ s₁ = s₂
Tactic:
cases e₁.deterministic e₂
State after:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₁✝ s₂✝ s₃✝ : State α
e₁ : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₃✝
hi : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
n : State.Nontrivial s₁✝
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ tl₂
⊢ s₁ = s₂

State before:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₁✝ s₂✝ s₃✝ : State α
e₁ : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₃✝
hi : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
n : State.Nontrivial s₁✝
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
e₂ : Step s₁✝ s₂✝
e₂' : Steps s₂✝ tl₂
⊢ s₁ = s₂
Tactic:
exact hi (e₁.preserves_nontrivial n) tail₁ e₂' ht
State after:
no goals

State before:
case step.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
a✝ : Step tl₂ s₂✝
n : State.Nontrivial tl₂
⊢ s₁ = s₂
Tactic:
cases ‹Step _ _›
State after:
case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case step.refl.time
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ₜ s₂✝
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝ : State α
e' : Steps s₂✝ tl₂
e : s✝ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
exact absurd ht $ ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
e' : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
e : tl₂ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
exact absurd ht.symm $ ne_of_lt $ lt_of_lt_of_le e.tag_lt e'.tag_le
State after:
no goals

State before:
case step.refl.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ s₃✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₃✝ s₁ → Steps s₂✝ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ᵢ| s₂✝
⊢ s₁ = s₂
Tactic:
cases ‹Steps _ _›
State after:
case step.refl.inst.refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ : State α
n : State.Nontrivial tl₂
a✝ : tl₂ ↓ᵢ| s₂✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₂✝ s₁ → Steps s₂✝ tl₂ → s₂✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₂✝ s₁
ht : s₂✝.tag = tl₂.tag
⊢ s₁ = s₂

case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₃✝
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
e : s✝ ↓ᵢ| tl₂
⊢ s₁ = s₂
Tactic:
cases tail₂.closed_to_none e.closed
State after:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
tail₂ : Tail s₂ s₂
ht : s✝.tag = s₂.tag
e : s✝ ↓ᵢ| s₂
⊢ s₁ = s₂

State before:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
tail₂ : Tail s₂ s₂
ht : s✝.tag = s₂.tag
e : s✝ ↓ᵢ| s₂
⊢ s₁ = s₂
Tactic:
cases tail₁
State after:
case refl.none
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ : State α
tail₂ : Tail s₂ s₂
n : State.Nontrivial s₁
ht : s₁.tag = s₂.tag
e : s₁ ↓ᵢ| s₂
⊢ s₁ = s₂

case refl.some
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ s✝ : State α
n : State.Nontrivial s✝
tail₂ : Tail s₂ s₂
ht : s✝.tag = s₂.tag
e : s✝ ↓ᵢ| s₂
a✝ : s✝ ↓ᵢ+ s₁
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ : State α
tail₂ : Tail s₂ s₂
n : State.Nontrivial s₁
ht : s₁.tag = s₂.tag
e : s₁ ↓ᵢ| s₂
⊢ s₁ = s₂
Tactic:
case none   => exact absurd hp $ ne_of_ssubset e.progress_ssubset
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ s✝ : State α
n : State.Nontrivial s✝
tail₂ : Tail s₂ s₂
ht : s✝.tag = s₂.tag
e : s✝ ↓ᵢ| s₂
f : s✝ ↓ᵢ+ s₁
⊢ s₁ = s₂
Tactic:
case some f => exact f.deterministic e.exec hp
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ : State α
tail₂ : Tail s₂ s₂
n : State.Nontrivial s₁
ht : s₁.tag = s₂.tag
e : s₁ ↓ᵢ| s₂
⊢ s₁ = s₂
Tactic:
exact absurd hp $ ne_of_ssubset e.progress_ssubset
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ s✝ : State α
n : State.Nontrivial s✝
tail₂ : Tail s₂ s₂
ht : s✝.tag = s₂.tag
e : s✝ ↓ᵢ| s₂
f : s✝ ↓ᵢ+ s₁
⊢ s₁ = s₂
Tactic:
exact f.deterministic e.exec hp
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝ : State α
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₂✝
a_ih✝ : State.Nontrivial s₂✝ → Tail s₂✝ s₁ → Steps s₂✝ tl₂ → s₂✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₂✝ s₁
ht : s₂✝.tag = tl₂.tag
⊢ s₁ = s₂
Tactic:
cases tail₁.closed_to_none e.closed
State after:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ tl₂ → s₁.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₁ s₁
ht : s₁.tag = tl₂.tag
⊢ s₁ = s₂

State before:
case refl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ tl₂ → s₁.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₁ s₁
ht : s₁.tag = tl₂.tag
⊢ s₁ = s₂
Tactic:
cases tail₂
State after:
case refl.none
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ : State α
tail₁ : Tail s₁ s₁
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ s₂ → s₁.tag = s₂.tag → s₁ = s₂
ht : s₁.tag = s₂.tag
⊢ s₁ = s₂

case refl.some
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ tl₂ → s₁.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₁ s₁
ht : s₁.tag = tl₂.tag
a✝ : tl₂ ↓ᵢ+ s₂
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ : State α
tail₁ : Tail s₁ s₁
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ s₂ → s₁.tag = s₂.tag → s₁ = s₂
ht : s₁.tag = s₂.tag
⊢ s₁ = s₂
Tactic:
case none   => exact absurd hp.symm $ ne_of_ssubset e.progress_ssubset
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ tl₂ → s₁.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₁ s₁
ht : s₁.tag = tl₂.tag
f : tl₂ ↓ᵢ+ s₂
⊢ s₁ = s₂
Tactic:
case some f => exact e.exec.deterministic f hp
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ : State α
tail₁ : Tail s₁ s₁
n : State.Nontrivial s₂
e : s₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ s₂ → s₁.tag = s₂.tag → s₁ = s₂
ht : s₁.tag = s₂.tag
⊢ s₁ = s₂
Tactic:
exact absurd hp.symm $ ne_of_ssubset e.progress_ssubset
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₁
a_ih✝ : State.Nontrivial s₁ → Tail s₁ s₁ → Steps s₁ tl₂ → s₁.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₁ s₁
ht : s₁.tag = tl₂.tag
f : tl₂ ↓ᵢ+ s₂
⊢ s₁ = s₂
Tactic:
exact e.exec.deterministic f hp
State after:
no goals

State before:
case step.refl.inst.step
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Step s₂✝¹ s₂✝
a✝ : Steps s₂✝ s₃✝
⊢ s₁ = s₂
Tactic:
cases ‹Step _ _›
State after:
case step.refl.inst.step.inst
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂

case step.refl.inst.step.time
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
a✝² : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
a✝¹ : Steps s₂✝ s₃✝
a✝ : s₂✝¹ ↓ₜ s₂✝
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ tl₂
f : s₂✝¹ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
exact absurd ht $ ne_of_lt $ e.preserves_tag ▸ lt_of_lt_of_le f.tag_lt f'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ₜ s₂✝
⊢ s₁ = s₂
Tactic:
exact absurd ht.symm $ ne_of_lt $ e.preserves_tag ▸ lt_of_lt_of_le f.tag_lt f'.tag_le
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s✝ : State α
n : State.Nontrivial s✝
tail₁ : Tail s✝ s₁
ht : s✝.tag = tl₂.tag
s₂✝¹ : State α
e : s✝ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ tl₂
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂
Tactic:
exact e.nonrepeatable f |>.elim
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
hp : s₁.progress = s₂.progress
tl₁ tl₂ : State α
tail₂ : Tail tl₂ s₂
s₂✝¹ s₃✝ : State α
a_ih✝ : State.Nontrivial s₂✝¹ → Tail s₃✝ s₁ → Steps s₂✝¹ tl₂ → s₃✝.tag = tl₂.tag → s₁ = s₂
tail₁ : Tail s₃✝ s₁
ht : s₃✝.tag = tl₂.tag
n : State.Nontrivial tl₂
e : tl₂ ↓ᵢ| s₂✝¹
s₂✝ : State α
f' : Steps s₂✝ s₃✝
f : s₂✝¹ ↓ᵢ| s₂✝
⊢ s₁ = s₂
Tactic:
exact e.nonrepeatable f |>.elim
State after:
no goals