let I be non empty set ; :: thesis: for S being non empty FSM of I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN w1,the InitS of S = GEN w2,the InitS of S ) holds
S is calculating_type
let S be non empty FSM of I; :: thesis: ( ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN w1,the InitS of S = GEN w2,the InitS of S ) implies S is calculating_type )
assume A1: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN w1,the InitS of S = GEN w2,the InitS of S ; :: thesis: S is calculating_type

now

let w1, w2 be FinSequence of I; :: thesis: ( w1 . 1 = w2 . 1 implies GEN w1,the InitS of S, GEN w2,the InitS of S are_c=-comparable )
assume A2: w1 . 1 = w2 . 1 ; :: thesis: GEN w1,the InitS of S, GEN w2,the InitS of S are_c=-comparable
thus GEN w1,the InitS of S, GEN w2,the InitS of S are_c=-comparable :: thesis: verum

proof

per cases ( w1 = <*> I or w2 = <*> I or ( w1 <> {} & w2 <> {} ) ) ;

suppose ( w1 = <*> I or w2 = <*> I ) ; :: thesis: GEN w1,the InitS of S, GEN w2,the InitS of S are_c=-comparable

hence GEN w1,the InitS of S, GEN w2,the InitS of S are_c=-comparable by Lm1; :: thesis: verum

end;

suppose A3: ( w1 <> {} & w2 <> {} ) ; :: thesis: GEN w1,the InitS of S, GEN w2,the InitS of S are_c=-comparable

reconsider v1 = w2 | (Seg (len w1)), v2 = w1 | (Seg (len w2)) as FinSequence of I by FINSEQ_1:23;
( len w1 <= len w2 or len w2 <= len w1 ) ;
then A4: ( ( v1 = w2 & len v2 = len w2 & len w1 >= len w2 ) or ( len v1 = len w1 & v2 = w1 & len w1 <= len w2 ) ) by FINSEQ_1:21, FINSEQ_2:23;
A5: len w1 >= 0 + 1 by A3, NAT_1:13;
A6: len w2 >= 0 + 1 by A3, NAT_1:13;
A7: v1 . 1 = w2 . 1 by A4, A5, GRAPH_2:2;
v2 . 1 = w1 . 1 by A4, A6, GRAPH_2:2;
then A8: ( GEN v1,the InitS of S = GEN w1,the InitS of S or GEN v2,the InitS of S = GEN w2,the InitS of S ) by A1, A2, A4, A7;
consider s1 being FinSequence such that
A9: w2 = v1 ^ s1 by FINSEQ_1:101;
consider s2 being FinSequence such that
A10: w1 = v2 ^ s2 by FINSEQ_1:101;
reconsider s1 = s1, s2 = s2 as FinSequence of I by A9, A10, FINSEQ_1:50;
v1 <> {}

proof

assume A11: v1 = {} ; :: thesis: contradiction
A12: dom v1 = (dom w2) /\ (Seg (len w1)) by RELAT_1:90
.= (Seg (len w2)) /\ (Seg (len w1)) by FINSEQ_1:def 3 ;
( len w2 <= len w1 or len w1 <= len w2 ) ;
then ( dom v1 = Seg (len w2) or dom v1 = Seg (len w1) ) by A12, FINSEQ_1:9;
then ( len v1 = len w2 or len v1 = len w1 ) by FINSEQ_1:def 3;
hence contradiction by A3, A11; :: thesis: verum

end;

then 1 <= len v1 by NAT_1:14;
then A13: ex WI being Element of I ex QI, QI1 being State of S st
( WI = v1 . (len v1) & QI = (GEN v1,the InitS of S) . (len v1) & QI1 = (GEN v1,the InitS of S) . ((len v1) + 1) & WI -succ_of QI = QI1 ) by FSM_1:def 2;
v2 <> {}

proof

assume v2 = {} ; :: thesis: contradiction
then A14: len v2 = 0 ;
A15: dom v2 = (dom w1) /\ (Seg (len w2)) by RELAT_1:90
.= (Seg (len w1)) /\ (Seg (len w2)) by FINSEQ_1:def 3 ;
( len w2 <= len w1 or len w1 <= len w2 ) ;
then ( dom v2 = Seg (len w2) or dom v2 = Seg (len w1) ) by A15, FINSEQ_1:9;
hence contradiction by A3, A14, FINSEQ_1:def 3; :: thesis: verum

end;

then 1 <= len v2 by NAT_1:14;
then ex WI2 being Element of I ex QI2, QI12 being State of S st
( WI2 = v2 . (len v2) & QI2 = (GEN v2,the InitS of S) . (len v2) & QI12 = (GEN v2,the InitS of S) . ((len v2) + 1) & WI2 -succ_of QI2 = QI12 ) by FSM_1:def 2;
then reconsider q1 = (GEN v1,the InitS of S) . ((len v1) + 1), q2 = (GEN v2,the InitS of S) . ((len v2) + 1) as State of S by A13;
A16: (GEN s1,q1) . 1 = q1 by FSM_1:def 2;
A17: (GEN s2,q2) . 1 = q2 by FSM_1:def 2;
A18: len (GEN v1,the InitS of S) = (len v1) + 1 by FSM_1:def 2;
A19: len (GEN v2,the InitS of S) = (len v2) + 1 by FSM_1:def 2;
the InitS of S,v1 -leads_to q1 by FSM_1:def 3;
then A20: GEN w2,the InitS of S = (Del (GEN v1,the InitS of S),((len v1) + 1)) ^ (GEN s1,q1) by A9, FSM_1:23
.= (GEN v1,the InitS of S) ^ (Del (GEN s1,q1),1) by A16, A18, Lm2 ;
the InitS of S,v2 -leads_to q2 by FSM_1:def 3;
then GEN w1,the InitS of S = (Del (GEN v2,the InitS of S),((len v2) + 1)) ^ (GEN s2,q2) by A10, FSM_1:23
.= (GEN v2,the InitS of S) ^ (Del (GEN s2,q2),1) by A17, A19, Lm2 ;
then ( GEN w1,the InitS of S c= GEN w2,the InitS of S or GEN w2,the InitS of S c= GEN w1,the InitS of S ) by A8, A20, TREES_1:8;
hence GEN w1,the InitS of S, GEN w2,the InitS of S are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;

end;

end;

end;

hence S is calculating_type by Th5; :: thesis: verum