let I be non empty set ; :: thesis: for S being non empty FSM over 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 over 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 :: thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable

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:18;
( 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:17, FINSEQ_2:20;
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, FINSEQ_6:128;
v2 . 1 = w1 . 1 by A4, A6, FINSEQ_6:128;
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:80;
consider s2 being FinSequence such that
A10: w1 = v2 ^ s2 by FINSEQ_1:80;
reconsider s1 = s1, s2 = s2 as FinSequence of I by A9, A10, FINSEQ_1:36;
v1 <> {}

proof

assume A11: v1 = {} ; :: thesis: contradiction
A12: dom v1 = (dom w2) /\ (Seg (len w1)) by RELAT_1:61
.= (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:7;
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:61
.= (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:7;
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 ;
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:8
.= (GEN (v1, the InitS of S)) ^ (Del ((GEN (s1,q1)),1)) by A16, A18, Lm2 ;
the InitS of S,v2 -leads_to q2 ;
then GEN (w1, the InitS of S) = (Del ((GEN (v2, the InitS of S)),((len v2) + 1))) ^ (GEN (s2,q2)) by A10, FSM_1:8
.= (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:1;
hence GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ; :: thesis: verum

end;

end;

end;

end;

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