let I be non empty set ; 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; ( 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
; 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; 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; ( 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]
; 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
; 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 <> {} )
;
suppose
w = {}
;
contradictionthen 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;
verum end; suppose
w <> {}
;
contradictionthen 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;
verum end;