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 & len w2 <> 0 ) by A3;
then ( len w1 > 0 & len w2 > 0 ) ;
then ( len w1 >= 0 + 1 & len w2 >= 0 + 1 & 1 <= 1 ) by NAT_1:13;
then ( v1 . 1 = w2 . 1 & v2 . 1 = w1 . 1 ) by A4, GRAPH_2:2;
then A6: ( 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;
consider s1 being FinSequence such that
A7: w2 = v1 ^ s1 by TREES_1:3;
consider s2 being FinSequence such that
A8: w1 = v2 ^ s2 by TREES_1:3;
reconsider s1 = s1, s2 = s2 as FinSequence of I by A7, A8, FINSEQ_1:50;
v1 <> {}

proof

assume A9: v1 = {} ; :: thesis: contradiction
A10: 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 A10, FINSEQ_1:9;
then ( len v1 = len w2 or len v1 = len w1 ) by FINSEQ_1:def 3;
then ( 0 = len w2 or 0 = len w1 ) by A9;
hence contradiction by A3; :: thesis: verum

end;

then len v1 <> 0 ;
then ( 1 <= len v1 & len v1 <= len v1 ) by NAT_1:14;
then consider WI being Element of I, QI, QI1 being State of S such that
A11: ( 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 A12: len v2 = 0 ;
A13: 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 A13, FINSEQ_1:9;
hence contradiction by A5, A12, FINSEQ_1:def 3; :: thesis: verum

end;

then len v2 <> 0 ;
then ( 1 <= len v2 & len v2 <= len v2 ) by NAT_1:14;
then consider WI2 being Element of I, QI2, QI12 being State of S such that
A14: ( 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;
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 A11, A14;
A15: ( (GEN s1,q1) . 1 = q1 & (GEN s2,q2) . 1 = q2 & len (GEN v1,the InitS of S) = (len v1) + 1 & 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 A16: GEN w2,the InitS of S = (Del (GEN v1,the InitS of S),((len v1) + 1)) ^ (GEN s1,q1) by A7, FSM_1:23
.= (GEN v1,the InitS of S) ^ (Del (GEN s1,q1),1) by A15, 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 A8, FSM_1:23
.= (GEN v2,the InitS of S) ^ (Del (GEN s2,q2),1) by A15, 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 A6, A16, 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