let I be non empty set ; :: thesis: for S being non empty FSM over I st S is regular & S is calculating_type holds

for s, s1, s2 being Element of I

for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds

the Tran of S . [q,s] <> the InitS of S

let S be non empty FSM over I; :: thesis: ( S is regular & S is calculating_type implies for s, s1, s2 being Element of I

for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds

the Tran of S . [q,s] <> the InitS of S )

assume that

A1: S is regular and

A2: S is calculating_type ; :: thesis: for s, s1, s2 being Element of I

for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds

the Tran of S . [q,s] <> the InitS of S

let s, s1, s2 be Element of I; :: thesis: for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds

the Tran of S . [q,s] <> the InitS of S

let q be State of S; :: thesis: ( the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] implies the Tran of S . [q,s] <> the InitS of S )

assume A3: the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] ; :: thesis: the Tran of S . [q,s] <> the InitS of S

q is accessible by A1;

then consider w being FinSequence of I such that

A4: the InitS of S,w -leads_to q ;

A5: (GEN (w, the InitS of S)) . ((len w) + 1) = q by A4;

assume A6: the Tran of S . [q,s] = the InitS of S ; :: thesis: contradiction

reconsider w1 = <*s,s1*>, w2 = <*s,s2*> as FinSequence of I ;

A7: GEN (w1,q) = <*q, the InitS of S,( the Tran of S . [ the InitS of S,s1])*> by A6, Th2;

A8: GEN (w2,q) = <*q, the InitS of S,( the Tran of S . [ the InitS of S,s2])*> by A6, Th2;

A9: (GEN (w1,q)) . 3 = the Tran of S . [ the InitS of S,s1] by A7, FINSEQ_1:45;

A10: (GEN (w2,q)) . 3 = the Tran of S . [ the InitS of S,s2] by A8, FINSEQ_1:45;

A11: len w1 = 2 by FINSEQ_1:44;

A12: len w2 = 2 by FINSEQ_1:44;

A13: 3 <= (len w1) + 1 by A11;

A14: 3 <= (len w2) + 1 by A12;

A15: (GEN ((w ^ w1), the InitS of S)) . ((len w) + 3) = the Tran of S . [ the InitS of S,s1] by A4, A9, A13, FSM_1:7;

A16: (GEN ((w ^ w2), the InitS of S)) . ((len w) + 3) = the Tran of S . [ the InitS of S,s2] by A4, A10, A14, FSM_1:7;

for s, s1, s2 being Element of I

for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds

the Tran of S . [q,s] <> the InitS of S

let S be non empty FSM over I; :: thesis: ( S is regular & S is calculating_type implies for s, s1, s2 being Element of I

for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds

the Tran of S . [q,s] <> the InitS of S )

assume that

A1: S is regular and

A2: S is calculating_type ; :: thesis: for s, s1, s2 being Element of I

for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds

the Tran of S . [q,s] <> the InitS of S

let s, s1, s2 be Element of I; :: thesis: for q being State of S st the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] holds

the Tran of S . [q,s] <> the InitS of S

let q be State of S; :: thesis: ( the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] implies the Tran of S . [q,s] <> the InitS of S )

assume A3: the Tran of S . [ the InitS of S,s1] <> the Tran of S . [ the InitS of S,s2] ; :: thesis: the Tran of S . [q,s] <> the InitS of S

q is accessible by A1;

then consider w being FinSequence of I such that

A4: the InitS of S,w -leads_to q ;

A5: (GEN (w, the InitS of S)) . ((len w) + 1) = q by A4;

assume A6: the Tran of S . [q,s] = the InitS of S ; :: thesis: contradiction

reconsider w1 = <*s,s1*>, w2 = <*s,s2*> as FinSequence of I ;

A7: GEN (w1,q) = <*q, the InitS of S,( the Tran of S . [ the InitS of S,s1])*> by A6, Th2;

A8: GEN (w2,q) = <*q, the InitS of S,( the Tran of S . [ the InitS of S,s2])*> by A6, Th2;

A9: (GEN (w1,q)) . 3 = the Tran of S . [ the InitS of S,s1] by A7, FINSEQ_1:45;

A10: (GEN (w2,q)) . 3 = the Tran of S . [ the InitS of S,s2] by A8, FINSEQ_1:45;

A11: len w1 = 2 by FINSEQ_1:44;

A12: len w2 = 2 by FINSEQ_1:44;

A13: 3 <= (len w1) + 1 by A11;

A14: 3 <= (len w2) + 1 by A12;

A15: (GEN ((w ^ w1), the InitS of S)) . ((len w) + 3) = the Tran of S . [ the InitS of S,s1] by A4, A9, A13, FSM_1:7;

A16: (GEN ((w ^ w2), the InitS of S)) . ((len w) + 3) = the Tran of S . [ the InitS of S,s2] by A4, A10, A14, FSM_1:7;

per cases
( w = {} or w <> {} )
;

