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

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq : nfa.pushRegex next r.star = 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₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)
Tactic:
have ih₂ : pathToNext nfa' next nfa.nodes.size nfa'.val.start cs₂ := ih₂ eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)
Tactic:
apply pushRegex.star eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
⊢ ∀ (placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size })
    (compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }) (patched : Array Node) (nfa'_1 : NFA)
    (isLt : nfa.nodes.size < patched.size) (inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size)
    (property : nfa.nodes.size < nfa'_1.nodes.size),
    placeholder = nfa.pushNode Node.fail ⋯ →
      compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r →
        patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next) →
          nfa'_1 = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds } →
            nfa' = ⟨nfa'_1, property⟩ → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
⊢ ∀ (placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size })
    (compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }) (patched : Array Node) (nfa'_1 : NFA)
    (isLt : nfa.nodes.size < patched.size) (inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size)
    (property : nfa.nodes.size < nfa'_1.nodes.size),
    placeholder = nfa.pushNode Node.fail ⋯ →
      compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r →
        patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next) →
          nfa'_1 = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds } →
            nfa' = ⟨nfa'_1, property⟩ → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) (cs₁ ++ cs₂)
Tactic:
intro placeholder compiled patched nfa' isLt inBounds property
  eq₁ eq₂ eq₃ eq₄ eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) (cs₁ ++ cs₂)
Tactic:
rw [eq]
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ (↑⟨nfa', property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨nfa', property⟩).start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ (↑⟨nfa', property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨nfa', property⟩).start) (cs₁ ++ cs₂)
Tactic:
simp
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
ih₂ : (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)
Tactic:
rw [eq] at ih₂
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : (↑⟨nfa', property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨nfa', property⟩).start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : (↑⟨nfa', property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨nfa', property⟩).start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)
Tactic:
simp at ih₂
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)
Tactic:
have eqStart : nfa'.start = nfa.nodes.size := by
  rw [eq₄]
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)
Tactic:
have ih₁ : pathToNext compiled nfa.nodes.size placeholder.val.nodes.size compiled.val.start cs₁ :=
  ih₁ eq₂.symm
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)
Tactic:
have ih₁ : pathToNext nfa' nfa.nodes.size placeholder.val.nodes.size compiled.val.start cs₁ := by
  apply ih₁.cast
  intro i h₁ h₂
  rw [eq₄]
  simp [eq₃]
  exists h₂
  simp [get_eq_nodes_get, eq₃]
  rw [Array.get_set_ne (hj := h₂)]
  simp
  apply Nat.ne_of_lt (Nat.lt_of_lt_of_le placeholder.property h₁)
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)
Tactic:
have ih₁ : pathToNext nfa' nfa.nodes.size nfa.nodes.size compiled.val.start cs₁ :=
  ih₁.castStart (Nat.le_of_lt placeholder.property)
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)
Tactic:
have ih₂ : pathToNext nfa' next nfa.nodes.size nfa.nodes.size cs₂ := by
  rw [eqStart] at ih₂
  exact ih₂
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂✝ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂✝ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)
Tactic:
have := ih₁.trans ih₂
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂✝ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
this : nfa'.pathToNext (↑next) nfa.nodes.size (↑(↑compiled).start) (cs₁ ++ cs₂)
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂✝ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
this : nfa'.pathToNext (↑next) nfa.nodes.size (↑(↑compiled).start) (cs₁ ++ cs₂)
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)
Tactic:
apply this.cons (.εStep (by simp [eqStart]) nfa'.start.isLt ?_)
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂✝ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
this : nfa'.pathToNext (↑next) nfa.nodes.size (↑(↑compiled).start) (cs₁ ++ cs₂)
⊢ ↑(↑compiled).start ∈ nfa'[↑nfa'.start].εStep

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂✝ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
this : nfa'.pathToNext (↑next) nfa.nodes.size (↑(↑compiled).start) (cs₁ ++ cs₂)
⊢ ↑(↑compiled).start ∈ nfa'[↑nfa'.start].εStep
Tactic:
rw [eq₄]
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂✝ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
this : nfa'.pathToNext (↑next) nfa.nodes.size (↑(↑compiled).start) (cs₁ ++ cs₂)
⊢ ↑(↑compiled).start ∈
    { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩,
          inBounds :=
            inBounds }[↑{ nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }.start].εStep

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂✝ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
this : nfa'.pathToNext (↑next) nfa.nodes.size (↑(↑compiled).start) (cs₁ ++ cs₂)
⊢ ↑(↑compiled).start ∈
    { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩,
          inBounds :=
            inBounds }[↑{ nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }.start].εStep
Tactic:
simp [get_eq_nodes_get, eq₃, Node.εStep]
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
⊢ ↑nfa'.start = nfa.nodes.size
Tactic:
rw [eq₄]
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
Tactic:
apply ih₁.cast
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ ∀ (i : ℕ),
    (↑placeholder).nodes.size ≤ i →
      ∀ (h₂ : i < (↑compiled).nodes.size), ∃ (h' : i < nfa'.nodes.size), (↑compiled)[i] = nfa'[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ ∀ (i : ℕ),
    (↑placeholder).nodes.size ≤ i →
      ∀ (h₂ : i < (↑compiled).nodes.size), ∃ (h' : i < nfa'.nodes.size), (↑compiled)[i] = nfa'[i]
Tactic:
intro i h₁ h₂
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ∃ (h' : i < nfa'.nodes.size), (↑compiled)[i] = nfa'[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ∃ (h' : i < nfa'.nodes.size), (↑compiled)[i] = nfa'[i]
Tactic:
rw [eq₄]
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ∃ (h' : i < { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }.nodes.size),
    (↑compiled)[i] = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ∃ (h' : i < { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }.nodes.size),
    (↑compiled)[i] = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }[i]
Tactic:
simp [eq₃]
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ∃ (h : i < (↑compiled).nodes.size),
    (↑compiled)[i] = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ∃ (h : i < (↑compiled).nodes.size),
    (↑compiled)[i] = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }[i]
Tactic:
exists h₂
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ (↑compiled)[i] = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ (↑compiled)[i] = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }[i]
Tactic:
simp [get_eq_nodes_get, eq₃]
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ (↑compiled).nodes[i] = ((↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next))[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ (↑compiled).nodes[i] = ((↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next))[i]
Tactic:
rw [Array.get_set_ne (hj := h₂)]
State after:
case h
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ↑⟨nfa.nodes.size, ⋯⟩ ≠ i

State before:
case h
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ↑⟨nfa.nodes.size, ⋯⟩ ≠ i
Tactic:
simp
State after:
case h
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ¬nfa.nodes.size = i

State before:
case h
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
i : ℕ
h₁ : (↑placeholder).nodes.size ≤ i
h₂ : i < (↑compiled).nodes.size
⊢ ¬nfa.nodes.size = i
Tactic:
apply Nat.ne_of_lt (Nat.lt_of_lt_of_le placeholder.property h₁)
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
Tactic:
rw [eqStart] at ih₂
State after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
Tactic:
exact ih₂
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
ih₂✝ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝¹ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁✝ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size nfa.nodes.size (↑(↑compiled).start) cs₁
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size nfa.nodes.size cs₂
this : nfa'.pathToNext (↑next) nfa.nodes.size (↑(↑compiled).start) (cs₁ ++ cs₂)
⊢ nfa.nodes.size ≤ ↑nfa'.start
Tactic:
simp [eqStart]
State after:
no goals