internlm/Lean-Github huggingface dataset:
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
rw [hi] at hp
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Sum.inl input✝ = Sum.inr { fst := c, snd := output }
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
input✝ : (Class.interface (Path.class reactor) Reactor.InterfaceKind.inputs).vars
hp : Sum.inl input✝ = Sum.inr { fst := c, snd := output }
h : Activates exec (Reaction.Trigger.port { reactor := reactor, port := input✝ })
hi : Interface.Subscheme.coe p' = Sum.inl input✝
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
contradiction
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
hp : Interface.Subscheme.coe p' = Sum.inr { fst := c, snd := output }
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
simp [ho] at hp
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
hp : { fst := c', snd := output' } = { fst := c, snd := output }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
hp : { fst := c', snd := output' } = { fst := c, snd := output }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
injection hp with hc ho
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
hc : c' = c
ho : HEq output' output
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c : Child (Path.class reactor)
output : (Class.interface (Child.class c) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
hc : c' = c
ho : HEq output' output
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c) Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
subst hc
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
output : (Class.interface (Child.class c') Reactor.InterfaceKind.outputs).vars
ho : HEq output' output
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output)) = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho✝ : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
output : (Class.interface (Child.class c') Reactor.InterfaceKind.outputs).vars
ho : HEq output' output
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output)) = some v
Tactic:
subst ho
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
h : Activates exec (Reaction.Trigger.port { reactor := Path.extend reactor c', port := cast _ output' })
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Tactic:
cases h
Proof state after:
case port
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
a✝ : portIsPresent exec { reactor := Path.extend reactor c', port := cast _ output' } = true
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : portIsPresent exec { reactor := Path.extend reactor c', port := cast _ output' } = true
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Tactic:
case port h =>
  simp [portIsPresent] at h
  have ⟨v, hv⟩ := h
  exists cast sorry v
  simp [hv]
  sorry
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : portIsPresent exec { reactor := Path.extend reactor c', port := cast _ output' } = true
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Tactic:
simp [portIsPresent] at h
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Tactic:
have ⟨v, hv⟩ := h
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ ∃ v, cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some v
Tactic:
exists cast sorry v
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some (cast _ v)
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ cast _ (interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output')) = some (cast _ v)
Tactic:
simp [hv]
Proof state after:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ cast _ (some v) = some (cast _ v)
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
exec : Executable net✝
reactor : ReactorId net✝
reaction : Class.Reaction (Path.class reactor)
p' : reaction.val.portSources.vars
sub : (subinterface (Path.class reactor) Reactor.InterfaceKind.outputs).vars
c' : Child (Path.class reactor)
output' : ((fun child => Class.interface (Child.class child) Reactor.InterfaceKind.outputs) c').vars
ho : Interface.Subscheme.coe p' = Sum.inr { fst := c', snd := output' }
h : ∃ v, interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
v :
  Interface.Scheme.type (Class.interface (Path.class (Path.extend reactor c')) Reactor.InterfaceKind.outputs)
    (cast _ output')
hv : interface exec (Path.extend reactor c') Reactor.InterfaceKind.outputs (cast _ output') = some v
⊢ cast _ (some v) = some (cast _ v)
Tactic:
sorry
Proof state after:
no goals
Theorem: Execution.Executable.Activates.port_iff_equiv_port_activated
Proof state before:
net✝ : Network
kind✝ : Reactor.PortKind
p : PortId net✝ kind✝
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
p' : reaction.val.portSources.vars
he : Reaction.Trigger.port p ≡ Trigger.port p'
h : Execution.Executable.triggers.activated exec reaction (Trigger.port p') = true
⊢ Activates exec (Reaction.Trigger.port p)
Tactic:
sorry
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
⊢ t ≡ t' → (Activates exec t ↔ Execution.Executable.triggers.activated exec reaction t' = true)
Tactic:
intro equiv
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 exec t ↔ Execution.Executable.triggers.activated exec reaction t' = true
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 ↔ Execution.Executable.triggers.activated exec reaction t' = true
Tactic:
unfold triggers.activated
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 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
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
Proof 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