Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case intro.intro.intro.intro.intro.step.εStep.base
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
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 : result = ⟨↑nfa''', property⟩
cs₂✝ cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs✝ : cs = [] ++ cs₂ ++ cs₂✝
cs₃ : List Char
path' : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₃
h✝ : nfa.nodes.size ≤ ↑(↑nfa').start
step : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa').start) (↑next) cs₂✝
heq : ↑(↑nfa').start = nfa.nodes.size ∧ cs₂✝ = []
rest : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) (↑(↑nfa').start) cs₂
this : (↑nfa'').pathIn nfa.nodes.size (↑(↑nfa'').start) (↑(↑nfa').start) cs₂
eqs : cs₂ = cs₃ ++ []
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₂
Tactic:
simp at eqs
Proof state after:
case intro.intro.intro.intro.intro.step.εStep.base
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
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 : result = ⟨↑nfa''', property⟩
cs₂✝ cs₂ : List Char
eqStart : (↑nfa''')[↑(↑nfa''').start] = Node.save (2 * i) ↑(↑nfa'').start
h₁✝ : nfa.nodes.size ≤ ↑(↑nfa''').start
h₂✝ : ↑(↑nfa''').start < (↑nfa''').nodes.size
eqs✝ : cs = [] ++ cs₂ ++ cs₂✝
cs₃ : List Char
path' : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₃
h✝ : nfa.nodes.size ≤ ↑(↑nfa').start
step : (↑nfa''').stepIn nfa.nodes.size (↑(↑nfa').start) (↑next) cs₂✝
heq : ↑(↑nfa').start = nfa.nodes.size ∧ cs₂✝ = []
rest : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa'').start) (↑(↑nfa').start) cs₂
this : (↑nfa'').pathIn nfa.nodes.size (↑(↑nfa'').start) (↑(↑nfa').start) cs₂
eqs : cs₂ = cs₃
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs₂