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

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

hence
S is calculating_type
by Th5; :: thesis: verumGEN (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

end;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
end;

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

end;

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

end;

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 <> {}

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 <> {}

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;( 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

then
1 <= len v1
by NAT_1:14;
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;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

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

then
1 <= len v2
by NAT_1:14;
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 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

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