Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
import Mt.Thread

namespace Mt

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

/-- Describes a system of zero or more threads running in parallel

  Systems can be iterated one atomic step at a time by choosing
  one of its threads. They keep track of the number of threads
  which panicked during execution
-/
structure 
System: {spec : Spec} β†’ spec.State β†’ List (Thread spec) β†’ Nat β†’ System spec
System (
spec: Spec
spec : 
Spec: Type 1
Spec) where
  
state: {spec : Spec} β†’ System spec β†’ spec.State
state   : 
spec: Spec
spec.
State: Spec β†’ Type
State
  
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads : 
List: Type ?u.34 β†’ Type ?u.34
List (
Thread: Spec β†’ Type 1
Thread 
spec: Spec
spec)
  
panics: {spec : Spec} β†’ System spec β†’ Nat
panics  : 
Nat: Type
Nat

namespace System

def 
ThreadIndex: System spec β†’ Type
ThreadIndex (
s: System spec
s : 
System: Spec β†’ Type 1
System 
spec: Spec
spec) : 
Type: Type 1
Type :=
Fin: Nat β†’ Type
Fin 
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
length: {Ξ± : Type ?u.540} β†’ List Ξ± β†’ Nat
length
def 
done: System spec β†’ Bool
done (
s: System spec
s : 
System: Spec β†’ Type 1
System 
spec: Spec
spec) : 
Bool: Type
Bool :=
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
length: {Ξ± : Type ?u.559} β†’ List Ξ± β†’ Nat
length = 
0: ?m.565
0

def 
iterate: (s : System spec) β†’ ThreadIndex s β†’ System spec
iterate (
s: System spec
s : 
System: Spec β†’ Type 1
System 
spec: Spec
spec) : 
s: System spec
s.
ThreadIndex: {spec : Spec} β†’ System spec β†’ Type
ThreadIndex -> 
System: Spec β†’ Type 1
System 
spec: Spec
spec
  | 
thread_idx: ?m.670
thread_idx =>
    if (
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
get: {Ξ± : Type ?u.673} β†’ (as : List Ξ±) β†’ Fin (List.length as) β†’ Ξ±
get 
thread_idx: ?m.670
thread_idx).
block_until: {spec : Spec} β†’ Thread spec β†’ spec.State β†’ Bool
block_until 
s: System spec
s.
state: {spec : Spec} β†’ System spec β†’ spec.State
state then 
      match (
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
get: {Ξ± : Type ?u.763} β†’ (as : List Ξ±) β†’ Fin (List.length as) β†’ Ξ±
get 
thread_idx: ?m.670
thread_idx).
iterate: {spec : Spec} β†’ Thread spec β†’ spec.State β†’ Thread.IterationResult spec
iterate 
s: System spec
s.
state: {spec : Spec} β†’ System spec β†’ spec.State
state with
        | 
Thread.IterationResult.Done: {spec : Spec} β†’ spec.State β†’ Thread.IterationResult spec
Thread.IterationResult.Done 
state: spec.State
state =>
          {
            
state: spec.State
state
            threads := 
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
eraseIdx: {Ξ± : Type ?u.789} β†’ List Ξ± β†’ Nat β†’ List Ξ±
eraseIdx 
thread_idx: ?m.670
thread_idx.
val: {n : Nat} β†’ Fin n β†’ Nat
val
            panics := 
s: System spec
s.
panics: {spec : Spec} β†’ System spec β†’ Nat
panics
          }
        | 
Thread.IterationResult.Panic: {spec : Spec} β†’ spec.State β†’ Thread.IterationResult spec
Thread.IterationResult.Panic 
state: spec.State
state =>
          {
            
state: spec.State
state
            threads := 
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
eraseIdx: {Ξ± : Type ?u.811} β†’ List Ξ± β†’ Nat β†’ List Ξ±
eraseIdx 
thread_idx: ?m.670
thread_idx.
val: {n : Nat} β†’ Fin n β†’ Nat
val
            panics := 
s: System spec
s.
panics: {spec : Spec} β†’ System spec β†’ Nat
panics + 
1: ?m.822
1
          }
        | 
