Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated (Runtime/Execution/Triggers.lean)

State before:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
⊢ t ≡ t' → (Activates exec t ↔ Execution.Executable.triggers.activated exec reaction t' = true)
Tactic:
intro equiv
State after:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ Activates exec t ↔ Execution.Executable.triggers.activated exec reaction t' = true

State before:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ Activates exec t ↔ Execution.Executable.triggers.activated exec reaction t' = true
Tactic:
unfold triggers.activated
State after:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ Activates exec t ↔
    (match t' with
      | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
      | Trigger.action action =>
        Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
      | Trigger.timer timer =>
        (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
      | Trigger.startup => isStartingUp exec
      | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
      true

State before:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ Activates exec t ↔
    (match t' with
      | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
      | Trigger.action action =>
        Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
      | Trigger.timer timer =>
        (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
      | Trigger.startup => isStartingUp exec
      | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
      true
Tactic:
constructor
State after:
case mp
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ Activates exec t →
    (match t' with
      | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
      | Trigger.action action =>
        Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
      | Trigger.timer timer =>
        (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
      | Trigger.startup => isStartingUp exec
      | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
      true

case mpr
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ (match t' with
      | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
      | Trigger.action action =>
        Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
      | Trigger.timer timer =>
        (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
      | Trigger.startup => isStartingUp exec
      | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
      true →
    Activates exec t

State before:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ Activates exec t →
    (match t' with
      | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
      | Trigger.action action =>
        Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
      | Trigger.timer timer =>
        (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
      | Trigger.startup => isStartingUp exec
      | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
      true
Tactic:
case mp =>
  intro activates
  cases t <;> cases t' <;> (try contradiction)
  case port.port => exact Activates.port_iff_equiv_port_activated equiv |>.mp activates
  all_goals
    cases activates
    cases equiv
    all_goals
      simp_all [actionIsPresent, portIsPresent, reactionInputs]
      try assumption
State after:
no goals

State before:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ (match t' with
      | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
      | Trigger.action action =>
        Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
      | Trigger.timer timer =>
        (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
      | Trigger.startup => isStartingUp exec
      | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
      true →
    Activates exec t
Tactic:
case mpr =>
  intro h
  cases t <;> cases t' <;> (try contradiction)
  case port.port => exact Activates.port_iff_equiv_port_activated equiv |>.mpr h
  all_goals
    simp at h
    constructor
    cases equiv
    all_goals
      simp_all [actionIsPresent, portIsPresent, reactionInputs]
      try assumption
State after:
no goals

State before:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ Activates exec t →
    (match t' with
      | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
      | Trigger.action action =>
        Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
      | Trigger.timer timer =>
        (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
      | Trigger.startup => isStartingUp exec
      | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
      true
Tactic:
intro activates
State after:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
activates : Activates exec t
⊢ (match t' with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true

State before:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
activates : Activates exec t
⊢ (match t' with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
Tactic:
cases t <;> cases t' <;> (try contradiction)
State after:
case port.port
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
kind✝ : Reactor.PortKind
id✝ : PortId net✝ kind✝
activates : Activates exec (Reaction.Trigger.port id✝)
p✝ : reaction.val.portSources.vars
equiv : Reaction.Trigger.port id✝ ≡ Trigger.port p✝
⊢ (match Trigger.port p✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true

case action.action
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
id✝ : ActionId net✝
activates : Activates exec (Reaction.Trigger.action id✝)
a✝ : reaction.val.actionSources.vars
equiv : Reaction.Trigger.action id✝ ≡ Trigger.action a✝
⊢ (match Trigger.action a✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝¹) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝¹ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true

case timer.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
id✝ : TimerId net✝
activates : Activates exec (Reaction.Trigger.timer id✝)
t✝ : reaction.val.timers
equiv : Reaction.Trigger.timer id✝ ≡ Trigger.timer t✝
⊢ (match Trigger.timer t✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true

case startup.startup
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
activates : Activates exec Reaction.Trigger.startup
equiv : Reaction.Trigger.startup ≡ Trigger.startup
⊢ (match Trigger.startup with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true

case shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
activates : Activates exec Reaction.Trigger.shutdown
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
⊢ (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
kind✝ : Reactor.PortKind
id✝ : PortId net✝ kind✝
activates : Activates exec (Reaction.Trigger.port id✝)
p✝ : reaction.val.portSources.vars
equiv : Reaction.Trigger.port id✝ ≡ Trigger.port p✝
⊢ (match Trigger.port p✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
Tactic:
case port.port => exact Activates.port_iff_equiv_port_activated equiv |>.mp activates
State after:
no goals

State before:
case action.action
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
id✝ : ActionId net✝
activates : Activates exec (Reaction.Trigger.action id✝)
a✝ : reaction.val.actionSources.vars
equiv : Reaction.Trigger.action id✝ ≡ Trigger.action a✝
⊢ (match Trigger.action a✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝¹) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝¹ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true

case timer.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
id✝ : TimerId net✝
activates : Activates exec (Reaction.Trigger.timer id✝)
t✝ : reaction.val.timers
equiv : Reaction.Trigger.timer id✝ ≡ Trigger.timer t✝
⊢ (match Trigger.timer t✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true

case startup.startup
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
activates : Activates exec Reaction.Trigger.startup
equiv : Reaction.Trigger.startup ≡ Trigger.startup
⊢ (match Trigger.startup with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true

case shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
activates : Activates exec Reaction.Trigger.shutdown
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
⊢ (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
Tactic:
all_goals
  cases activates
  cases equiv
  all_goals
    simp_all [actionIsPresent, portIsPresent, reactionInputs]
    try assumption
State after:
no goals

State before:
case shutdown.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
activates : Activates exec Reaction.Trigger.shutdown
t✝ : reaction.val.timers
equiv : Reaction.Trigger.shutdown ≡ Trigger.timer t✝
⊢ (match Trigger.timer t✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
Tactic:
try contradiction
State after:
no goals

State before:
case shutdown.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
activates : Activates exec Reaction.Trigger.shutdown
t✝ : reaction.val.timers
equiv : Reaction.Trigger.shutdown ≡ Trigger.timer t✝
⊢ (match Trigger.timer t✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
Tactic:
contradiction
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
kind✝ : Reactor.PortKind
id✝ : PortId net✝ kind✝
activates : Activates exec (Reaction.Trigger.port id✝)
p✝ : reaction.val.portSources.vars
equiv : Reaction.Trigger.port id✝ ≡ Trigger.port p✝
⊢ (match Trigger.port p✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
Tactic:
exact Activates.port_iff_equiv_port_activated equiv |>.mp activates
State after:
no goals

State before:
case shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
activates : Activates exec Reaction.Trigger.shutdown
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
⊢ (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
Tactic:
cases activates
State after:
case shutdown.shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
a✝ : exec.state = State.shuttingDown
⊢ (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝¹) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝¹ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true

State before:
case shutdown.shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
a✝ : exec.state = State.shuttingDown
⊢ (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝¹) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝¹ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
Tactic:
cases equiv
State after:
case shutdown.shutdown.shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
a✝ : exec.state = State.shuttingDown
⊢ (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝¹) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝¹ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true

State before:
case shutdown.shutdown.shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
a✝ : exec.state = State.shuttingDown
⊢ (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝¹) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝¹ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
Tactic:
all_goals
  simp_all [actionIsPresent, portIsPresent, reactionInputs]
  try assumption
State after:
no goals

State before:
case shutdown.shutdown.shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
a✝ : exec.state = State.shuttingDown
⊢ (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝¹) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝¹ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
Tactic:
simp_all [actionIsPresent, portIsPresent, reactionInputs]
State after:
no goals

State before:
case timer.timer.timer.timer
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
t✝ : reaction.val.timers
a✝ :
  (Executable.timer exec
        { reactor := a✝¹, timer := (_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ t✝ }).isFiring =
    true
⊢ (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ t✝)).isFiring = true
Tactic:
try assumption
State after:
no goals

State before:
case timer.timer.timer.timer
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
t✝ : reaction.val.timers
a✝ :
  (Executable.timer exec
        { reactor := a✝¹, timer := (_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ t✝ }).isFiring =
    true
⊢ (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ t✝)).isFiring = true
Tactic:
assumption
State after:
no goals

State before:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
⊢ (match t' with
      | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
      | Trigger.action action =>
        Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
      | Trigger.timer timer =>
        (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
      | Trigger.startup => isStartingUp exec
      | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
      true →
    Activates exec t
Tactic:
intro h
State after:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
h :
  (match t' with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
⊢ Activates exec t

State before:
net✝ : Network
t : Reaction.Trigger net✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t' : Reaction.triggerType reaction.val
equiv : t ≡ t'
h :
  (match t' with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
⊢ Activates exec t
Tactic:
cases t <;> cases t' <;> (try contradiction)
State after:
case port.port
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
kind✝ : Reactor.PortKind
id✝ : PortId net✝ kind✝
p✝ : reaction.val.portSources.vars
h :
  (match Trigger.port p✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.port id✝ ≡ Trigger.port p✝
⊢ Activates exec (Reaction.Trigger.port id✝)

case action.action
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
id✝ : ActionId net✝
a✝ : reaction.val.actionSources.vars
h :
  (match Trigger.action a✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝¹) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝¹ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.action id✝ ≡ Trigger.action a✝
⊢ Activates exec (Reaction.Trigger.action id✝)

case timer.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
id✝ : TimerId net✝
t✝ : reaction.val.timers
h :
  (match Trigger.timer t✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.timer id✝ ≡ Trigger.timer t✝
⊢ Activates exec (Reaction.Trigger.timer id✝)

case startup.startup
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  (match Trigger.startup with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.startup ≡ Trigger.startup
⊢ Activates exec Reaction.Trigger.startup

case shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
⊢ Activates exec Reaction.Trigger.shutdown

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
kind✝ : Reactor.PortKind
id✝ : PortId net✝ kind✝
p✝ : reaction.val.portSources.vars
h :
  (match Trigger.port p✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.port id✝ ≡ Trigger.port p✝
⊢ Activates exec (Reaction.Trigger.port id✝)
Tactic:
case port.port => exact Activates.port_iff_equiv_port_activated equiv |>.mpr h
State after:
no goals

State before:
case action.action
net✝ : Network
exec : Executable net✝
a✝¹ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝¹)
id✝ : ActionId net✝
a✝ : reaction.val.actionSources.vars
h :
  (match Trigger.action a✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝¹) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝¹ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝¹) ((_ : reaction.val.timers = timers (Path.class a✝¹)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.action id✝ ≡ Trigger.action a✝
⊢ Activates exec (Reaction.Trigger.action id✝)

case timer.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
id✝ : TimerId net✝
t✝ : reaction.val.timers
h :
  (match Trigger.timer t✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.timer id✝ ≡ Trigger.timer t✝
⊢ Activates exec (Reaction.Trigger.timer id✝)

case startup.startup
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  (match Trigger.startup with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.startup ≡ Trigger.startup
⊢ Activates exec Reaction.Trigger.startup

case shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
⊢ Activates exec Reaction.Trigger.shutdown
Tactic:
all_goals
  simp at h
  constructor
  cases equiv
  all_goals
    simp_all [actionIsPresent, portIsPresent, reactionInputs]
    try assumption
State after:
no goals

State before:
case shutdown.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : reaction.val.timers
h :
  (match Trigger.timer t✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.shutdown ≡ Trigger.timer t✝
⊢ Activates exec Reaction.Trigger.shutdown
Tactic:
try contradiction
State after:
no goals

State before:
case shutdown.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : reaction.val.timers
h :
  (match Trigger.timer t✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.shutdown ≡ Trigger.timer t✝
⊢ Activates exec Reaction.Trigger.shutdown
Tactic:
contradiction
State after:
no goals

State before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
kind✝ : Reactor.PortKind
id✝ : PortId net✝ kind✝
p✝ : reaction.val.portSources.vars
h :
  (match Trigger.port p✝ with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.port id✝ ≡ Trigger.port p✝
⊢ Activates exec (Reaction.Trigger.port id✝)
Tactic:
exact Activates.port_iff_equiv_port_activated equiv |>.mpr h
State after:
no goals

State before:
case shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h :
  (match Trigger.shutdown with
    | Trigger.port port => Interface?.isPresent (reactionInputs exec a✝) (Interface.Subscheme.coe port)
    | Trigger.action action =>
      Interface?.isPresent (interface exec a✝ Reactor.InterfaceKind.actions) (Interface.Subscheme.coe action)
    | Trigger.timer timer =>
      (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ timer)).isFiring
    | Trigger.startup => isStartingUp exec
    | Trigger.shutdown => decide (exec.state = State.shuttingDown)) =
    true
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
⊢ Activates exec Reaction.Trigger.shutdown
Tactic:
simp at h
State after:
case shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
h : exec.state = State.shuttingDown
⊢ Activates exec Reaction.Trigger.shutdown

State before:
case shutdown.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
h : exec.state = State.shuttingDown
⊢ Activates exec Reaction.Trigger.shutdown
Tactic:
constructor
State after:
case shutdown.shutdown.a
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
h : exec.state = State.shuttingDown
⊢ exec.state = State.shuttingDown

State before:
case shutdown.shutdown.a
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
equiv : Reaction.Trigger.shutdown ≡ Trigger.shutdown
h : exec.state = State.shuttingDown
⊢ exec.state = State.shuttingDown
Tactic:
cases equiv
State after:
case shutdown.shutdown.a.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h : exec.state = State.shuttingDown
⊢ exec.state = State.shuttingDown

State before:
case shutdown.shutdown.a.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h : exec.state = State.shuttingDown
⊢ exec.state = State.shuttingDown
Tactic:
all_goals
  simp_all [actionIsPresent, portIsPresent, reactionInputs]
  try assumption
State after:
no goals

State before:
case shutdown.shutdown.a.shutdown
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
h : exec.state = State.shuttingDown
⊢ exec.state = State.shuttingDown
Tactic:
simp_all [actionIsPresent, portIsPresent, reactionInputs]
State after:
no goals

State before:
case timer.timer.a.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : reaction.val.timers
h : (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ t✝)).isFiring = true
⊢ (Executable.timer exec { reactor := a✝, timer := (_ : reaction.val.timers = timers (Path.class a✝)) ▸ t✝ }).isFiring =
    true
Tactic:
try assumption
State after:
no goals

State before:
case timer.timer.a.timer
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
t✝ : reaction.val.timers
h : (Reactor.timer (reactors exec a✝) ((_ : reaction.val.timers = timers (Path.class a✝)) ▸ t✝)).isFiring = true
⊢ (Executable.timer exec { reactor := a✝, timer := (_ : reaction.val.timers = timers (Path.class a✝)) ▸ t✝ }).isFiring =
    true
Tactic:
assumption
State after:
no goals