internlm/Lean-Github huggingface dataset:
Theorem: Execution.Step.Apply.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂ s₂' s₁₂ s₂₁ : State α
c : Change
e : s₁ -[c]→ s₂
⊢ s₁.rtr ≈ s₂.rtr
Tactic:
cases e
Proof state after:
case inp
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr

case out
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr

case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr

case act
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ s₁.rtr ≈ (schedule s₁ i✝ t✝ v✝).rtr

case mut
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
x✝ : Change.Mutation
⊢ s₁.rtr ≈ s₁.rtr
Theorem: Execution.Step.Apply.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
x✝ : Change.Mutation
⊢ s₁.rtr ≈ s₁.rtr
Tactic:
case «mut» => exact .refl _
Proof state after:
no goals
Theorem: Execution.Step.Apply.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ s₁.rtr ≈ (schedule s₁ i✝ t✝ v✝).rtr
Tactic:
case act => simp [schedule_preserves_rtr]; exact .refl _
Proof state after:
no goals
Theorem: Execution.Step.Apply.equiv
Proof state before:
case inp
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr

case out
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr

case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr
Tactic:
all_goals exact LawfulUpdate.equiv ‹_›
Proof state after:
no goals
Theorem: Execution.Step.Apply.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
x✝ : Change.Mutation
⊢ s₁.rtr ≈ s₁.rtr
Tactic:
exact .refl _
Proof state after:
no goals
Theorem: Execution.Step.Apply.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ s₁.rtr ≈ (schedule s₁ i✝ t✝ v✝).rtr
Tactic:
simp [schedule_preserves_rtr]
Proof state after:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ s₁.rtr ≈ s₁.rtr
Theorem: Execution.Step.Apply.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ s₁.rtr ≈ s₁.rtr
Tactic:
exact .refl _
Proof state after:
no goals
Theorem: Execution.Step.Apply.equiv
Proof state before:
case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
i✝ : ID
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr ≈ { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr
Tactic:
exact LawfulUpdate.equiv ‹_›
Proof state after:
no goals
Theorem: Execution.Step.Apply.preserves_unchanged
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂ s₂' s₁₂ s₂₁ : State α
c : Change
cpt : Component.Valued
i : ID
e : s₁ -[c]→ s₂
h : ¬Change.Targets c cpt i
⊢ s₁.rtr[Component.val cpt][i] = s₂.rtr[Component.val cpt][i]
Tactic:
cases e <;> try exact .refl _
Proof state after:
case inp
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.inp i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]

case out
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.out i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]

case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.stv i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]
Theorem: Execution.Step.Apply.preserves_unchanged
Proof state before:
case inp
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.inp i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]

case out
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.out i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]

case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.stv i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]
Tactic:
all_goals simp [LawfulUpdate.obj?_preserved (Change.Targets.norm_not h) ‹_›]
Proof state after:
no goals
Theorem: Execution.Step.Apply.preserves_unchanged
Proof state before:
case mut
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i : ID
x✝ : Change.Mutation
h : ¬Change.Targets (Change.mut x✝) cpt i
⊢ s₁.rtr[Component.val cpt][i] = s₁.rtr[Component.val cpt][i]
Tactic:
exact .refl _
Proof state after:
no goals
Theorem: Execution.Step.Apply.preserves_unchanged
Proof state before:
case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.stv i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]
Tactic:
simp [LawfulUpdate.obj?_preserved (Change.Targets.norm_not h) ‹_›]
Proof state after:
no goals
Theorem: Execution.Step.Apply.events_congr
Proof state before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂ s₂' s₁₂ s₂₁ : State α
c : Change
e : s₁ -[c]→ s₂
e' : s₁' -[c]→ s₂'
he : s₁.events = s₁'.events
⊢ s₂.events = s₂'.events
Tactic:
cases e <;> cases e' <;> simp [he]
Proof state after:
case act.act
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₁₂ s₂₁ : State α
he : s₁.events = s₁'.events
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ (schedule s₁ i✝ t✝ v✝).events = (schedule s₁' i✝ t✝ v✝).events
Theorem: Execution.Step.Apply.events_congr
Proof state before:
case act.act
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₁₂ s₂₁ : State α
he : s₁.events = s₁'.events
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ (schedule s₁ i✝ t✝ v✝).events = (schedule s₁' i✝ t✝ v✝).events
Tactic:
exact schedule_events_congr he
Proof state after:
no goals
Theorem: Execution.Step.Apply.rtr_congr
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
s₁' s₂' : State α
e : s₁ -[c]→ s₂
e' : s₁' -[c]→ s₂'
h : s₁.rtr = s₁'.rtr
⊢ s₂.rtr = s₂'.rtr
Tactic:
cases e <;> cases e' <;> simp [State.schedule_preserves_rtr, h]
Proof state after:
case inp.inp
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝

case out.out
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝

case stv.stv
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝
Theorem: Execution.Step.Apply.rtr_congr
Proof state before:
case inp.inp
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝

case out.out
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝

case stv.stv
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝
Tactic:
all_goals rw [h] at *; exact LawfulUpdate.unique ‹_› ‹_›
Proof state after:
no goals
Theorem: Execution.Step.Apply.rtr_congr
Proof state before:
case stv.stv
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝
Tactic:
rw [h] at *
Proof state after:
case stv.stv
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁'.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝
Theorem: Execution.Step.Apply.rtr_congr
Proof state before:
case stv.stv
α : Type
inst✝ : Readable α
s s₁ s₁' : State α
h : s₁'.rtr = s₁'.rtr
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁'.rtr rtr✝
⊢ rtr✝¹ = rtr✝
Tactic:
exact LawfulUpdate.unique ‹_› ‹_›
Proof state after:
no goals
Theorem: Execution.Step.Apply.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ record s₁ rcn = s₂
Tactic:
ext1
Proof state after:
case rtr
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).rtr = s₂.rtr

case tag
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).tag = s₂.tag

