Documentation
Regex
.
NFA
.
Compile
.
Lemmas
Search
return to top
source
Imports
Init
Regex.NFA.Compile.Basic
Imported by
Regex
.
NFA
.
pushRegex_size_lt
source
theorem
Regex
.
NFA
.
pushRegex_size_lt
{
nfa
:
NFA
}
{
next
:
Nat
}
{
e
:
Data.Expr
}
:
nfa
.
nodes
.
size
<
(
nfa
.
pushRegex
next
e
)
.
nodes
.
size