Thread.IterationResult.Running: {spec : Spec} β†’ spec.State β†’ Thread spec β†’ Thread.IterationResult spec
Thread.IterationResult.Running 
state: spec.State
state 
thread: Thread spec
thread =>
          {
            
state: spec.State
state
            threads := 
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
set: {Ξ± : Type ?u.890} β†’ List Ξ± β†’ Nat β†’ Ξ± β†’ List Ξ±
set 
thread_idx: ?m.670
thread_idx.
val: {n : Nat} β†’ Fin n β†’ Nat
val 
thread: Thread spec
thread
            panics := 
s: System spec
s.
panics: {spec : Spec} β†’ System spec β†’ Nat
panics
          }
    else
      
s: System spec
s

theorem 
iterate_threads: βˆ€ (s : System spec) (thread_idx : ThreadIndex s),
  Thread.block_until (List.get s.threads thread_idx) s.state = true β†’
    (iterate s thread_idx).threads =       let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
      match Thread.iterate (List.get s.threads thread_idx) s.state with
      | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
      | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
      | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
iterate_threads (
s: System spec
s : 
System: Spec β†’ Type 1
System 
spec: Spec
spec) (
thread_idx: ThreadIndex s
thread_idx : 
s: System spec
s.
ThreadIndex: {spec : Spec} β†’ System spec β†’ Type
ThreadIndex)
  (
blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true
blocked_until : (
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
get: {Ξ± : Type ?u.1259} β†’ (as : List Ξ±) β†’ Fin (List.length as) β†’ Ξ±
get 
thread_idx: ThreadIndex s
thread_idx).
block_until: {spec : Spec} β†’ Thread spec β†’ spec.State β†’ Bool
block_until 
s: System spec
s.
state: {spec : Spec} β†’ System spec β†’ spec.State
state) :
  (
s: System spec
s.
iterate: {spec : Spec} β†’ (s : System spec) β†’ ThreadIndex s β†’ System spec
iterate 
thread_idx: ThreadIndex s
thread_idx).
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads =
    match (
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
get: {Ξ± : Type ?u.1293} β†’ (as : List Ξ±) β†’ Fin (List.length as) β†’ Ξ±
get 
thread_idx: ThreadIndex s
thread_idx).
iterate: {spec : Spec} β†’ Thread spec β†’ spec.State β†’ Thread.IterationResult spec
iterate 
s: System spec
s.
state: {spec : Spec} β†’ System spec β†’ spec.State
state with
      | 
Thread.IterationResult.Done: {spec : Spec} β†’ spec.State β†’ Thread.IterationResult spec
Thread.IterationResult.Done .. => 
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
eraseIdx: {Ξ± : Type ?u.1327} β†’ List Ξ± β†’ Nat β†’ List Ξ±
eraseIdx 
thread_idx: ThreadIndex s
thread_idx.
val: {n : Nat} β†’ Fin n β†’ Nat
val
      | 
Thread.IterationResult.Panic: {spec : Spec} β†’ spec.State β†’ Thread.IterationResult spec
Thread.IterationResult.Panic .. => 
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
eraseIdx: {Ξ± : Type ?u.1347} β†’ List Ξ± β†’ Nat β†’ List Ξ±
eraseIdx 
thread_idx: ThreadIndex s
thread_idx.
val: {n : Nat} β†’ Fin n β†’ Nat
val
      | 