case progress
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).progress = s₂.progress

case events
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).events = s₂.events
Theorem: Execution.Step.Apply.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).rtr = s₂.rtr
Tactic:
case rtr      => exact e₁.rtr_congr e₂ (s.record_preserves_rtr rcn)
Proof state after:
no goals
Theorem: Execution.Step.Apply.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).tag = s₂.tag
Tactic:
case tag      => simp [record_preserves_tag, ←e₁.preserves_tag, ←e₂.preserves_tag]
Proof state after:
no goals
Theorem: Execution.Step.Apply.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).progress = s₂.progress
Tactic:
case progress => simp [record_progress_eq, ←e₂.preserves_progress, e₁.preserves_progress]
Proof state after:
no goals
Theorem: Execution.Step.Apply.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).events = s₂.events
Tactic:
case events   => exact e₁.events_congr e₂ (s.record_preserves_events rcn)
Proof state after:
no goals
Theorem: Execution.Step.Apply.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).rtr = s₂.rtr
Tactic:
exact e₁.rtr_congr e₂ (s.record_preserves_rtr rcn)
Proof state after:
no goals
Theorem: Execution.Step.Apply.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).tag = s₂.tag
Tactic:
simp [record_preserves_tag, ←e₁.preserves_tag, ←e₂.preserves_tag]
Proof state after:
no goals
Theorem: Execution.Step.Apply.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).progress = s₂.progress
Tactic:
simp [record_progress_eq, ←e₂.preserves_progress, e₁.preserves_progress]
Proof state after:
no goals
Theorem: Execution.Step.Apply.comm_record
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
rcn : ID
e₁ : s -[c]→ s₁
e₂ : (record s rcn) -[c]→ s₂
⊢ (record s₁ rcn).events = s₂.events
Tactic:
exact e₁.events_congr e₂ (s.record_preserves_events rcn)
Proof state after:
no goals
Theorem: Execution.Step.Apply.deterministic
Proof state before:
α : Type
inst✝ : Readable α
s s₁ s₂ : State α
c : Change
e₁ : s -[c]→ s₁
e₂ : s -[c]→ s₂
⊢ s₁ = s₂
Tactic:
cases e₁ <;> cases e₂ <;> simp <;> exact LawfulUpdate.unique ‹_› ‹_›
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝¹ : _root_.Time
v✝¹ : Value
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : ¬i✝¹ = i✝
⊢ schedule (schedule s i✝¹ t✝¹ v✝¹) i✝ t✝ v✝ = schedule (schedule s i✝ t✝ v✝) i✝¹ t✝¹ v✝¹
Tactic:
case act.act.act.act =>               exact schedule_ne_comm ht
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
case inp.act.act.inp u₁ _ _ _ _ u₂ => cases LawfulUpdate.unique u₁ u₂; rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
case out.act.act.out u₁ _ _ _ _ u₂ => cases LawfulUpdate.unique u₁ u₂; rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
case stv.act.act.stv u₁ _ _ _ _ u₂ => cases LawfulUpdate.unique u₁ u₂; rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.inp i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
case act.inp.inp.act u₁ _ u₂       => cases LawfulUpdate.unique u₁ u₂; rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
case act.out.out.act u₁ _ u₂       => cases LawfulUpdate.unique u₁ u₂; rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.stv i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
case act.stv.stv.act u₁ _ u₂       => cases LawfulUpdate.unique u₁ u₂; rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝¹ : _root_.Time
v✝¹ : Value
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : ¬i✝¹ = i✝
⊢ schedule (schedule s i✝¹ t✝¹ v✝¹) i✝ t✝ v✝ = schedule (schedule s i✝ t✝ v✝) i✝¹ t✝¹ v✝¹
Tactic:
exact schedule_ne_comm ht
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
cases LawfulUpdate.unique u₁ u₂
Proof state after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
cases LawfulUpdate.unique u₁ u₂
Proof state after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
rfl
Proof state after:
no goals
Theorem: Execution.Step.Apply.ne_target_comm
Proof state before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
cases LawfulUpdate.unique u₁ u₂
Proof state after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }