Documentation

Regex.NFA.Compile.ProofData.Lemmas

theorem Regex.NFA.pushNode_wf {nfa : NFA} {node : Node} (wf : nfa.WellFormed) (inBounds : node.inBounds (nfa.nodes.size + 1)) :

(nfa.pushNode node).WellFormed

theorem Regex.NFA.pushRegex_wf {nfa : NFA} {next : Nat} {e : Data.Expr} (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

(nfa.pushRegex next e).WellFormed

theorem Regex.NFA.compile_wf {e : Data.Expr} :

(compile e).WellFormed

theorem Regex.NFA.Compile.ProofData.Empty.wf' [Empty] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfa'.WellFormed

theorem Regex.NFA.Compile.ProofData.Epsilon.wf' [Epsilon] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfa'.WellFormed

theorem Regex.NFA.Compile.ProofData.Char.wf' [Char] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfa'.WellFormed

theorem Regex.NFA.Compile.ProofData.Classes.wf' [Classes] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfa'.WellFormed

theorem Regex.NFA.Compile.ProofData.Group.wf_close [Group] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfaClose.WellFormed

theorem Regex.NFA.Compile.ProofData.Group.wf_expr [Group] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfaExpr.WellFormed

theorem Regex.NFA.Compile.ProofData.Group.wf' [Group] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfa'.WellFormed

theorem Regex.NFA.Compile.ProofData.Alternate.wf₁ [Alternate] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfa₁.WellFormed

theorem Regex.NFA.Compile.ProofData.Alternate.wf₂ [Alternate] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfa₂.WellFormed

theorem Regex.NFA.Compile.ProofData.Alternate.wf' [Alternate] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfa'.WellFormed

theorem Regex.NFA.Compile.ProofData.Concat.wf₂ [Concat] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfa₂.WellFormed

theorem Regex.NFA.Compile.ProofData.Concat.wf' [Concat] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfa'.WellFormed

theorem Regex.NFA.Compile.ProofData.Star.wf_placeholder [Star] (wf : nfa.WellFormed) :

nfaPlaceholder.WellFormed

theorem Regex.NFA.Compile.ProofData.Star.wf_expr [Star] (wf : nfa.WellFormed) :

nfaExpr.WellFormed

theorem Regex.NFA.Compile.ProofData.Star.wf' [Star] (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) :

nfa'.WellFormed