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 holds

GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) 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 holds

GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) implies S is calculating_type )

assume A1: 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 ; :: thesis: S is calculating_type

let j be non zero Element of NAT ; :: according to FSM_2:def 1 :: thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds

(GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j

let w1, w2 be FinSequence of I; :: thesis: ( w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j )

assume that

A2: w1 . 1 = w2 . 1 and

A3: j <= (len w1) + 1 and

A4: j <= (len w2) + 1 ; :: thesis: (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j

A5: dom (GEN (w1, the InitS of S)) = Seg (len (GEN (w1, the InitS of S))) by FINSEQ_1:def 3

.= Seg ((len w1) + 1) by FSM_1:def 2 ;

A6: dom (GEN (w2, the InitS of S)) = Seg (len (GEN (w2, the InitS of S))) by FINSEQ_1:def 3

.= Seg ((len w2) + 1) by FSM_1:def 2 ;

A7: 1 <= j by NAT_1:14;

then A8: j in dom (GEN (w1, the InitS of S)) by A3, A5, FINSEQ_1:1;

j in dom (GEN (w2, the InitS of S)) by A4, A6, A7, FINSEQ_1:1;

then A9: j in (dom (GEN (w1, the InitS of S))) /\ (dom (GEN (w2, the InitS of S))) by A8, XBOOLE_0:def 4;

GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable by A1, A2;

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

then GEN (w1, the InitS of S) tolerates GEN (w2, the InitS of S) by PARTFUN1:54;

hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by A9, PARTFUN1:def 4; :: thesis: verum

GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) 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 holds

GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) implies S is calculating_type )

assume A1: 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 ; :: thesis: S is calculating_type

let j be non zero Element of NAT ; :: according to FSM_2:def 1 :: thesis: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 holds

(GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j

let w1, w2 be FinSequence of I; :: thesis: ( w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j )

assume that

A2: w1 . 1 = w2 . 1 and

A3: j <= (len w1) + 1 and

A4: j <= (len w2) + 1 ; :: thesis: (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j

A5: dom (GEN (w1, the InitS of S)) = Seg (len (GEN (w1, the InitS of S))) by FINSEQ_1:def 3

.= Seg ((len w1) + 1) by FSM_1:def 2 ;

A6: dom (GEN (w2, the InitS of S)) = Seg (len (GEN (w2, the InitS of S))) by FINSEQ_1:def 3

.= Seg ((len w2) + 1) by FSM_1:def 2 ;

A7: 1 <= j by NAT_1:14;

then A8: j in dom (GEN (w1, the InitS of S)) by A3, A5, FINSEQ_1:1;

j in dom (GEN (w2, the InitS of S)) by A4, A6, A7, FINSEQ_1:1;

then A9: j in (dom (GEN (w1, the InitS of S))) /\ (dom (GEN (w2, the InitS of S))) by A8, XBOOLE_0:def 4;

GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable by A1, A2;

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

then GEN (w1, the InitS of S) tolerates GEN (w2, the InitS of S) by PARTFUN1:54;

hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by A9, PARTFUN1:def 4; :: thesis: verum