let I be non empty set ; :: thesis: for S being non empty FSM of I st S is regular & S is calculating_type holds
for s, s1, s2 being Element of I
for q being State of S st the Tran of S . [the InitS of S,s1] <> the Tran of S . [the InitS of S,s2] holds
the Tran of S . [q,s] <> the InitS of S
let S be non empty FSM of I; :: thesis: ( S is regular & S is calculating_type implies for s, s1, s2 being Element of I
for q being State of S st the Tran of S . [the InitS of S,s1] <> the Tran of S . [the InitS of S,s2] holds
the Tran of S . [q,s] <> the InitS of S )
assume A1:
( S is regular & S is calculating_type )
; :: thesis: for s, s1, s2 being Element of I
for q being State of S st the Tran of S . [the InitS of S,s1] <> the Tran of S . [the InitS of S,s2] holds
the Tran of S . [q,s] <> the InitS of S
let s, s1, s2 be Element of I; :: thesis: for q being State of S st the Tran of S . [the InitS of S,s1] <> the Tran of S . [the InitS of S,s2] holds
the Tran of S . [q,s] <> the InitS of S
let q be State of S; :: thesis: ( the Tran of S . [the InitS of S,s1] <> the Tran of S . [the InitS of S,s2] implies the Tran of S . [q,s] <> the InitS of S )
assume A2:
the Tran of S . [the InitS of S,s1] <> the Tran of S . [the InitS of S,s2]
; :: thesis: the Tran of S . [q,s] <> the InitS of S
q is accessible
by A1, Def4;
then consider w being FinSequence of I such that
A3:
the InitS of S,w -leads_to q
by Def3;
A4:
(GEN w,the InitS of S) . ((len w) + 1) = q
by A3, FSM_1:def 3;
assume A5:
the Tran of S . [q,s] = the InitS of S
; :: thesis: contradiction
reconsider w1 = <*s,s1*>, w2 = <*s,s2*> as FinSequence of I ;
A6:
GEN w1,q = <*q,the InitS of S,(the Tran of S . [the InitS of S,s1])*>
by A5, Th2;
GEN w2,q = <*q,the InitS of S,(the Tran of S . [the InitS of S,s2])*>
by A5, Th2;
then A7:
( (GEN w1,q) . 3 = the Tran of S . [the InitS of S,s1] & (GEN w2,q) . 3 = the Tran of S . [the InitS of S,s2] )
by A6, FINSEQ_1:62;
A8:
( len w1 = 2 & len w2 = 2 )
by FINSEQ_1:61;
then
( 1 <= 3 & 3 <= (len w1) + 1 & 3 <= (len w2) + 1 )
;
then A9:
( (GEN (w ^ w1),the InitS of S) . ((len w) + 3) = the Tran of S . [the InitS of S,s1] & (GEN (w ^ w2),the InitS of S) . ((len w) + 3) = the Tran of S . [the InitS of S,s2] )
by A3, A7, FSM_1:22;
per cases
( w = {} or w <> {} )
;
suppose
w = {}
;
:: thesis: contradictionthen A10:
len w = 0
;
A11:
(
GEN w1,the
InitS of
S = <*the InitS of S,(the Tran of S . [the InitS of S,s]),(the Tran of S . [(the Tran of S . [the InitS of S,s]),s1])*> &
GEN w2,the
InitS of
S = <*the InitS of S,(the Tran of S . [the InitS of S,s]),(the Tran of S . [(the Tran of S . [the InitS of S,s]),s2])*> )
by Th2;
A12:
(
w1 . 1
= s &
w2 . 1
= s )
by FINSEQ_1:61;
A13:
( 3
<= (len w1) + 1 & 3
<= (len w2) + 1 )
by A8;
A14:
(GEN w1,the InitS of S) . 3 =
the
Tran of
S . [(the Tran of S . [the InitS of S,s]),s1]
by A11, FINSEQ_1:62
.=
the
Tran of
S . [the InitS of S,s1]
by A4, A5, A10, FSM_1:def 2
;
(GEN w2,the InitS of S) . 3 =
the
Tran of
S . [(the Tran of S . [the InitS of S,s]),s2]
by A11, FINSEQ_1:62
.=
the
Tran of
S . [the InitS of S,s2]
by A4, A5, A10, FSM_1:def 2
;
hence
contradiction
by A1, A2, A12, A13, A14, Def1;
:: thesis: verum end; suppose
w <> {}
;
:: thesis: contradictionthen consider s' being
set ,
w' being
FinSequence such that A15:
(
w = <*s'*> ^ w' &
len w = (len w') + 1 )
by REWRITE1:5;
dom <*s'*> = Seg 1
by FINSEQ_1:def 8;
then A16:
1
in dom <*s'*>
by FINSEQ_1:3;
then A17:
w . 1 =
<*s'*> . 1
by A15, FINSEQ_1:def 7
.=
s'
by FINSEQ_1:def 8
;
dom <*s'*> c= dom w
by A15, FINSEQ_1:39;
then A18:
(
(w ^ w1) . 1
= s' &
(w ^ w2) . 1
= s' )
by A16, A17, FINSEQ_1:def 7;
(
(len (w ^ w1)) + 1
= ((len w) + 2) + 1 &
(len (w ^ w2)) + 1
= ((len w) + 2) + 1 )
by A8, FINSEQ_1:35;
hence
contradiction
by A1, A2, A9, A18, Def1;
:: thesis: verum end;