Theorem: Regex.NFA.pathToNext_of_matches.group (RegexCorrectness/NFA/Transition/Path/Equivalence/PathOfMatch.lean)

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Data.Expr.group i r) = nfa'
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
Tactic:
apply pushRegex.group eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Data.Expr.group i r) = nfa'
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
⊢ ∀ (nfa'_1 : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa'' : { nfa' // (↑nfa'_1).nodes.size < nfa'.nodes.size })
    (nfa''' : { nfa' // (↑nfa'').nodes.size < nfa'.nodes.size }) (property : nfa.nodes.size < (↑nfa''').nodes.size)
    (inBounds' : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1))
    (inBounds''' : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)),
    nfa'_1 = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds' →
      nfa'' = (↑nfa'_1).pushRegex (↑nfa'_1).start r →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds''' →
          nfa' = ⟨↑nfa''', property⟩ → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (Data.Expr.group i r) = nfa'
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
⊢ ∀ (nfa'_1 : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa'' : { nfa' // (↑nfa'_1).nodes.size < nfa'.nodes.size })
    (nfa''' : { nfa' // (↑nfa'').nodes.size < nfa'.nodes.size }) (property : nfa.nodes.size < (↑nfa''').nodes.size)
    (inBounds' : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1))
    (inBounds''' : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)),
    nfa'_1 = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds' →
      nfa'' = (↑nfa'_1).pushRegex (↑nfa'_1).start r →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds''' →
          nfa' = ⟨↑nfa''', property⟩ → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
Tactic:
intro nfa' nfa'' nfa''' property _ _ eq₁ eq₂ eq₃ eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) cs
Tactic:
rw [eq]
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑⟨↑nfa''', property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨↑nfa''', property⟩).start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑⟨↑nfa''', property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨↑nfa''', property⟩).start) cs
Tactic:
simp
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₃ : pathToNext nfa' next nfa.nodes.size nfa'.val.start [] := by
  have h₁ : nfa.nodes.size ≤ nfa'.val.start.val := by
    rw [eq₁]
    simp
  refine ⟨nfa'.val.start.val, [], [], rfl, .base h₁, ?_⟩
  refine .εStep h₁ nfa'.val.start.isLt ?_
  rw [eq₁]
  simp [Node.εStep]
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₃ : pathToNext nfa'' next nfa.nodes.size nfa'.val.start [] := by
  apply path₃.cast
  intro i _ h₂
  exists Nat.lt_trans h₂ nfa''.property
  rw [pushRegex_get_lt eq₂.symm _ h₂]
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₂ : pathToNext nfa'' nfa'.val.start nfa'.val.nodes.size nfa''.val.start cs :=
  ih eq₂.symm
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₂ : pathToNext nfa'' nfa'.val.start nfa.nodes.size nfa''.val.start cs :=
  path₂.castStart (Nat.le_of_lt nfa'.property)
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₂₃ : pathToNext nfa'' next nfa.nodes.size nfa''.val.start (cs ++ []) :=
  pathToNext.trans path₂ path₃
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) (cs ++ [])
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) (cs ++ [])
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
simp at path₂₃
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₂₃ : pathToNext nfa''' next nfa.nodes.size nfa''.val.start cs := by
  apply path₂₃.cast
  intro i _ h₂
  exists Nat.lt_trans h₂ nfa'''.property
  rw [eq₃, pushNode_get_lt _ h₂]
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₁ : pathToNext nfa''' nfa''.val.start nfa''.val.nodes.size nfa'''.val.start [] := by
  have h₁ : nfa''.val.nodes.size ≤ nfa'''.val.start.val := by
    rw [eq₃]
    simp
  refine ⟨nfa'''.val.start, [], [], rfl, .base h₁, ?_⟩
  refine .εStep h₁ nfa'''.val.start.isLt ?_
  rw [eq₃]
  simp [Node.εStep]
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₁ : (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₁ : (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₁ : pathToNext nfa''' nfa''.val.start nfa.nodes.size nfa'''.val.start [] := by
  apply path₁.castStart (Nat.le_of_lt ?_)
  exact Nat.lt_trans nfa'.property nfa''.property
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₁✝ : (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []
path₁ : (↑nfa''').pathToNext (↑(↑nfa'').start) nfa.nodes.size ↑(↑nfa''').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₁✝ : (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []
path₁ : (↑nfa''').pathToNext (↑(↑nfa'').start) nfa.nodes.size ↑(↑nfa''').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
exact pathToNext.trans path₁ path₂₃
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
Tactic:
have h₁ : nfa.nodes.size ≤ nfa'.val.start.val := by
  rw [eq₁]
  simp
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
h₁ : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
h₁ : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
Tactic:
refine ⟨nfa'.val.start.val, [], [], rfl, .base h₁, ?_⟩
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
h₁ : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ (↑nfa').stepIn nfa.nodes.size ↑(↑nfa').start ↑next []

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
h₁ : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ (↑nfa').stepIn nfa.nodes.size ↑(↑nfa').start ↑next []
Tactic:
refine .εStep h₁ nfa'.val.start.isLt ?_
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
h₁ : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑nfa')[↑(↑nfa').start].εStep

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
h₁ : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈ (↑nfa')[↑(↑nfa').start].εStep
Tactic:
rw [eq₁]
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
h₁ : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈
    (↑(nfa.pushNode (Node.save (2 * i + 1) ↑next)
            inBounds'✝))[↑(↑(nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝)).start].εStep

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
h₁ : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈
    (↑(nfa.pushNode (Node.save (2 * i + 1) ↑next)
            inBounds'✝))[↑(↑(nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝)).start].εStep
Tactic:
simp [Node.εStep]
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa').start
Tactic:
rw [eq₁]
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝)).start

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝)).start
Tactic:
simp
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
⊢ (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
Tactic:
apply path₃.cast
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
⊢ ∀ (i : ℕ),
    nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa').nodes.size), ∃ (h' : i < (↑nfa'').nodes.size), (↑nfa')[i] = (↑nfa'')[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
⊢ ∀ (i : ℕ),
    nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa').nodes.size), ∃ (h' : i < (↑nfa'').nodes.size), (↑nfa')[i] = (↑nfa'')[i]
Tactic:
intro i _ h₂
State after:
nfa : NFA
next : Fin nfa.nodes.size
i✝ : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i✝ r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i✝ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i✝) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i✝) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa').nodes.size
⊢ ∃ (h' : i < (↑nfa'').nodes.size), (↑nfa')[i] = (↑nfa'')[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
i✝ : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i✝ r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i✝ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i✝) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i✝) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa').nodes.size
⊢ ∃ (h' : i < (↑nfa'').nodes.size), (↑nfa')[i] = (↑nfa'')[i]
Tactic:
exists Nat.lt_trans h₂ nfa''.property
State after:
nfa : NFA
next : Fin nfa.nodes.size
i✝ : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i✝ r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i✝ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i✝) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i✝) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa').nodes.size
⊢ (↑nfa')[i] = (↑nfa'')[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
i✝ : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i✝ r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i✝ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i✝) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i✝) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa').nodes.size
⊢ (↑nfa')[i] = (↑nfa'')[i]
Tactic:
rw [pushRegex_get_lt eq₂.symm _ h₂]
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
Tactic:
apply path₂₃.cast
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ ∀ (i : ℕ),
    nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa'').nodes.size), ∃ (h' : i < (↑nfa''').nodes.size), (↑nfa'')[i] = (↑nfa''')[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ ∀ (i : ℕ),
    nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa'').nodes.size), ∃ (h' : i < (↑nfa''').nodes.size), (↑nfa'')[i] = (↑nfa''')[i]
Tactic:
intro i _ h₂
State after:
nfa : NFA
next : Fin nfa.nodes.size
i✝ : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i✝ r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i✝ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i✝) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i✝) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa'').nodes.size
⊢ ∃ (h' : i < (↑nfa''').nodes.size), (↑nfa'')[i] = (↑nfa''')[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
i✝ : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i✝ r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i✝ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i✝) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i✝) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa'').nodes.size
⊢ ∃ (h' : i < (↑nfa''').nodes.size), (↑nfa'')[i] = (↑nfa''')[i]
Tactic:
exists Nat.lt_trans h₂ nfa'''.property
State after:
nfa : NFA
next : Fin nfa.nodes.size
i✝ : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i✝ r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i✝ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i✝) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i✝) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa'').nodes.size
⊢ (↑nfa'')[i] = (↑nfa''')[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
i✝ : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i✝ r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i✝ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i✝) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i✝ + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i✝) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa'').nodes.size
⊢ (↑nfa'')[i] = (↑nfa''')[i]
Tactic:
rw [eq₃, pushNode_get_lt _ h₂]
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []
Tactic:
have h₁ : nfa''.val.nodes.size ≤ nfa'''.val.start.val := by
  rw [eq₃]
  simp
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
h₁ : (↑nfa'').nodes.size ≤ ↑(↑nfa''').start
⊢ (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
h₁ : (↑nfa'').nodes.size ≤ ↑(↑nfa''').start
⊢ (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []
Tactic:
refine ⟨nfa'''.val.start, [], [], rfl, .base h₁, ?_⟩
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
h₁ : (↑nfa'').nodes.size ≤ ↑(↑nfa''').start
⊢ (↑nfa''').stepIn (↑nfa'').nodes.size ↑(↑nfa''').start ↑(↑nfa'').start []

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
h₁ : (↑nfa'').nodes.size ≤ ↑(↑nfa''').start
⊢ (↑nfa''').stepIn (↑nfa'').nodes.size ↑(↑nfa''').start ↑(↑nfa'').start []
Tactic:
refine .εStep h₁ nfa'''.val.start.isLt ?_
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
h₁ : (↑nfa'').nodes.size ≤ ↑(↑nfa''').start
⊢ ↑(↑nfa'').start ∈ (↑nfa''')[↑(↑nfa''').start].εStep

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
h₁ : (↑nfa'').nodes.size ≤ ↑(↑nfa''').start
⊢ ↑(↑nfa'').start ∈ (↑nfa''')[↑(↑nfa''').start].εStep
Tactic:
rw [eq₃]
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
h₁ : (↑nfa'').nodes.size ≤ ↑(↑nfa''').start
⊢ ↑(↑nfa'').start ∈
    (↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start)
            inBounds'''✝))[↑(↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝)).start].εStep

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
h₁ : (↑nfa'').nodes.size ≤ ↑(↑nfa''').start
⊢ ↑(↑nfa'').start ∈
    (↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start)
            inBounds'''✝))[↑(↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝)).start].εStep
Tactic:
simp [Node.εStep]
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa'').nodes.size ≤ ↑(↑nfa''').start
Tactic:
rw [eq₃]
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa'').nodes.size ≤ ↑(↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝)).start

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
⊢ (↑nfa'').nodes.size ≤ ↑(↑((↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝)).start
Tactic:
simp
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₁ : (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []
⊢ (↑nfa''').pathToNext (↑(↑nfa'').start) nfa.nodes.size ↑(↑nfa''').start []
Tactic:
apply path₁.castStart (Nat.le_of_lt ?_)
State after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₁ : (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []
⊢ nfa.nodes.size < (↑nfa'').nodes.size

State before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₁ : (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []
⊢ nfa.nodes.size < (↑nfa'').nodes.size
Tactic:
exact Nat.lt_trans nfa'.property nfa''.property
State after:
no goals