import Mt.System.Basic
import Mt.System.BasicAux
import Mt.System.Traced
import Mt.Utils.List

namespace Mt.System

variable {spec: Spec
spec : Spec: Type 1
Spec}
local instance: {spec : Spec} → IsReservation spec.Reservation
instance : IsReservation: Type → Type
IsReservation spec: Spec
spec.Reservation: Spec → Type
Reservation :=spec: Spec
spec.is_reservation: (self : Spec) → IsReservation self.Reservation
is_reservation

open Utils

/-- Central validation predicate for reasoning about systems.

  A valid system has the following property: Given any future
  iteration of the system (or the system itself), the following
  holds:
  * No threads have panicked yet (and they never will)
  * Its current state is valid according to the specification
-/
def valid: {spec : Spec} → System spec → Prop
valid (s: System spec
s : System: Spec → Type 1
System spec: Spec
spec) : Prop: Type
Prop :=
  ∀ s': System spec
s' : System: Spec → Type 1
System spec: Spec
spec, s: System spec
s.reduces_to_or_eq: {spec : Spec} → System spec → System spec → Prop
reduces_to_or_eq s': System spec
s' →
  s': System spec
s'.panics: {spec : Spec} → System spec → Nat
panics = 0: ?m.45
0 ∧ ∃ r: ?m.66
r, spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate r: ?m.66
r s': System spec
s'.state: {spec : Spec} → System spec → spec.State
state

theorem fundamental_validation_theorem: ∀ (s : System spec),
  s.panics = 0 →
    Spec.validate spec IsReservation.empty s.state → (∀ (t : Thread spec), t ∈ s.threads → Thread.valid t) → valid s
fundamental_validation_theorem (s: System spec
s : System: Spec → Type 1
System spec: Spec
spec)
  (no_panics_yet: s.panics = 0
no_panics_yet : s: System spec
s.panics: {spec : Spec} → System spec → Nat
panics = 0: ?m.92
0)
  (initial_valid: Spec.validate spec IsReservation.empty s.state
initial_valid : spec: Spec
spec.validate: (self : Spec) → self.Reservation → self.State → Prop
validate IsReservation.empty: {T : Type} → [self : IsReservation T] → T
IsReservation.empty s: System spec
s.state: {spec : Spec} → System spec → spec.State
state)
  (threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t
threads_valid : ∀ t: ?m.123
t, t: ?m.123
t ∈ s: System spec
s.threads: {spec : Spec} → System spec → List (Thread spec)
threads → t: ?m.123
t.valid: {spec : Spec} → Thread spec → Prop
valid)
  : s: System spec
s.valid: {spec : Spec} → System spec → Prop
valid :=by
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid sintro s': System spec
s' s_to_s': reduces_to_or_eq s s'
s_to_s'spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

s_to_s': reduces_to_or_eq s s'

s'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid scases s_to_s': reduces_to_or_eq s s'
s_to_s'spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

inls'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

inrs'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

s_to_s': reduces_to_or_eq s s'

s'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state<;>spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

inls'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

inrs'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

s_to_s': reduces_to_or_eq s s'

s'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.staterename_i h: ?m.193
hspec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: s = s'

inls'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid s.spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: s = s'

inls'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: s = s'

inls'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

inrs'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.staterw [spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: s = s'

inls'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state<- h: ?m.192
hspec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: s = s'

inls.panics = 0 ∧ ∃ r, Spec.validate spec r s.state]spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: s = s'

inls.panics = 0 ∧ ∃ r, Spec.validate spec r s.state
    spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: s = s'

inls'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state
spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

inrs'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.stateexact ⟨no_panics_yet: s.panics = 0
no_panics_yet, IsReservation.empty: {T : Type} → [self : IsReservation T] → T
IsReservation.empty, initial_valid: Spec.validate spec IsReservation.empty s.state
initial_valid⟩
Goals accomplished! 🐙
  
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid slet traced: ?m.267
traced := Traced.TracedSystem.mk_initial: {spec : Spec} → System spec → Traced.TracedSystem spec
Traced.TracedSystem.mk_initial s: System spec
sspec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

inrs'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid shave traced_valid: Traced.TracedSystem.valid traced
traced_valid : traced: ?m.267
traced.valid: {spec : Spec} → Traced.TracedSystem spec → Prop
valid :=
    Traced.TracedSystem.mk_initial.valid: ∀ {spec : Spec} (s : System spec),
  Spec.validate spec IsReservation.empty s.state →
    (∀ (t : Thread spec), t ∈ s.threads → Thread.valid t) → Traced.TracedSystem.valid (Traced.TracedSystem.mk_initial s)
