let IAlph, OAlph be non empty set ; for rtfsm, tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for qr1, qr2 being State of rtfsm st rtfsm = the_reduction_of tfsm & qr1 <> qr2 holds
not qr1,qr2 -are_equivalent
let rtfsm, tfsm be non empty finite Mealy-FSM of IAlph,OAlph; for qr1, qr2 being State of rtfsm st rtfsm = the_reduction_of tfsm & qr1 <> qr2 holds
not qr1,qr2 -are_equivalent
let qr1, qr2 be State of rtfsm; ( rtfsm = the_reduction_of tfsm & qr1 <> qr2 implies not qr1,qr2 -are_equivalent )
assume that
A1:
rtfsm = the_reduction_of tfsm
and
A2:
qr1 <> qr2
; not qr1,qr2 -are_equivalent
A3:
the carrier of rtfsm = final_states_partition tfsm
by A1, Def18;
then reconsider q19 = qr1 as Subset of tfsm by TARSKI:def 3;
consider x being Element of tfsm such that
A4:
x in q19
by A3, FINSEQ_4:102;
reconsider q29 = qr2 as Subset of tfsm by A3, TARSKI:def 3;
consider y being Element of tfsm such that
A5:
y in q29
by A3, FINSEQ_4:102;
A6:
final_states_partition tfsm is final
by Def15;
not x,y -are_equivalent
proof
assume
x,
y -are_equivalent
;
contradiction
then consider X being
Element of
rtfsm such that A7:
(
x in X &
y in X )
by A3, A6, Def14;
A8:
q29 misses q19
by A2, A3, EQREL_1:def 6;
X is
Subset of
tfsm
by A3, TARSKI:def 3;
then
(
X = q19 or
X misses q19 )
by A3, EQREL_1:def 6;
hence
contradiction
by A4, A5, A7, A8, XBOOLE_0:3;
verum
end;
then consider w being FinSequence of IAlph such that
A9:
x,w -response <> y,w -response
by Def10;
set q1adm = qr1,w -admissible ;
set q2adm = qr2,w -admissible ;
set xadm = x,w -admissible ;
set yadm = y,w -admissible ;
set xresp = x,w -response ;
set yresp = y,w -response ;
len (x,w -response ) =
len w
by Def6
.=
len (y,w -response )
by Def6
;
then consider k being Nat such that
A10:
( 1 <= k & k <= len (x,w -response ) )
and
A11:
(x,w -response ) . k <> (y,w -response ) . k
by A9, FINSEQ_1:18;
len (x,w -response ) = len w
by Def6;
then A12:
k in Seg (len w)
by A10, FINSEQ_1:3;
then
k in Seg ((len w) + 1)
by FINSEQ_2:9;
then A13:
(y,w -admissible ) . k in (qr2,w -admissible ) . k
by A1, A5, Th57;
set q1resp = qr1,w -response ;
set q2resp = qr2,w -response ;
A14: len (qr1,w -admissible ) =
(len w) + 1
by Def2
.=
(len (x,w -response )) + 1
by Def6
;
k in Seg (len (x,w -response ))
by A10, FINSEQ_1:3;
then A15:
k in Seg (len (qr1,w -admissible ))
by A14, FINSEQ_2:9;
then
k in dom (qr1,w -admissible )
by FINSEQ_1:def 3;
then A16:
(qr1,w -admissible ) . k is Element of rtfsm
by FINSEQ_2:13;
len (qr2,w -admissible ) =
(len w) + 1
by Def2
.=
len (qr1,w -admissible )
by Def2
;
then
k in dom (qr2,w -admissible )
by A15, FINSEQ_1:def 3;
then A17:
(qr2,w -admissible ) . k is Element of rtfsm
by FINSEQ_2:13;
k in dom w
by A12, FINSEQ_1:def 3;
then A18:
w . k is Element of IAlph
by FINSEQ_2:13;
A19: len (qr1,w -admissible ) =
(len w) + 1
by Def2
.=
len (x,w -admissible )
by Def2
;
then
k in dom (x,w -admissible )
by A15, FINSEQ_1:def 3;
then A20:
(x,w -admissible ) . k is Element of tfsm
by FINSEQ_2:13;
len (y,w -admissible ) =
(len w) + 1
by Def2
.=
len (x,w -admissible )
by Def2
;
then
k in dom (y,w -admissible )
by A15, A19, FINSEQ_1:def 3;
then A21:
(y,w -admissible ) . k is Element of tfsm
by FINSEQ_2:13;
k in Seg ((len w) + 1)
by A12, FINSEQ_2:9;
then A22:
(x,w -admissible ) . k in (qr1,w -admissible ) . k
by A1, A4, Th57;
now assume A23:
qr1,
w -response = qr2,
w -response
;
contradiction
len w = len (x,w -response )
by Def6;
then A24:
k in dom w
by A10, FINSEQ_3:27;
then A25:
(x,w -response ) . k = the
OFun of
tfsm . ((x,w -admissible ) . k),
(w . k)
by Def6;
A26:
(qr2,w -response ) . k =
the
OFun of
rtfsm . ((qr2,w -admissible ) . k),
(w . k)
by A24, Def6
.=
the
OFun of
tfsm . ((y,w -admissible ) . k),
(w . k)
by A1, A18, A17, A13, A21, Def18
;
(qr1,w -response ) . k =
the
OFun of
rtfsm . ((qr1,w -admissible ) . k),
(w . k)
by A24, Def6
.=
the
OFun of
tfsm . ((x,w -admissible ) . k),
(w . k)
by A1, A16, A18, A22, A20, Def18
;
hence
contradiction
by A11, A23, A24, A26, A25, Def6;
verum end;
hence
not qr1,qr2 -are_equivalent
by Def10; verum