Documentation
Acmoi
.
Exercise1_14
Search
Google site search
return to top
source
Imports
Init
Mathlib.Computability.DFA
Imported by
u
α
instDecidableEqα
instDecidableEqFinOfNatNat_acmoi
q0
q1
TwoState
uniquely_accepts
automatic_complexity_is_at_most
q0_ne_q1
TwoState_stay_q0
TwoState_stay_q1
TwoState_accepts_repeat
either_or
either_or_strong
TwoState_no_return_to_q0
TwoState_accepts_only_starts_z
TwoState_accepts_only_repeat
complexity_of_repeat
source
axiom
u
:
ℕ
source
def
α
:
Type
Equations
α
=
Fin
u
Instances For
source
noncomputable instance
instDecidableEqα
:
DecidableEq
α
Equations
instDecidableEqα
=
Classical.decEq
α
source
noncomputable instance
instDecidableEqFinOfNatNat_acmoi
:
DecidableEq
(
Fin
2
)
Equations
instDecidableEqFinOfNatNat_acmoi
=
Classical.decEq
(
Fin
2
)
source
def
q0
:
Fin
2
Equations
q0
=
⟨
0
,
q0.proof_1
⟩
Instances For
source
def
q1
:
Fin
2
Equations
q1
=
⟨
1
,
q1.proof_1
⟩
Instances For
source
noncomputable def
TwoState
(z :
α
)
:
DFA
α
(
Fin
2
)
Equations
TwoState
z
=
{
step
:=
fun (
q
:
Fin
2
) (
b
:
α
) =>
if
q
=
q0
then
if
b
=
z
then
q0
else
q1
else
q1
,
start
:=
q0
,
accept
:=
{
q0
}
}
Instances For
source
def
uniquely_accepts
{τ :
Type
}
(M :
DFA
α
τ
)
(s :
List
α
)
:
Prop
Equations
uniquely_accepts
M
s
=
∀ (
t
:
List
α
),
t
.length
=
s
.length
→
(
M
.accepts
t
↔
t
=
s
)
Instances For
source
def
automatic_complexity_is_at_most
:
List
α
→
ℕ
→
Prop
Equations
automatic_complexity_is_at_most
s
k
=
∃ (
M
:
DFA
α
(
Fin
k
)
),
uniquely_accepts
M
s
Instances For
source
theorem
q0_ne_q1
:
q0
≠
q1
source
theorem
TwoState_stay_q0
{a :
α
}
{z :
α
}
(h :
(
TwoState
z
)
.eval
[
a
]
=
q0
)
:
a
=
z
source
theorem
TwoState_stay_q1
(z :
α
)
(x :
List
α
)
:
(
TwoState
z
)
.evalFrom
q1
x
=
q1
source
theorem
TwoState_accepts_repeat
{z :
α
}
{n :
ℕ
}
:
(
TwoState
z
)
.eval
(
List.replicate
n
z
)
=
q0
source
theorem
either_or
{a :
Fin
2
}
(h :
↑
a
≠
1
)
:
↑
a
=
0
source
theorem
either_or_strong
{a :
Fin
2
}
(not_zero :
a
≠
q0
)
:
a
=
q1
source
theorem
TwoState_no_return_to_q0
{q :
Fin
2
}
{z :
α
}
{x :
List
α
}
(h :
(
TwoState
z
)
.evalFrom
q
x
=
q0
)
:
q
=
q0
source
theorem
TwoState_accepts_only_starts_z
{a :
α
}
{z :
α
}
{y :
List
α
}
(hq0 :
(
TwoState
z
)
.eval
(
a
::
y
)
=
q0
)
:
a
=
z
source
theorem
TwoState_accepts_only_repeat
{z :
α
}
{x :
List
α
}
:
(
TwoState
z
)
.eval
x
=
q0
→
x
=
List.replicate
x
.length
z
source
theorem
complexity_of_repeat
(z :
α
)
(n :
ℕ
)
:
automatic_complexity_is_at_most
(
List.replicate
n
z
)
2