Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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)
Proof 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