Traced.TracedSystem.mk_initial.valid s: System spec
s initial_valid: Spec.validate spec IsReservation.empty s.state
initial_valid threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t
threads_validspec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

inrs'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state
  
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid ssuffices ∃ ts: Traced.TracedSystem spec
ts : Traced.TracedSystem: Spec → Type 1
Traced.TracedSystem spec: Spec
spec, ts: Traced.TracedSystem spec
ts.to_system: {spec : Spec} → Traced.TracedSystem spec → System spec
to_system = s': System spec
s' ∧ ts: Traced.TracedSystem spec
ts.valid: {spec : Spec} → Traced.TracedSystem spec → Prop
valid by
    spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

inrs'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.statecases this: ∃ ts, Traced.TracedSystem.to_system ts = s' ∧ Traced.TracedSystem.valid ts
thisspec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

w✝: Traced.TracedSystem spec

intros'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state
    spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

this: ∃ ts, Traced.TracedSystem.to_system ts = s' ∧ Traced.TracedSystem.valid ts

s'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.staterename_i ts: ?m.335
ts ts_hyp: ?m.336 ts
ts_hypspec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

ts: Traced.TracedSystem spec

ts_hyp: Traced.TracedSystem.to_system ts = s' ∧ Traced.TracedSystem.valid ts

intros'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.state
    spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

this: ∃ ts, Traced.TracedSystem.to_system ts = s' ∧ Traced.TracedSystem.valid ts

s'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.statesimp only [<- ts_hyp: ?m.336 ts
ts_hyp.left: ∀ {a b : Prop}, a ∧ b → a
left, Traced.TracedSystem.to_system: {spec : Spec} → Traced.TracedSystem spec → System spec
Traced.TracedSystem.to_system, true_and: ∀ (p : Prop), (True ∧ p) = p
true_and]spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

ts: Traced.TracedSystem spec

ts_hyp: Traced.TracedSystem.to_system ts = s' ∧ Traced.TracedSystem.valid ts

intro∃ r, Spec.validate spec r ts.state
    spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

this: ∃ ts, Traced.TracedSystem.to_system ts = s' ∧ Traced.TracedSystem.valid ts

s'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.stateexists ts: ?m.335
ts.reservations: {spec : Spec} → Traced.TracedSystem spec → spec.Reservation
reservationsspec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

ts: Traced.TracedSystem spec

ts_hyp: Traced.TracedSystem.to_system ts = s' ∧ Traced.TracedSystem.valid ts

introSpec.validate spec (Traced.TracedSystem.reservations ts) ts.state
    spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

this: ∃ ts, Traced.TracedSystem.to_system ts = s' ∧ Traced.TracedSystem.valid ts

s'.panics = 0 ∧ ∃ r, Spec.validate spec r s'.stateexact ts_hyp: ?m.336 ts
ts_hyp.right: ∀ {a b : Prop}, a ∧ b → b
right.currently_valid: ∀ {spec : Spec} {s : Traced.TracedSystem spec},
  Traced.TracedSystem.valid s → Spec.validate spec (Traced.TracedSystem.reservations s) s.state
currently_valid
Goals accomplished! 🐙
  
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid sclear initial_valid: Spec.validate spec IsReservation.empty s.state
initial_valid threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t
threads_validspec: Spec

s: System spec

no_panics_yet: s.panics = 0

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

inr∃ ts, Traced.TracedSystem.to_system ts = s' ∧ Traced.TracedSystem.valid ts
  
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid ssuffices
    ∀ ts: Traced.TracedSystem spec
ts : Traced.TracedSystem: Spec → Type 1
Traced.TracedSystem spec: Spec
spec, ts: Traced.TracedSystem spec
ts.valid: {spec : Spec} → Traced.TracedSystem spec → Prop
valid →
    s: System spec
s = ts: Traced.TracedSystem spec
ts.to_system: {spec : Spec} → Traced.TracedSystem spec → System spec
to_system → ∃ ts': Traced.TracedSystem spec
ts' : Traced.TracedSystem: Spec → Type 1
Traced.TracedSystem spec: Spec
spec, ts': Traced.TracedSystem spec
ts'.to_system: {spec : Spec} → Traced.TracedSystem spec → System spec
to_system = s': System spec
s' ∧ ts': Traced.TracedSystem spec
ts'.valid: {spec : Spec} → Traced.TracedSystem spec → Prop
valid by
    spec: Spec