Thread.IterationResult.Running: {spec : Spec} β†’ spec.State β†’ Thread spec β†’ Thread.IterationResult spec
Thread.IterationResult.Running _ 
thread: Thread spec
thread => 
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
set: {Ξ± : Type ?u.1372} β†’ List Ξ± β†’ Nat β†’ Ξ± β†’ List Ξ±
set 
thread_idx: ThreadIndex s
thread_idx.
val: {n : Nat} β†’ Fin n β†’ Nat
val 
thread: Thread spec
thread :=
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(iterate s thread_idx).threads =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(iterate s thread_idx).threads =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(let thread_idx := thread_idx;
    if Thread.block_until (List.get s.threads thread_idx) s.state = true then
      match Thread.iterate (List.get s.threads thread_idx) s.state with
      | Thread.IterationResult.Done state =>
        { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
      | Thread.IterationResult.Panic state =>
        { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
      | Thread.IterationResult.Running state thread =>
        { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }
    else s).threads =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(let thread_idx := thread_idx;
    if Thread.block_until (List.get s.threads thread_idx) s.state = true then
      match Thread.iterate (List.get s.threads thread_idx) s.state with
      | Thread.IterationResult.Done state =>
        { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
      | Thread.IterationResult.Panic state =>
        { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
      | Thread.IterationResult.Running state thread =>
        { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }
    else s).threads =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(iterate s thread_idx).threads =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(match Thread.iterate (List.get s.threads thread_idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).threads =   match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(iterate s thread_idx).threads =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝: spec.State

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Done a✝

Done
(match Thread.IterationResult.Done a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).threads =   match Thread.IterationResult.Done a✝ with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝: spec.State

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Panic a✝

Panic
(match Thread.IterationResult.Panic a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).threads =   match Thread.IterationResult.Panic a✝ with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Running a✝¹ a✝

Running
(match Thread.IterationResult.Running a✝¹ a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).threads =   match Thread.IterationResult.Running a✝¹ a✝ with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(match Thread.iterate (List.get s.threads thread_idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).threads =   match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝: spec.State

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Done a✝

Done
(match Thread.IterationResult.Done a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).threads =   match Thread.IterationResult.Done a✝ with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝: spec.State

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Panic a✝

Panic
(match Thread.IterationResult.Panic a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).threads =   match Thread.IterationResult.Panic a✝ with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Running a✝¹ a✝

Running
(match Thread.IterationResult.Running a✝¹ a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).threads =   match Thread.IterationResult.Running a✝¹ a✝ with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(match Thread.iterate (List.get s.threads thread_idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).threads =   match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Panic a => List.eraseIdx s.threads thread_idx.val
  | Thread.IterationResult.Running a thread => List.set s.threads thread_idx.val thread
Goals accomplished! πŸ™


theorem 
iterate_panics: βˆ€ {spec : Spec} (s : System spec) (thread_idx : ThreadIndex s),
  Thread.block_until (List.get s.threads thread_idx) s.state = true β†’
    (iterate s thread_idx).panics =       let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
      match Thread.iterate (List.get s.threads thread_idx) s.state with
      | Thread.IterationResult.Done a => s.panics
      | Thread.IterationResult.Panic a => s.panics + 1
      | Thread.IterationResult.Running a a_1 => s.panics
iterate_panics (
s: System spec
s : 
System: Spec β†’ Type 1
System 
spec: Spec
spec) (
thread_idx: ThreadIndex s
thread_idx : 
s: System spec
s.
ThreadIndex: {spec : Spec} β†’ System spec β†’ Type
ThreadIndex)
  (
blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true
blocked_until : (
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
get: {Ξ± : Type ?u.2792} β†’ (as : List Ξ±) β†’ Fin (List.length as) β†’ Ξ±
get 
thread_idx: ThreadIndex s
thread_idx).
block_until: {spec : Spec} β†’ Thread spec β†’ spec.State β†’ Bool
block_until 
s: System spec
s.
state: {spec : Spec} β†’ System spec β†’ spec.State
state) :
  (
s: System spec
s.
iterate: {spec : Spec} β†’ (s : System spec) β†’ ThreadIndex s β†’ System spec
iterate 
thread_idx: ThreadIndex s
thread_idx).
panics: {spec : Spec} β†’ System spec β†’ Nat
panics =
    match (
s: System spec
s.
threads: {spec : Spec} β†’ System spec β†’ List (Thread spec)
threads.
get: {Ξ± : Type ?u.2826} β†’ (as : List Ξ±) β†’ Fin (List.length as) β†’ Ξ±
get 
thread_idx: ThreadIndex s
thread_idx).
iterate: {spec : Spec} β†’ Thread spec β†’ spec.State β†’ Thread.IterationResult spec
iterate 
s: System spec
s.
state: {spec : Spec} β†’ System spec β†’ spec.State
state with
      | 
Thread.IterationResult.Done: {spec : Spec} β†’ spec.State β†’ Thread.IterationResult spec
Thread.IterationResult.Done .. => 
s: System spec
s.
panics: {spec : Spec} β†’ System spec β†’ Nat
panics
      | 
Thread.IterationResult.Panic: {spec : Spec} β†’ spec.State β†’ Thread.IterationResult spec
Thread.IterationResult.Panic .. => 
s: System spec
s.
panics: {spec : Spec} β†’ System spec β†’ Nat
panics + 
1: ?m.2877
1
      | 
Thread.IterationResult.Running: {spec : Spec} β†’ spec.State β†’ Thread spec β†’ Thread.IterationResult spec
Thread.IterationResult.Running .. => 
s: System spec
s.
panics: {spec : Spec} β†’ System spec β†’ Nat
panics :=
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(iterate s thread_idx).panics =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(iterate s thread_idx).panics =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(let thread_idx := thread_idx;
    if Thread.block_until (List.get s.threads thread_idx) s.state = true then
      match Thread.iterate (List.get s.threads thread_idx) s.state with
      | Thread.IterationResult.Done state =>
        { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
      | Thread.IterationResult.Panic state =>
        { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
      | Thread.IterationResult.Running state thread =>
        { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }
    else s).panics =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(let thread_idx := thread_idx;
    if Thread.block_until (List.get s.threads thread_idx) s.state = true then
      match Thread.iterate (List.get s.threads thread_idx) s.state with
      | Thread.IterationResult.Done state =>
        { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
      | Thread.IterationResult.Panic state =>
        { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
      | Thread.IterationResult.Running state thread =>
        { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }
    else s).panics =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(iterate s thread_idx).panics =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(match Thread.iterate (List.get s.threads thread_idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).panics =   match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(iterate s thread_idx).panics =   let _discr := Thread.iterate (List.get s.threads thread_idx) s.state;
  match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝: spec.State

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Done a✝

Done
(match Thread.IterationResult.Done a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).panics =   match Thread.IterationResult.Done a✝ with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝: spec.State

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Panic a✝

Panic
(match Thread.IterationResult.Panic a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).panics =   match Thread.IterationResult.Panic a✝ with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Running a✝¹ a✝

Running
(match Thread.IterationResult.Running a✝¹ a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).panics =   match Thread.IterationResult.Running a✝¹ a✝ with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(match Thread.iterate (List.get s.threads thread_idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).panics =   match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝: spec.State

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Done a✝

Done
(match Thread.IterationResult.Done a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).panics =   match Thread.IterationResult.Done a✝ with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝: spec.State

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Panic a✝

Panic
(match Thread.IterationResult.Panic a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).panics =   match Thread.IterationResult.Panic a✝ with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

a✝¹: spec.State

a✝: Thread spec

h: Thread.iterate (List.get s.threads thread_idx) s.state = Thread.IterationResult.Running a✝¹ a✝

Running
(match Thread.IterationResult.Running a✝¹ a✝ with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).panics =   match Thread.IterationResult.Running a✝¹ a✝ with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
spec: Spec

s: System spec

thread_idx: ThreadIndex s

blocked_until: Thread.block_until (List.get s.threads thread_idx) s.state = true

(match Thread.iterate (List.get s.threads thread_idx) s.state with
    | Thread.IterationResult.Done state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics }
    | Thread.IterationResult.Panic state =>
      { state := state, threads := List.eraseIdx s.threads thread_idx.val, panics := s.panics + 1 }
    | Thread.IterationResult.Running state thread =>
      { state := state, threads := List.set s.threads thread_idx.val thread, panics := s.panics }).panics =   match Thread.iterate (List.get s.threads thread_idx) s.state with
  | Thread.IterationResult.Done a => s.panics
  | Thread.IterationResult.Panic a => s.panics + 1
  | Thread.IterationResult.Running a a_1 => s.panics
Goals accomplished! πŸ™


inductive 
reduces_to: System spec β†’ System spec β†’ Prop
reduces_to : 
System: Spec β†’ Type 1
System 
spec: Spec
spec -> 
System: Spec β†’ Type 1
System 
spec: Spec
spec -> 
Prop: Type
Prop where
| 
single: βˆ€ {spec : Spec} {a b : System spec} (idx : ThreadIndex a), iterate a idx = b β†’ reduces_to a b
single {
a: ?m.4086
a 
b: ?m.4089
b} (
idx: ?m.4092
idx : 
a: ?m.4086
a.
ThreadIndex: {spec : Spec} β†’ System spec β†’ Type
ThreadIndex) (
iteration: ?m.4098 = b
iteration : 
a: ?m.4086
a.
iterate: {spec : Spec} β†’ (s : System spec) β†’ ThreadIndex s β†’ System spec
iterate 
idx: ?m.4092
idx = 
b: ?m.4089
b) : 
reduces_to: System spec β†’ System spec β†’ Prop
reduces_to 
a: ?m.4086
a 
b: ?m.4089
b
| 
trans: βˆ€ {spec : Spec} {a b c : System spec}, reduces_to a b β†’ reduces_to b c β†’ reduces_to a c
trans {
a: ?m.4119
a 
b: ?m.4122
b 
c: ?m.4125
c} (
a_to_b: ?m.4128
a_to_b : 
a: ?m.4119
a.
reduces_to: System spec β†’ System spec β†’ Prop
reduces_to 
b: ?m.4122
b) (
b_to_c: ?m.4131
b_to_c : 
b: ?m.4122
b.
reduces_to: System spec β†’ System spec β†’ Prop
reduces_to 
c: ?m.4125
c) : 
reduces_to: System spec β†’ System spec β†’ Prop
reduces_to 
a: ?m.4119
a 
c: ?m.4125
c

def 
reduces_to_or_eq: System spec β†’ System spec β†’ Prop
reduces_to_or_eq (
a: System spec
a 
b: System spec
b : 
System: Spec β†’ Type 1
System 
spec: Spec
spec) : 
Prop: Type
Prop :=
a: System spec
a = 
b: System spec
b ∨ 
a: System spec
a.
reduces_to: {spec : Spec} β†’ System spec β†’ System spec β†’ Prop
reduces_to 
b: System spec
b

theorem 
reduces_to_or_eq.refl: βˆ€ (a : System spec), reduces_to_or_eq a a
reduces_to_or_eq.refl (
a: System spec
a : 
System: Spec β†’ Type 1
System 
spec: Spec
spec) : 
a: System spec
a.
reduces_to_or_eq: {spec : Spec} β†’ System spec β†’ System spec β†’ Prop
reduces_to_or_eq 
a: System spec
a :=
Or.inl: βˆ€ {a b : Prop}, a β†’ a ∨ b
Or.inl 
rfl: βˆ€ {Ξ± : Sort ?u.4389} {a : Ξ±}, a = a
rfl
theorem 
reduces_to_or_eq.trans: βˆ€ {spec : Spec} {a b c : System spec}, reduces_to_or_eq a b β†’ reduces_to_or_eq b c β†’ reduces_to_or_eq a c
reduces_to_or_eq.trans {
a: System spec
a 
b: System spec
b 
c: System spec
c : 
System: Spec β†’ Type 1
System 
spec: Spec
spec} :
  
a: System spec
a.
reduces_to_or_eq: {spec : Spec} β†’ System spec β†’ System spec β†’ Prop
reduces_to_or_eq 
b: System spec
b β†’ 
b: System spec
b.
reduces_to_or_eq: {spec : Spec} β†’ System spec β†’ System spec β†’ Prop
reduces_to_or_eq 
c: System spec
c β†’ 
a: System spec
a.
reduces_to_or_eq: {spec : Spec} β†’ System spec β†’ System spec β†’ Prop
reduces_to_or_eq 
c: System spec
c :=
spec: Spec

a, b, c: System spec

reduces_to_or_eq a b β†’ reduces_to_or_eq b c β†’ reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

ab: reduces_to_or_eq a b

bc: reduces_to_or_eq b c

reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

reduces_to_or_eq a b β†’ reduces_to_or_eq b c β†’ reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

bc: reduces_to_or_eq b c

inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

bc: reduces_to_or_eq b c

inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

ab: reduces_to_or_eq a b

bc: reduces_to_or_eq b c

reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

bc: reduces_to_or_eq b c

inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

bc: reduces_to_or_eq b c

inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

ab: reduces_to_or_eq a b

bc: reduces_to_or_eq b c

reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

inl.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

inl.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

bc: reduces_to_or_eq b c

inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

inr.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

bc: reduces_to_or_eq b c

inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

reduces_to_or_eq a b β†’ reduces_to_or_eq b c β†’ reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: b = c

inl.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: b = c

inl.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: reduces_to b c

inl.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: reduces_to b c

inr.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: b = c

inl.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: b = c

inl.inl
reduces_to_or_eq b c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: b = c

inl.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: b = c

inl.inl
reduces_to_or_eq c c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: b = c

inl.inl
reduces_to_or_eq c c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: b = c

inl.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: reduces_to b c

inl.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: reduces_to b c

inr.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: b = c

inl.inl
reduces_to_or_eq c c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: b = c

inl.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: reduces_to b c

inl.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: reduces_to b c

inr.inr
reduces_to_or_eq a c
Goals accomplished! πŸ™
spec: Spec

a, b, c: System spec

reduces_to_or_eq a b β†’ reduces_to_or_eq b c β†’ reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: reduces_to b c

inl.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: reduces_to b c

inl.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: reduces_to b c

inr.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: reduces_to b c

inl.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: reduces_to b c

inl.inr
reduces_to_or_eq b c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: reduces_to b c

inl.inr
reduces_to_or_eq b c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: reduces_to b c

inl.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: reduces_to b c

inr.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: reduces_to b c

inl.inr
reduces_to_or_eq b c
spec: Spec

a, b, c: System spec

h₁: a = b

hβ‚‚: reduces_to b c

inl.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: reduces_to b c

inr.inr
reduces_to_or_eq a c
Goals accomplished! πŸ™
spec: Spec

a, b, c: System spec

reduces_to_or_eq a b β†’ reduces_to_or_eq b c β†’ reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: reduces_to b c

inr.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a b
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a b
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: reduces_to b c

inr.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a b
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: b = c

inr.inl
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: reduces_to b c

inr.inr
reduces_to_or_eq a c
Goals accomplished! πŸ™
spec: Spec

a, b, c: System spec

reduces_to_or_eq a b β†’ reduces_to_or_eq b c β†’ reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: reduces_to b c

inr.inr
reduces_to_or_eq a c
spec: Spec

a, b, c: System spec

h₁: reduces_to a b

hβ‚‚: reduces_to b c

inr.inr
reduces_to_or_eq a c
Goals accomplished! πŸ™



end System

end Mt