def Regex.NFA.Node.charStep (n : Node) (c : Char) : Set ℕ

Equations

• (Regex.NFA.Node.char c' next).charStep c = if (c == c') = true then {next} else ∅
• (Regex.NFA.Node.sparse cs next).charStep c = if c ∈ cs then {next} else ∅
• n.charStep c = ∅

def Regex.NFA.Node.εStep (n : Node) : Set ℕ

Equations

• (Regex.NFA.Node.epsilon next).εStep = {next}
• (Regex.NFA.Node.split next₁ next₂).εStep = {next₁, next₂}
• (Regex.NFA.Node.save offset next).εStep = {next}
• n.εStep = ∅

def Regex.NFA.charStep (nfa : NFA) (i : ℕ) (c : Char) : Set ℕ

Equations

• nfa.charStep i c = if h : i < nfa.nodes.size then nfa[i].charStep c else ∅

def Regex.NFA.εStep (nfa : NFA) (i : ℕ) : Set ℕ

Equations

• nfa.εStep i = if h : i < nfa.nodes.size then nfa[i].εStep else ∅

theorem Regex.NFA.charStep_of_charStep {j : ℕ} {nfa : NFA} {i : ℕ} {c : Char} {h : i < nfa.nodes.size} (mem : j ∈ nfa[i].charStep c) : j ∈ nfa.charStep i c

theorem Regex.NFA.εStep_of_εStep {j : ℕ} {nfa : NFA} {i : ℕ} {h : i < nfa.nodes.size} (mem : j ∈ nfa[i].εStep) : j ∈ nfa.εStep i

theorem Regex.NFA.lt_of_inBounds_of_charStep {node : Node} {j k : ℕ} {c : Char} (inBounds : node.inBounds k) (mem : j ∈ node.charStep c) : j < k

theorem Regex.NFA.lt_of_inBounds_of_εStep {node : Node} {j k : ℕ} (inBounds : node.inBounds k) (mem : j ∈ node.εStep) : j < k

theorem Regex.NFA.lt_of_εStep {nfa : NFA} {i j : ℕ} {h : i < nfa.nodes.size} (wf : nfa.WellFormed) (mem : j ∈ nfa[i].εStep) : j < nfa.nodes.size

theorem Regex.NFA.lt_of_charStep {c : Char} {nfa : NFA} {i j : ℕ} {h : i < nfa.nodes.size} (wf : nfa.WellFormed) (mem : j ∈ nfa[i].charStep c) : j < nfa.nodes.size