Theorem: Regex.NFA.matches_of_path.alternate
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate r₂) = result
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₁ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₂ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₂
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
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)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
neStart₂ : ↑next ≠ ↑start₂
get₂ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑final)[i]
get₁ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₁).nodes.size), (↑nfa₁)[i] = (↑final)[i]
i✝ : ℕ
cs₂ : List Char
step✝ : (↑final).stepIn nfa.nodes.size i✝ (↑next) cs₂
j✝ : ℕ
cs₄ : List Char
rest : (↑final).pathIn nfa.nodes.size (↑start₂) i✝ cs₄
h₁✝ : nfa.nodes.size ≤ ↑(↑final).start
h₂✝ : ↑(↑final).start < (↑final).nodes.size
eqs : cs = cs₄ ++ cs₂
eqs₂ : j✝ = ↑start₂
this✝ : (↑final).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs
this : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs
i j : ℕ
h₁ : (↑nfa₁).nodes.size ≤ i
h₂ : i < (↑nfa₂).nodes.size
step : (∃ c, j ∈ (↑nfa₂)[i].charStep c) ∨ j ∈ (↑nfa₂)[i].εStep
hj : nfa.nodes.size ≤ j
⊢ (↑nfa₁).nodes.size ≤ j
Tactic:
have := eq_or_ge_of_step_pushRegex eq₃.symm h₁ h₂ step
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.alternate r₂) = result
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₁ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₁
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r₂ = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r₂
nfa₁ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
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)
final : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑final).nodes.size
eq₁ : nfa₁ = nfa.pushRegex next r₁
eq₂ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : final = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds
eq' : result = ⟨↑final, property⟩
startNode : (↑final)[↑(↑final).start] = Node.split ↑start₁ ↑start₂
neStart₁ : ↑next ≠ ↑start₁
neStart₂ : ↑next ≠ ↑start₂
get₂ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑final)[i]
get₁ : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₁).nodes.size), (↑nfa₁)[i] = (↑final)[i]
i✝ : ℕ
cs₂ : List Char
step✝ : (↑final).stepIn nfa.nodes.size i✝ (↑next) cs₂
j✝ : ℕ
cs₄ : List Char
rest : (↑final).pathIn nfa.nodes.size (↑start₂) i✝ cs₄
h₁✝ : nfa.nodes.size ≤ ↑(↑final).start
h₂✝ : ↑(↑final).start < (↑final).nodes.size
eqs : cs = cs₄ ++ cs₂
eqs₂ : j✝ = ↑start₂
this✝¹ : (↑final).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs
this✝ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs
i j : ℕ
h₁ : (↑nfa₁).nodes.size ≤ i
h₂ : i < (↑nfa₂).nodes.size
step : (∃ c, j ∈ (↑nfa₂)[i].charStep c) ∨ j ∈ (↑nfa₂)[i].εStep
hj : nfa.nodes.size ≤ j
this : j = ↑⟨↑next, ⋯⟩ ∨ (↑nfa₁).nodes.size ≤ j
⊢ (↑nfa₁).nodes.size ≤ j