s: System spec

no_panics_yet: s.panics = 0

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

inr∃ ts, Traced.TracedSystem.to_system ts = s' ∧ Traced.TracedSystem.valid tsapply this: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    s = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = s' ∧ Traced.TracedSystem.valid ts'
this traced: Traced.TracedSystem spec
traced traced_valid: Traced.TracedSystem.valid traced
traced_validspec: Spec

s: System spec

no_panics_yet: s.panics = 0

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

this: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    s = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = s' ∧ Traced.TracedSystem.valid ts'

s = Traced.TracedSystem.to_system traced
    spec: Spec

s: System spec

no_panics_yet: s.panics = 0

s': System spec

h: reduces_to s s'

traced:= Traced.TracedSystem.mk_initial s: Traced.TracedSystem spec

traced_valid: Traced.TracedSystem.valid traced

this: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    s = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = s' ∧ Traced.TracedSystem.valid ts'

∃ ts, Traced.TracedSystem.to_system ts = s' ∧ Traced.TracedSystem.valid tsexact Eq.symm: ∀ {α : Sort ?u.846} {a b : α}, a = b → b = a
Eq.symm <| Traced.TracedSystem.mk_initial.cancels_to_system: ∀ {spec : Spec} {s : System spec}, s.panics = 0 → Traced.TracedSystem.to_system (Traced.TracedSystem.mk_initial s) = s
Traced.TracedSystem.mk_initial.cancels_to_system no_panics_yet: s.panics = 0
no_panics_yet
Goals accomplished! 🐙

  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid sclear traced: ?m.267
traced traced_valid: Traced.TracedSystem.valid traced
traced_valid no_panics_yet: s.panics = 0
no_panics_yetspec: Spec

s, s': System spec

h: reduces_to s s'

inr∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    s = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = s' ∧ Traced.TracedSystem.valid ts'
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid sinduction h: ?m.193
hspec: Spec

s, s', a✝, b✝: System spec

idx✝: ThreadIndex a✝

inr.single∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = b✝ ∧ Traced.TracedSystem.valid ts'
spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid s.spec: Spec

s, s', a✝, b✝: System spec

idx✝: ThreadIndex a✝

inr.single∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = b✝ ∧ Traced.TracedSystem.valid ts' spec: Spec

s, s', a✝, b✝: System spec

idx✝: ThreadIndex a✝

inr.single∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = b✝ ∧ Traced.TracedSystem.valid ts'
spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'clear s: System spec
s s': System spec
s'spec: Spec

a✝, b✝: System spec

idx✝: ThreadIndex a✝

inr.single∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = b✝ ∧ Traced.TracedSystem.valid ts' spec: Spec

s, s', a✝, b✝: System spec

idx✝: ThreadIndex a✝

inr.single∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = b✝ ∧ Traced.TracedSystem.valid ts'
spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts';spec: Spec

a✝, b✝: System spec

idx✝: ThreadIndex a✝

inr.single∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = b✝ ∧ Traced.TracedSystem.valid ts' spec: Spec

s, s', a✝, b✝: System spec

idx✝: ThreadIndex a✝

inr.single∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = b✝ ∧ Traced.TracedSystem.valid ts'
spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'rename_i s: System ?m.888
s s': System ?m.888
s' idx: ThreadIndex s
idx iteration: iterate s idx = s'
iterationspec: Spec

s, s': System spec

idx: ThreadIndex s

iteration: iterate s idx = s'

inr.single∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    s = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = s' ∧ Traced.TracedSystem.valid ts'
    spec: Spec

s, s', a✝, b✝: System spec

idx✝: ThreadIndex a✝

inr.single∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = b✝ ∧ Traced.TracedSystem.valid ts'
spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'intro ts: Traced.TracedSystem spec
ts ts_valid: Traced.TracedSystem.valid ts
ts_valid s_def: s = Traced.TracedSystem.to_system ts
s_defspec: Spec

s, s': System spec

idx: ThreadIndex s

iteration: iterate s idx = s'

ts: Traced.TracedSystem spec

ts_valid: Traced.TracedSystem.valid ts

s_def: s = Traced.TracedSystem.to_system ts

