Theorem: Regex.NFA.ge_pushRegex_start (RegexCorrectness/NFA/Compile.lean)

State before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
induction r generalizing nfa next with
| empty =>
  apply pushRegex.empty eq
  intro eq
  subst eq
  simp
| epsilon =>
  apply pushRegex.epsilon eq
  intro eq
  subst eq
  simp
| char c =>
  apply pushRegex.char eq
  intro eq
  subst eq
  simp
| classes c =>
  apply pushRegex.sparse eq
  intro eq
  subst eq
  simp
| group =>
  apply pushRegex.group eq
  intro nfa' nfa'' nfa''' property _ _ _ _ eq₃ eq
  rw [eq]
  simp
  rw [eq₃]
  simp
  apply Nat.le_of_lt (Nat.lt_trans nfa'.property nfa''.property)
| alternate r₁ r₂ =>
  apply pushRegex.alternate eq
  intro nfa₁ _ nfa₂ _ _ _ _ _ _ _ _ eq₅ eq
  rw [eq]
  simp
  rw [eq₅]
  simp [pushNode]
  exact Nat.le_of_lt (Nat.lt_trans nfa₁.property nfa₂.property)
| concat r₁ r₂ ih₁ =>
  apply pushRegex.concat eq
  intro nfa₂ nfa₁ _ _ eq₁ eq
  rw [eq]
  simp
  exact Nat.le_trans (Nat.le_of_lt nfa₂.property) (ih₁ eq₁.symm)
| star r =>
  apply pushRegex.star eq
  intro _ _ _ nfa' _ _ _ _ _ _ eq₄ eq
  rw [eq]
  simp
  rw [eq₄]
State after:
no goals

State before:
case empty
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.empty = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.empty eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.empty = result
⊢ result = nfa.pushNode Node.fail ⋯ → nfa.nodes.size ≤ ↑(↑result).start

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.empty = result
⊢ result = nfa.pushNode Node.fail ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next Data.Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next Data.Expr.empty = result
eq : result = nfa.pushNode Node.fail ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
subst eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode Node.fail ⋯)).start

State before:
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode Node.fail ⋯)).start
Tactic:
simp
State after:
no goals

State before:
case epsilon
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.epsilon eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = result
⊢ result = nfa.pushNode (Node.epsilon ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next Data.Expr.epsilon = result
⊢ result = nfa.pushNode (Node.epsilon ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next Data.Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start

State before:
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next Data.Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
subst eq
State after:
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next Data.Expr.epsilon = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start

State before:
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next Data.Expr.epsilon = nfa.pushNode (Node.epsilon ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).start
Tactic:
simp
State after:
no goals

State before:
case char
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.char eq
State after:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = result
⊢ result = nfa.pushNode (Node.char c ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start

State before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.char c) = result
⊢ result = nfa.pushNode (Node.char c ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro eq
State after:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start

State before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.char c) = result
eq : result = nfa.pushNode (Node.char c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
subst eq
State after:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.char c) = nfa.pushNode (Node.char c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start

State before:
c : Char
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.char c) = nfa.pushNode (Node.char c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start
Tactic:
simp
State after:
no goals

State before:
case classes
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes c) = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.sparse eq
State after:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes c) = result
⊢ result = nfa.pushNode (Node.sparse c ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start

State before:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes c) = result
⊢ result = nfa.pushNode (Node.sparse c ↑next) ⋯ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro eq
State after:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.classes c) = result
eq : result = nfa.pushNode (Node.sparse c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start

State before:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.classes c) = result
eq : result = nfa.pushNode (Node.sparse c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
subst eq
State after:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.classes c) = nfa.pushNode (Node.sparse c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.sparse c ↑next) ⋯)).start

State before:
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.classes c) = nfa.pushNode (Node.sparse c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.sparse c ↑next) ⋯)).start
Tactic:
simp
State after:
no goals

State before:
case group
a✝¹ : ℕ
a✝ : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.group a✝¹ a✝) = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.group eq
State after:
a✝¹ : ℕ
a✝ : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.group a✝¹ a✝) = result
⊢ ∀ (nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size })
    (nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }) (property : nfa.nodes.size < (↑nfa''').nodes.size)
    (inBounds' : (Node.save (2 * a✝¹ + 1) ↑next).inBounds (nfa.nodes.size + 1))
    (inBounds''' : (Node.save (2 * a✝¹) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)),
    nfa' = nfa.pushNode (Node.save (2 * a✝¹ + 1) ↑next) inBounds' →
      nfa'' = (↑nfa').pushRegex (↑nfa').start a✝ →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝¹) ↑(↑nfa'').start) inBounds''' →
          result = ⟨↑nfa''', property⟩ → nfa.nodes.size ≤ ↑(↑result).start

State before:
a✝¹ : ℕ
a✝ : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.group a✝¹ a✝) = result
⊢ ∀ (nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size })
    (nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }) (property : nfa.nodes.size < (↑nfa''').nodes.size)
    (inBounds' : (Node.save (2 * a✝¹ + 1) ↑next).inBounds (nfa.nodes.size + 1))
    (inBounds''' : (Node.save (2 * a✝¹) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)),
    nfa' = nfa.pushNode (Node.save (2 * a✝¹ + 1) ↑next) inBounds' →
      nfa'' = (↑nfa').pushRegex (↑nfa').start a✝ →
        nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝¹) ↑(↑nfa'').start) inBounds''' →
          result = ⟨↑nfa''', property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro nfa' nfa'' nfa''' property _ _ _ _ eq₃ eq
State after:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start

