let IAlph, OAlph be non empty set ; for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm st qa,qb -are_equivalent holds
for w being FinSequence of IAlph
for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent )
let tfsm be non empty Mealy-FSM over IAlph,OAlph; for qa, qb being State of tfsm st qa,qb -are_equivalent holds
for w being FinSequence of IAlph
for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent )
let qa, qb be State of tfsm; ( qa,qb -are_equivalent implies for w being FinSequence of IAlph
for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent ) )
assume A1:
qa,qb -are_equivalent
; for w being FinSequence of IAlph
for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent )
let w be FinSequence of IAlph; for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent )
defpred S1[ Nat] means ( $1 in Seg (len w) implies ex qai, qbi being Element of tfsm st
( qai = ((qa,w) -admissible) . $1 & qbi = ((qb,w) -admissible) . $1 & qai,qbi -are_equivalent ) );
A2:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A3:
(
i in Seg (len w) implies ex
qai,
qbi being
Element of
tfsm st
(
qai = ((qa,w) -admissible) . i &
qbi = ((qb,w) -admissible) . i &
qai,
qbi -are_equivalent ) )
;
S1[i + 1]
A4:
(
i = 0 or (
0 < i &
0 + 1
= 1 ) )
;
assume
i + 1
in Seg (len w)
;
ex qai, qbi being Element of tfsm st
( qai = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )
then
i + 1
<= len w
by FINSEQ_1:1;
then A5:
(
0 = i or ( 1
<= i &
i <= len w ) )
by A4, NAT_1:13;
per cases
( i = 0 or i in Seg (len w) )
by A5, FINSEQ_1:1;
suppose A6:
i = 0
;
ex qai, qbi being Element of tfsm st
( qai = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )reconsider qai =
((qa,w) -admissible) . 1,
qbi =
((qb,w) -admissible) . 1 as
Element of
tfsm by Def2;
take
qai
;
ex qbi being Element of tfsm st
( qai = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )take
qbi
;
( qai = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )thus
qai = ((qa,w) -admissible) . (i + 1)
by A6;
( qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )thus
qbi = ((qb,w) -admissible) . (i + 1)
by A6;
qai,qbi -are_equivalent
qai = qa
by Def2;
hence
qai,
qbi -are_equivalent
by A1, Def2;
verum end; suppose A7:
i in Seg (len w)
;
ex qai, qbi being Element of tfsm st
( qai = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai,qbi -are_equivalent )then A8:
( 1
<= i &
i <= len w )
by FINSEQ_1:1;
then consider wi being
Element of
IAlph,
qai9,
qai19 being
Element of
tfsm such that A9:
(
wi = w . i &
qai9 = ((qa,w) -admissible) . i )
and A10:
qai19 = ((qa,w) -admissible) . (i + 1)
and A11:
wi -succ_of qai9 = qai19
by Def2;
take
qai19
;
ex qbi being Element of tfsm st
( qai19 = ((qa,w) -admissible) . (i + 1) & qbi = ((qb,w) -admissible) . (i + 1) & qai19,qbi -are_equivalent )consider wi9 being
Element of
IAlph,
qbi9,
qbi19 being
Element of
tfsm such that A12:
(
wi9 = w . i &
qbi9 = ((qb,w) -admissible) . i )
and A13:
qbi19 = ((qb,w) -admissible) . (i + 1)
and A14:
wi9 -succ_of qbi9 = qbi19
by A8, Def2;
take
qbi19
;
( qai19 = ((qa,w) -admissible) . (i + 1) & qbi19 = ((qb,w) -admissible) . (i + 1) & qai19,qbi19 -are_equivalent )thus
qai19 = ((qa,w) -admissible) . (i + 1)
by A10;
( qbi19 = ((qb,w) -admissible) . (i + 1) & qai19,qbi19 -are_equivalent )thus
qbi19 = ((qb,w) -admissible) . (i + 1)
by A13;
qai19,qbi19 -are_equivalent thus
qai19,
qbi19 -are_equivalent
by A3, A7, A9, A11, A12, A14, Th19;
verum end;
end;
A15:
Seg (len w) = dom w
by FINSEQ_1:def 3;
A16:
S1[ 0 ]
by FINSEQ_1:1;
for i being Nat holds S1[i]
from NAT_1:sch 2(A16, A2);
hence
for i being Nat st i in dom w holds
ex qai, qbi being State of tfsm st
( qai = ((qa,w) -admissible) . i & qbi = ((qb,w) -admissible) . i & qai,qbi -are_equivalent )
by A15; verum