end;

suppose
w = {}
; :: thesis: contradiction

then A17:
len w = 0
;

A18: GEN (w1, the InitS of S) = <* the InitS of S,( the Tran of S . [ the InitS of S,s]),( the Tran of S . [( the Tran of S . [ the InitS of S,s]),s1])*> by Th2;

A19: GEN (w2, the InitS of S) = <* the InitS of S,( the Tran of S . [ the InitS of S,s]),( the Tran of S . [( the Tran of S . [ the InitS of S,s]),s2])*> by Th2;

A20: w1 . 1 = s by FINSEQ_1:44;

A21: w2 . 1 = s by FINSEQ_1:44;

A22: 3 <= (len w1) + 1 by A11;

A23: 3 <= (len w2) + 1 by A12;

A24: (GEN (w1, the InitS of S)) . 3 = the Tran of S . [( the Tran of S . [ the InitS of S,s]),s1] by A18, FINSEQ_1:45

.= the Tran of S . [ the InitS of S,s1] by A5, A6, A17, FSM_1:def 2 ;

(GEN (w2, the InitS of S)) . 3 = the Tran of S . [( the Tran of S . [ the InitS of S,s]),s2] by A19, FINSEQ_1:45

.= the Tran of S . [ the InitS of S,s2] by A5, A6, A17, FSM_1:def 2 ;

hence contradiction by A2, A3, A20, A21, A22, A23, A24; :: thesis: verum

end;A18: GEN (w1, the InitS of S) = <* the InitS of S,( the Tran of S . [ the InitS of S,s]),( the Tran of S . [( the Tran of S . [ the InitS of S,s]),s1])*> by Th2;

A19: GEN (w2, the InitS of S) = <* the InitS of S,( the Tran of S . [ the InitS of S,s]),( the Tran of S . [( the Tran of S . [ the InitS of S,s]),s2])*> by Th2;

A20: w1 . 1 = s by FINSEQ_1:44;

A21: w2 . 1 = s by FINSEQ_1:44;

A22: 3 <= (len w1) + 1 by A11;

A23: 3 <= (len w2) + 1 by A12;

A24: (GEN (w1, the InitS of S)) . 3 = the Tran of S . [( the Tran of S . [ the InitS of S,s]),s1] by A18, FINSEQ_1:45

.= the Tran of S . [ the InitS of S,s1] by A5, A6, A17, FSM_1:def 2 ;

(GEN (w2, the InitS of S)) . 3 = the Tran of S . [( the Tran of S . [ the InitS of S,s]),s2] by A19, FINSEQ_1:45

.= the Tran of S . [ the InitS of S,s2] by A5, A6, A17, FSM_1:def 2 ;

hence contradiction by A2, A3, A20, A21, A22, A23, A24; :: thesis: verum

suppose
w <> {}
; :: thesis: contradiction

then consider s9 being object , w9 being FinSequence such that

A25: w = <*s9*> ^ w9 and

len w = (len w9) + 1 by REWRITE1:5;

dom <*s9*> = Seg 1 by FINSEQ_1:def 8;

then A26: 1 in dom <*s9*> by FINSEQ_1:1;

then A27: w . 1 = <*s9*> . 1 by A25, FINSEQ_1:def 7

.= s9 by FINSEQ_1:def 8 ;

A28: dom <*s9*> c= dom w by A25, FINSEQ_1:26;

then A29: (w ^ w1) . 1 = s9 by A26, A27, FINSEQ_1:def 7;

A30: (w ^ w2) . 1 = s9 by A26, A27, A28, FINSEQ_1:def 7;

A31: (len (w ^ w1)) + 1 = ((len w) + 2) + 1 by A11, FINSEQ_1:22;

(len (w ^ w2)) + 1 = ((len w) + 2) + 1 by A12, FINSEQ_1:22;

hence contradiction by A2, A3, A15, A16, A29, A30, A31; :: thesis: verum

end;A25: w = <*s9*> ^ w9 and

len w = (len w9) + 1 by REWRITE1:5;

dom <*s9*> = Seg 1 by FINSEQ_1:def 8;

then A26: 1 in dom <*s9*> by FINSEQ_1:1;

then A27: w . 1 = <*s9*> . 1 by A25, FINSEQ_1:def 7

.= s9 by FINSEQ_1:def 8 ;

A28: dom <*s9*> c= dom w by A25, FINSEQ_1:26;

then A29: (w ^ w1) . 1 = s9 by A26, A27, FINSEQ_1:def 7;

A30: (w ^ w2) . 1 = s9 by A26, A27, A28, FINSEQ_1:def 7;

A31: (len (w ^ w1)) + 1 = ((len w) + 2) + 1 by A11, FINSEQ_1:22;

(len (w ^ w2)) + 1 = ((len w) + 2) + 1 by A12, FINSEQ_1:22;

hence contradiction by A2, A3, A15, A16, A29, A30, A31; :: thesis: verum