internlm/Lean-Github huggingface dataset:
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'
⊢ 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
Proof state after:
no goals
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'
⊢ (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
Proof state after:
no goals
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'
⊢ 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
Proof 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
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof 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
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof 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
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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]
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
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'
⊢ (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
Proof 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
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof 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
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof 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
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof 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
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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]
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Activates.iff_equiv_trigger_activated
Proof 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
Proof state after:
no goals
Theorem: Execution.Executable.Triggers.iff_triggers_eq_true
Proof state before:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction ↔ Execution.Executable.triggers exec reaction = true
Tactic:
unfold triggers
Proof state after:
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Triggers exec reaction ↔
    Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true