Documentation
Cslib
.
Computability
.
Automata
.
NABuchiEquiv
Search
return to top
source
Imports
Init
Cslib.Computability.Automata.NA
Imported by
Cslib
.
Automata
.
NA
.
Buchi
.
reindex
Cslib
.
Automata
.
NA
.
Buchi
.
reindex_run_iff
Cslib
.
Automata
.
NA
.
Buchi
.
reindex_run_iff'
Cslib
.
Automata
.
NA
.
Buchi
.
reindex_language_eq
Equivalence of nondeterministic Buchi automata (NBAs).
#
source
def
Cslib
.
Automata
.
NA
.
Buchi
.
reindex
{
Symbol
:
Type
u}
{
State
:
Type
v}
{
State'
:
Type
w}
(
f
:
State
≃
State'
)
:
Buchi
State
Symbol
≃
Buchi
State'
Symbol
Lifts an equivalence on states to an equivalence on NBAs.
Equations
One or more equations did not get rendered due to their size.
Instances For
source
theorem
Cslib
.
Automata
.
NA
.
Buchi
.
reindex_run_iff
{
Symbol
:
Type
u}
{
State
:
Type
v}
{
State'
:
Type
w}
{
f
:
State
≃
State'
}
{
nba
:
Buchi
State
Symbol
}
{
xs
:
ωSequence
Symbol
}
{
ss'
:
ωSequence
State'
}
:
(
(
reindex
f
)
nba
)
.
Run
xs
ss'
↔
nba
.
Run
xs
(
ωSequence.map
(⇑
f
.
symm
)
ss'
)
source
@[simp]
theorem
Cslib
.
Automata
.
NA
.
Buchi
.
reindex_run_iff'
{
Symbol
:
Type
u}
{
State
:
Type
v}
{
State'
:
Type
w}
{
f
:
State
≃
State'
}
{
nba
:
Buchi
State
Symbol
}
{
xs
:
ωSequence
Symbol
}
{
ss
:
ωSequence
State
}
:
(
(
reindex
f
)
nba
)
.
Run
xs
(
ωSequence.map
(⇑
f
)
ss
)
↔
nba
.
Run
xs
ss
source
@[simp]
theorem
Cslib
.
Automata
.
NA
.
Buchi
.
reindex_language_eq
{
Symbol
:
Type
u}
{
State
:
Type
v}
{
State'
:
Type
w}
{
f
:
State
≃
State'
}
{
nba
:
Buchi
State
Symbol
}
:
ωAcceptor.language
(
(
reindex
f
)
nba
)
=
ωAcceptor.language
nba