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

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate 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.alternate eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate 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 }) (start₁ : Fin (↑nfa₁).nodes.size)
    (nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }) (start₂ : Fin (↑nfa₂).nodes.size)
    (inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1))
    (nfa'_1 : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }) (property : nfa.nodes.size < (↑nfa'_1).nodes.size),
    nfa₁ = nfa.pushRegex next r₁ →
      start₁ = (↑nfa₁).start →
        nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂ →
          start₂ = (↑nfa₂).start →
            nfa'_1 = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds →
              nfa' = ⟨↑nfa'_1, property⟩ → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate 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 }) (start₁ : Fin (↑nfa₁).nodes.size)
    (nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }) (start₂ : Fin (↑nfa₂).nodes.size)
    (inBounds : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1))
    (nfa'_1 : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }) (property : nfa.nodes.size < (↑nfa'_1).nodes.size),
    nfa₁ = nfa.pushRegex next r₁ →
      start₁ = (↑nfa₁).start →
        nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂ →
          start₂ = (↑nfa₂).start →
            nfa'_1 = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds →
              nfa' = ⟨↑nfa'_1, property⟩ → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
Tactic:
intro nfa₁ start₁ nfa₂ start₂ _ nfa' property eq₁ eq₂ eq₃ _ eq₅ eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
⊢ (↑nfa'✝).pathToNext (↑next) nfa.nodes.size (↑(↑nfa'✝).start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑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
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑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
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑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
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
Tactic:
have : pathToNext nfa₁ next nfa.nodes.size nfa₁.val.start cs := ih eq₁.symm
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this : (↑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
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
Tactic:
have : pathToNext nfa' next nfa.nodes.size nfa₁.val.start cs := by
  apply this.cast
  intro i _ h₂
  have lt₂ : i < nfa₂.val.nodes.size := Nat.lt_trans h₂ nfa₂.property
  have : i < nfa'.val.nodes.size := Nat.lt_trans lt₂ nfa'.property
  exists this
  simp [eq₅]
  rw [pushNode_get_lt _ lt₂]
  rw [pushRegex_get_lt eq₃.symm _ h₂]
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑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
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
Tactic:
apply this.cons (.εStep ?_ nfa'.val.start.isLt ?_)
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ nfa.nodes.size ≤ ↑(↑nfa').start

nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ ↑(↑nfa₁).start ∈ (↑nfa')[↑(↑nfa').start].εStep

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ nfa.nodes.size ≤ ↑(↑nfa').start

nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ ↑(↑nfa₁).start ∈ (↑nfa')[↑(↑nfa').start].εStep
Tactic:
. rw [eq₅]
  simp
  exact Nat.le_of_lt (Nat.lt_trans nfa₁.property nfa₂.property)
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ ↑(↑nfa₁).start ∈ (↑nfa')[↑(↑nfa').start].εStep

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ ↑(↑nfa₁).start ∈ (↑nfa')[↑(↑nfa').start].εStep
Tactic:
. rw [eq₅]
  simp [Node.εStep, eq₂]
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
Tactic:
apply this.cast
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this : (↑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
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this : (↑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
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this : (↑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
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this : (↑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:
have lt₂ : i < nfa₂.val.nodes.size := Nat.lt_trans h₂ nfa₂.property
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₁).nodes.size
lt₂ : i < (↑nfa₂).nodes.size
⊢ ∃ (h' : i < (↑nfa').nodes.size), (↑nfa₁)[i] = (↑nfa')[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₁).nodes.size
lt₂ : i < (↑nfa₂).nodes.size
⊢ ∃ (h' : i < (↑nfa').nodes.size), (↑nfa₁)[i] = (↑nfa')[i]
Tactic:
have : i < nfa'.val.nodes.size := Nat.lt_trans lt₂ nfa'.property
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₁).nodes.size
lt₂ : i < (↑nfa₂).nodes.size
this : i < (↑nfa').nodes.size
⊢ ∃ (h' : i < (↑nfa').nodes.size), (↑nfa₁)[i] = (↑nfa')[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₁).nodes.size
lt₂ : i < (↑nfa₂).nodes.size
this : i < (↑nfa').nodes.size
⊢ ∃ (h' : i < (↑nfa').nodes.size), (↑nfa₁)[i] = (↑nfa')[i]
Tactic:
exists this
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₁).nodes.size
lt₂ : i < (↑nfa₂).nodes.size
this : i < (↑nfa').nodes.size
⊢ (↑nfa₁)[i] = (↑nfa')[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₁).nodes.size
lt₂ : i < (↑nfa₂).nodes.size
this : i < (↑nfa').nodes.size
⊢ (↑nfa₁)[i] = (↑nfa')[i]
Tactic:
simp [eq₅]
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₁).nodes.size
lt₂ : i < (↑nfa₂).nodes.size
this : i < (↑nfa').nodes.size
⊢ (↑nfa₁)[i] = (↑((↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝))[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₁).nodes.size
lt₂ : i < (↑nfa₂).nodes.size
this : i < (↑nfa').nodes.size
⊢ (↑nfa₁)[i] = (↑((↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝))[i]
Tactic:
rw [pushNode_get_lt _ lt₂]
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₁).nodes.size
lt₂ : i < (↑nfa₂).nodes.size
this : i < (↑nfa').nodes.size
⊢ (↑nfa₁)[i] = (↑nfa₂)[i]

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
i : ℕ
h₁✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₁).nodes.size
lt₂ : i < (↑nfa₂).nodes.size
this : 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
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑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
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ nfa.nodes.size ≤ ↑(↑((↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝)).start

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ nfa.nodes.size ≤ ↑(↑((↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝)).start
Tactic:
simp
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ nfa.nodes.size ≤ (↑nfa₂).nodes.size

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ nfa.nodes.size ≤ (↑nfa₂).nodes.size
Tactic:
exact Nat.le_of_lt (Nat.lt_trans nfa₁.property nfa₂.property)
State after:
no goals

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ ↑(↑nfa₁).start ∈ (↑nfa')[↑(↑nfa').start].εStep
Tactic:
rw [eq₅]
State after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ ↑(↑nfa₁).start ∈
    (↑((↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂)
            inBounds✝))[↑(↑((↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝)).start].εStep

State before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
⊢ ↑(↑nfa₁).start ∈
    (↑((↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂)
            inBounds✝))[↑(↑((↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝)).start].εStep
Tactic:
simp [Node.εStep, eq₂]
State after:
no goals