inr.single∃ ts', Traced.TracedSystem.to_system ts' = s' ∧ Traced.TracedSystem.valid ts'
    spec: Spec

s, s', a✝, b✝: System spec

idx✝: ThreadIndex a✝

inr.single∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = b✝ ∧ Traced.TracedSystem.valid ts'
spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'exact Traced.TracedSystem.valid_by_iteration: ∀ {spec : Spec} (s s' : System spec) {idx : ThreadIndex s} {ts : Traced.TracedSystem spec},
  s = Traced.TracedSystem.to_system ts →
    Traced.TracedSystem.valid ts →
      iterate s idx = s' → ∃ ts', Traced.TracedSystem.to_system ts' = s' ∧ Traced.TracedSystem.valid ts'
Traced.TracedSystem.valid_by_iteration s: System ?m.888
s s': System ?m.888
s' s_def: s = Traced.TracedSystem.to_system ts
s_def ts_valid: Traced.TracedSystem.valid ts
ts_valid iteration: iterate s idx = s'
iteration
Goals accomplished! 🐙
  spec: Spec

s: System spec

no_panics_yet: s.panics = 0

initial_valid: Spec.validate spec IsReservation.empty s.state

threads_valid: ∀ (t : Thread spec), t ∈ s.threads → Thread.valid t

valid s.spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts' spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'rename_i a: System ?m.888
a b: System ?m.888
b c: System ?m.888
c _ _ IHab: ?m.889 a b a_to_b✝
IHab IHbc: ?m.889 b c b_to_c✝
IHbcspec: Spec

s, s', a, b, c: System spec

IHab: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = b ∧ Traced.TracedSystem.valid ts'

IHbc: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    b = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'
    spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'intro ts_a: Traced.TracedSystem spec
ts_a ts_a_valid: Traced.TracedSystem.valid ts_a
ts_a_valid ts_a_hyp: a = Traced.TracedSystem.to_system ts_a
ts_a_hypspec: Spec

s, s', a, b, c: System spec

IHab: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = b ∧ Traced.TracedSystem.valid ts'

IHbc: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    b = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'

ts_a: Traced.TracedSystem spec

ts_a_valid: Traced.TracedSystem.valid ts_a

ts_a_hyp: a = Traced.TracedSystem.to_system ts_a

inr.trans∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'
    spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'cases IHab: ?m.889 a b a_to_b✝
IHab ts_a: Traced.TracedSystem spec
ts_a ts_a_valid: Traced.TracedSystem.valid ts_a
ts_a_valid ts_a_hyp: a = Traced.TracedSystem.to_system ts_a
ts_a_hypspec: Spec

s, s', a, b, c: System spec

IHab: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = b ∧ Traced.TracedSystem.valid ts'

IHbc: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    b = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'

ts_a: Traced.TracedSystem spec

ts_a_valid: Traced.TracedSystem.valid ts_a

ts_a_hyp: a = Traced.TracedSystem.to_system ts_a

w✝: Traced.TracedSystem spec

inr.trans.intro∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'
    spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'rename_i ts_b: ?m.976
ts_b ts_b_hyp: ?m.977 ts_b
ts_b_hypspec: Spec

s, s', a, b, c: System spec

IHab: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = b ∧ Traced.TracedSystem.valid ts'

IHbc: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    b = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'

ts_a: Traced.TracedSystem spec

ts_a_valid: Traced.TracedSystem.valid ts_a

ts_a_hyp: a = Traced.TracedSystem.to_system ts_a

ts_b: Traced.TracedSystem spec

ts_b_hyp: Traced.TracedSystem.to_system ts_b = b ∧ Traced.TracedSystem.valid ts_b

inr.trans.intro∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'
    spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'apply IHbc: ?m.889 b c b_to_c✝
IHbc ts_b: ?m.976
ts_bspec: Spec

s, s', a, b, c: System spec

IHab: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = b ∧ Traced.TracedSystem.valid ts'

IHbc: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    b = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'

ts_a: Traced.TracedSystem spec

ts_a_valid: Traced.TracedSystem.valid ts_a

ts_a_hyp: a = Traced.TracedSystem.to_system ts_a

ts_b: Traced.TracedSystem spec

ts_b_hyp: Traced.TracedSystem.to_system ts_b = b ∧ Traced.TracedSystem.valid ts_b

inr.trans.intro.aTraced.TracedSystem.valid ts_b
spec: Spec

s, s', a, b, c: System spec

IHab: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = b ∧ Traced.TracedSystem.valid ts'

