Theorem: Execution.State.Over.exists_allowed_of_acyclic_has_unprocessed
Proof state before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr : α
s : State.Over rtr
_x✝ :
  (i : Component.idType Component.rcn) ×'
    (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝⁴ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y _x✝ →
      ∃ i, Allows s.toState i
i : Component.idType Component.rcn
a✝³ : (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝² :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := a✝³ } →
      ∃ i, Allows s.toState i
a : Dependency.Acyclic rtr
h₁✝¹ : (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝¹ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := { fst := a, snd := h₁✝¹ } } →
      ∃ i, Allows s.toState i
h₁✝ : i ∈ s.rtr[Component.rcn]
h₂✝ : i ∉ s.progress
a✝ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := { fst := a, snd := { fst := h₁✝, snd := h₂✝ } } } →
      ∃ i, Allows s.toState i
h : ¬dependencies s.rtr i \ s.progress = ∅
w✝ : ID
hd : w✝ ∈ dependencies s.rtr i \ s.progress
h₁ : w✝ ∈ dependencies s.rtr i
h₂ : w✝ ∉ s.progress
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun i snd =>
            PSigma.casesOn snd fun a snd =>
              PSigma.casesOn snd fun h₁ snd =>
                let_fun fin := ⋯;
                (Set.Finite.toFinset fin).card)
        instWellFoundedRelation).1
    { fst := w✝, snd := { fst := a, snd := { fst := ⋯, snd := h₂ } } }
    { fst := i, snd := { fst := a, snd := { fst := h₁✝, snd := h₂✝ } } }
Tactic:
simp_wf
Proof state after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr : α
s : State.Over rtr
_x✝ :
  (i : Component.idType Component.rcn) ×'
    (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝⁴ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y _x✝ →
      ∃ i, Allows s.toState i
i : Component.idType Component.rcn
a✝³ : (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝² :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := a✝³ } →
      ∃ i, Allows s.toState i
a : Dependency.Acyclic rtr
h₁✝¹ : (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress
a✝¹ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := { fst := a, snd := h₁✝¹ } } →
      ∃ i, Allows s.toState i
h₁✝ : i ∈ s.rtr[Component.rcn]
h₂✝ : i ∉ s.progress
a✝ :
  ∀
    (y :
      (i : Component.idType Component.rcn) ×'
        (_ : Dependency.Acyclic rtr) ×' (_ : i ∈ s.rtr[Component.rcn]) ×' i ∉ s.progress),
    (invImage
            (fun a =>
              PSigma.casesOn a fun i snd =>
                PSigma.casesOn snd fun a snd =>
                  PSigma.casesOn snd fun h₁ snd =>
                    let_fun fin := ⋯;
                    (Set.Finite.toFinset fin).card)
            instWellFoundedRelation).1
        y { fst := i, snd := { fst := a, snd := { fst := h₁✝, snd := h₂✝ } } } →
      ∃ i, Allows s.toState i
h : ¬dependencies s.rtr i \ s.progress = ∅
w✝ : ID
hd : w✝ ∈ dependencies s.rtr i \ s.progress
h₁ : w✝ ∈ dependencies s.rtr i
h₂ : w✝ ∉ s.progress
⊢ (Set.Finite.toFinset ⋯).card < (Set.Finite.toFinset ⋯).card