Theorem: Execution.Executable.Next.for_tag_strictly_monotonic
Proof state before:
net : Network
next : Next net
exec : Executable net
h : Next.for exec = some next
⊢ exec.tag < next.tag
Tactic:
simp [Next.for] at h
Proof state after:
net : Network
next : Next net
exec : Executable net
h :
  (match h :
      nextTime
        { state := exec.state, tag := exec.tag,
          queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec), reactors := exec.reactors,
          physicalOffset := exec.physicalOffset, toPropagate := exec.toPropagate } with
    | none => none
    | some time =>
      some
        { tag := Tag.advance exec.tag time,
          events :=
            (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time.val
                (_ :
                  ∀
                    (x :
                      Time.From
                        { state := exec.state, tag := exec.tag,
                              queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                              reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                              toPropagate := exec.toPropagate }.tag.time),
                    Queue.nextTime
                          { state := exec.state, tag := exec.tag,
                              queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                              reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                              toPropagate := exec.toPropagate }.queue =
                        some x →
                      time ≤ x)).fst,
          queue :=
            (_ :
                time.val =
                  (Tag.advance
                      { state := exec.state, tag := exec.tag,
                          queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                          reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                          toPropagate := exec.toPropagate }.tag
                      time).time) ▸
              Queue.merge
                (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time.val
                    (_ :
                      ∀
                        (x :
                          Time.From
                            { state := exec.state, tag := exec.tag,
                                  queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                  reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                  toPropagate := exec.toPropagate }.tag.time),
                        Queue.nextTime
                              { state := exec.state, tag := exec.tag,
                                  queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                  reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                  toPropagate := exec.toPropagate }.queue =
                            some x →
                          time ≤ x)).snd
                (Execution.Executable.nextTimerEvents
                  { state := exec.state, tag := exec.tag,
                    queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                    reactors := exec.reactors, physicalOffset := exec.physicalOffset, toPropagate := exec.toPropagate }
                  (Array.filterMap (fun x => Event.timer? x)
                    (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time.val
                        (_ :
                          ∀
                            (x :
                              Time.From
                                { state := exec.state, tag := exec.tag,
                                      queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                      reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                      toPropagate := exec.toPropagate }.tag.time),
                            Queue.nextTime
                                  { state := exec.state, tag := exec.tag,
                                      queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                      reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                      toPropagate := exec.toPropagate }.queue =
                                some x →
                              time ≤ x)).fst
                    0
                    (Array.size
                      (Queue.split (Queue.merge exec.queue (Execution.Executable.propagationEvents exec)) time.val
                          (_ :
                            ∀
                              (x :
                                Time.From
                                  { state := exec.state, tag := exec.tag,
                                        queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                        reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                        toPropagate := exec.toPropagate }.tag.time),
                              Queue.nextTime
                                    { state := exec.state, tag := exec.tag,
                                        queue := Queue.merge exec.queue (Execution.Executable.propagationEvents exec),
                                        reactors := exec.reactors, physicalOffset := exec.physicalOffset,
                                        toPropagate := exec.toPropagate }.queue =
                                  some x →
                                time ≤ x)).fst))
                  time.val) }) =
    some next
⊢ exec.tag < next.tag