IHbc: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    b = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'

ts_a: Traced.TracedSystem spec

ts_a_valid: Traced.TracedSystem.valid ts_a

ts_a_hyp: a = Traced.TracedSystem.to_system ts_a

ts_b: Traced.TracedSystem spec

ts_b_hyp: Traced.TracedSystem.to_system ts_b = b ∧ Traced.TracedSystem.valid ts_b

inr.trans.intro.ab = Traced.TracedSystem.to_system ts_b
    spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'.spec: Spec

s, s', a, b, c: System spec

IHab: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = b ∧ Traced.TracedSystem.valid ts'

IHbc: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    b = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'

ts_a: Traced.TracedSystem spec

ts_a_valid: Traced.TracedSystem.valid ts_a

ts_a_hyp: a = Traced.TracedSystem.to_system ts_a

ts_b: Traced.TracedSystem spec

ts_b_hyp: Traced.TracedSystem.to_system ts_b = b ∧ Traced.TracedSystem.valid ts_b

inr.trans.intro.aTraced.TracedSystem.valid ts_b spec: Spec

s, s', a, b, c: System spec

IHab: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = b ∧ Traced.TracedSystem.valid ts'

IHbc: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    b = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'

ts_a: Traced.TracedSystem spec

ts_a_valid: Traced.TracedSystem.valid ts_a

ts_a_hyp: a = Traced.TracedSystem.to_system ts_a

ts_b: Traced.TracedSystem spec

ts_b_hyp: Traced.TracedSystem.to_system ts_b = b ∧ Traced.TracedSystem.valid ts_b

inr.trans.intro.aTraced.TracedSystem.valid ts_b
spec: Spec

s, s', a, b, c: System spec

IHab: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = b ∧ Traced.TracedSystem.valid ts'

IHbc: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    b = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'

ts_a: Traced.TracedSystem spec

ts_a_valid: Traced.TracedSystem.valid ts_a

ts_a_hyp: a = Traced.TracedSystem.to_system ts_a

ts_b: Traced.TracedSystem spec

ts_b_hyp: Traced.TracedSystem.to_system ts_b = b ∧ Traced.TracedSystem.valid ts_b

inr.trans.intro.ab = Traced.TracedSystem.to_system ts_bexact ts_b_hyp: ?m.977 ts_b
ts_b_hyp.right: ∀ {a b : Prop}, a ∧ b → b
right
Goals accomplished! 🐙
    spec: Spec

s, s', a✝, b✝, c✝: System spec

inr.trans∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a✝ = Traced.TracedSystem.to_system ts →
      ∃ ts', Traced.TracedSystem.to_system ts' = c✝ ∧ Traced.TracedSystem.valid ts'.spec: Spec

s, s', a, b, c: System spec

IHab: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = b ∧ Traced.TracedSystem.valid ts'

IHbc: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    b = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'

ts_a: Traced.TracedSystem spec

ts_a_valid: Traced.TracedSystem.valid ts_a

ts_a_hyp: a = Traced.TracedSystem.to_system ts_a

ts_b: Traced.TracedSystem spec

ts_b_hyp: Traced.TracedSystem.to_system ts_b = b ∧ Traced.TracedSystem.valid ts_b

inr.trans.intro.ab = Traced.TracedSystem.to_system ts_b spec: Spec

s, s', a, b, c: System spec

IHab: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    a = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = b ∧ Traced.TracedSystem.valid ts'

IHbc: ∀ (ts : Traced.TracedSystem spec),
  Traced.TracedSystem.valid ts →
    b = Traced.TracedSystem.to_system ts → ∃ ts', Traced.TracedSystem.to_system ts' = c ∧ Traced.TracedSystem.valid ts'

ts_a: Traced.TracedSystem spec

ts_a_valid: Traced.TracedSystem.valid ts_a

ts_a_hyp: a = Traced.TracedSystem.to_system ts_a

ts_b: Traced.TracedSystem spec

ts_b_hyp: Traced.TracedSystem.to_system ts_b = b ∧ Traced.TracedSystem.valid ts_b

inr.trans.intro.ab = Traced.TracedSystem.to_system ts_bexact ts_b_hyp: ?m.977 ts_b
ts_b_hyp.left: ∀ {a b : Prop}, a ∧ b → a
left.symm: ∀ {α : Sort ?u.1017} {a b : α}, a = b → b = a
symm
Goals accomplished! 🐙

end Mt.System