let IAlph, OAlph be non empty set ; for tfsm, rtfsm being non empty finite Mealy-FSM over IAlph,OAlph
for qr1, qr2 being State of rtfsm st rtfsm = the_reduction_of tfsm & qr1 <> qr2 holds
not qr1,qr2 -are_equivalent
let tfsm, rtfsm be non empty finite Mealy-FSM over 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:87;
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:87;
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;
A8:
q29 misses q19
by A2, A3, EQREL_1:def 4;
X is
Subset of
tfsm
by A3, TARSKI:def 3;
then
(
X = q19 or
X misses q19 )
by A3, EQREL_1:def 4;
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
;
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:14;
len ((x,w) -response) = len w
by Def6;
then A12:
k in Seg (len w)
by A10, FINSEQ_1:1;
then
k in Seg ((len w) + 1)
by FINSEQ_2:8;
then A13:
((y,w) -admissible) . k in ((qr2,w) -admissible) . k
by A1, A5, Th40;
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:1;
then A15:
k in Seg (len ((qr1,w) -admissible))
by A14, FINSEQ_2:8;
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:11;
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:11;
k in dom w
by A12, FINSEQ_1:def 3;
then A18:
w . k is Element of IAlph
by FINSEQ_2:11;
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:11;
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:11;
k in Seg ((len w) + 1)
by A12, FINSEQ_2:8;
then A22:
((x,w) -admissible) . k in ((qr1,w) -admissible) . k
by A1, A4, Th40;
now not (qr1,w) -response = (qr2,w) -response 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:25;
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
; verum