State before:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
rw [eq]
State after:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa''', property⟩).start

State before:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa''', property⟩).start
Tactic:
simp
State after:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa''').start

State before:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa''').start
Tactic:
rw [eq₃]
State after:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑((↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝)).start

State before:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ ↑(↑((↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝)).start
Tactic:
simp
State after:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ (↑nfa'').nodes.size

State before:
a✝³ : ℕ
a✝² : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next a✝² = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.group a✝³ a✝²) = result
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * a✝³ + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * a✝³) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
a✝¹ : nfa' = nfa.pushNode (Node.save (2 * a✝³ + 1) ↑next) inBounds'✝
a✝ : nfa'' = (↑nfa').pushRegex (↑nfa').start a✝²
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * a✝³) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
⊢ nfa.nodes.size ≤ (↑nfa'').nodes.size
Tactic:
apply Nat.le_of_lt (Nat.lt_trans nfa'.property nfa''.property)
State after:
no goals

State before:
case alternate
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.alternate r₂) = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.alternate eq
State after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.alternate r₂) = result
⊢ ∀ (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),
    nfa₁ = nfa.pushRegex next r₁ →
      start₁ = (↑nfa₁).start →
        nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂ →
          start₂ = (↑nfa₂).start →
            nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds →
              result = ⟨↑nfa', property⟩ → nfa.nodes.size ≤ ↑(↑result).start

State before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.alternate r₂) = result
⊢ ∀ (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),
    nfa₁ = nfa.pushRegex next r₁ →
      start₁ = (↑nfa₁).start →
        nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂ →
          start₂ = (↑nfa₂).start →
            nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds →
              result = ⟨↑nfa', property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro nfa₁ _ nfa₂ _ _ _ _ _ _ _ _ eq₅ eq
State after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
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
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start

State before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
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
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
rw [eq]
State after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
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
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa'✝, property✝⟩).start

State before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
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
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa'✝, property✝⟩).start
Tactic:
simp
State after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
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
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa'✝).start

State before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
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
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa'✝).start
Tactic:
rw [eq₅]
State after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
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
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑((↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝)).start

State before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
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
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑((↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝)).start
Tactic:
simp [pushNode]
State after:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
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
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ nfa.nodes.size ≤ (↑nfa₂).nodes.size

State before:
r₁ r₂ : Data.Expr
a_ih✝¹ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.alternate r₂) = result
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
a✝³ : nfa₁ = nfa.pushRegex next r₁
a✝² : start₁✝ = (↑nfa₁).start
a✝¹ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
a✝ : start₂✝ = (↑nfa₂).start
eq₅ : nfa'✝ = (↑nfa₂).pushNode (Node.split ↑start₁✝ ↑start₂✝) inBounds✝
eq : result = ⟨↑nfa'✝, property✝⟩
⊢ 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:
case concat
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.concat r₂) = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.concat eq
State after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.concat r₂) = result
⊢ ∀ (nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size })
    (property : nfa.nodes.size < (↑nfa₁).nodes.size),
    nfa₂ = nfa.pushRegex next r₂ →
      nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁ → result = ⟨↑nfa₁, property⟩ → nfa.nodes.size ≤ ↑(↑result).start

State before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (r₁.concat r₂) = result
⊢ ∀ (nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }) (nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size })
    (property : nfa.nodes.size < (↑nfa₁).nodes.size),
    nfa₂ = nfa.pushRegex next r₂ →
      nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁ → result = ⟨↑nfa₁, property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro nfa₂ nfa₁ _ _ eq₁ eq
State after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start

State before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
rw [eq]
State after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa₁, property✝⟩).start

State before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨↑nfa₁, property✝⟩).start
Tactic:
simp
State after:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa₁).start

State before:
r₁ r₂ : Data.Expr
ih₁ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result → nfa.nodes.size ≤ ↑(↑result).start
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
nfa₂ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa₁ : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property✝ : nfa.nodes.size < (↑nfa₁).nodes.size
a✝ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq : result = ⟨↑nfa₁, property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑nfa₁).start
Tactic:
exact Nat.le_trans (Nat.le_of_lt nfa₂.property) (ih₁ eq₁.symm)
State after:
no goals

State before:
case star
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r.star = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
apply pushRegex.star eq
State after:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r.star = result
⊢ ∀ (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),
    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' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds } →
            result = ⟨nfa', property⟩ → nfa.nodes.size ≤ ↑(↑result).start

State before:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r.star = result
⊢ ∀ (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),
    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' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds } →
            result = ⟨nfa', property⟩ → nfa.nodes.size ≤ ↑(↑result).start
Tactic:
intro _ _ _ nfa' _ _ _ _ _ _ eq₄ eq
State after:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
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
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start

State before:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
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
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑result).start
Tactic:
rw [eq]
State after:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
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
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨nfa', property✝⟩).start

State before:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
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
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑(↑⟨nfa', property✝⟩).start
Tactic:
simp
State after:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
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
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑nfa'.start

State before:
r : Data.Expr
a_ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result → nfa.nodes.size ≤ ↑(↑result).start
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
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
a✝² : placeholder✝ = nfa.pushNode Node.fail ⋯
a✝¹ : compiled✝ = (↑placeholder✝).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
a✝ : patched✝ = (↑compiled✝).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled✝).start ↑next)
eq₄ : nfa' = { nodes := patched✝, start := ⟨nfa.nodes.size, isLt✝⟩, inBounds := inBounds✝ }
eq : result = ⟨nfa', property✝⟩
⊢ nfa.nodes.size ≤ ↑nfa'.start
Tactic:
rw [eq₄]
State after:
no goals