let I be non empty set ; :: thesis: for S being non empty FSM over I st ( for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I

for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) holds

S is calculating_type

let S be non empty FSM over I; :: thesis: ( ( for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I

for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) implies S is calculating_type )

assume that

A1: for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2] and

A2: for s being Element of I

for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ; :: thesis: S is calculating_type

A3: for j being non zero Element of NAT st j >= 2 holds

for w1 being FinSequence of I st j <= (len w1) + 1 holds

(GEN (w1, the InitS of S)) . j <> the InitS of S

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

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I

for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) holds

S is calculating_type

let S be non empty FSM over I; :: thesis: ( ( for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2] ) & ( for s being Element of I

for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ) implies S is calculating_type )

assume that

A1: for s1, s2 being Element of I

for q being State of S st q <> the InitS of S holds

the Tran of S . [q,s1] = the Tran of S . [q,s2] and

A2: for s being Element of I

for q1 being State of S holds the Tran of S . [q1,s] <> the InitS of S ; :: thesis: S is calculating_type

A3: for j being non zero Element of NAT st j >= 2 holds

for w1 being FinSequence of I st j <= (len w1) + 1 holds

(GEN (w1, the InitS of S)) . j <> the InitS of S

proof

for j being non zero Element of NAT
let j be non zero Element of NAT ; :: thesis: ( j >= 2 implies for w1 being FinSequence of I st j <= (len w1) + 1 holds

(GEN (w1, the InitS of S)) . j <> the InitS of S )

assume j >= 2 ; :: thesis: for w1 being FinSequence of I st j <= (len w1) + 1 holds

(GEN (w1, the InitS of S)) . j <> the InitS of S

then j <> 1 ;

then A4: not j is trivial by NAT_2:def 1;

defpred S_{1}[ Nat] means for w1 being FinSequence of I st $1 <= (len w1) + 1 holds

(GEN (w1, the InitS of S)) . $1 <> the InitS of S;

A5: S_{1}[2]
_{1}[h] holds

S_{1}[h + 1]
_{1}[h]
from NAT_2:sch 2(A5, A6);

hence for w1 being FinSequence of I st j <= (len w1) + 1 holds

(GEN (w1, the InitS of S)) . j <> the InitS of S by A4; :: thesis: verum

end;(GEN (w1, the InitS of S)) . j <> the InitS of S )

assume j >= 2 ; :: thesis: for w1 being FinSequence of I st j <= (len w1) + 1 holds

(GEN (w1, the InitS of S)) . j <> the InitS of S

then j <> 1 ;

then A4: not j is trivial by NAT_2:def 1;

defpred S

(GEN (w1, the InitS of S)) . $1 <> the InitS of S;

A5: S

proof

A6:
for h being non trivial Nat st S
let w1 be FinSequence of I; :: thesis: ( 2 <= (len w1) + 1 implies (GEN (w1, the InitS of S)) . 2 <> the InitS of S )

assume 2 <= (len w1) + 1 ; :: thesis: (GEN (w1, the InitS of S)) . 2 <> the InitS of S

then 1 + 1 <= (len w1) + 1 ;

then 1 <= len w1 by XREAL_1:6;

then ex WI being Element of I ex QI, QI1 being State of S st

( WI = w1 . 1 & QI = (GEN (w1, the InitS of S)) . 1 & QI1 = (GEN (w1, the InitS of S)) . (1 + 1) & WI -succ_of QI = QI1 ) by FSM_1:def 2;

hence (GEN (w1, the InitS of S)) . 2 <> the InitS of S by A2; :: thesis: verum

end;assume 2 <= (len w1) + 1 ; :: thesis: (GEN (w1, the InitS of S)) . 2 <> the InitS of S

then 1 + 1 <= (len w1) + 1 ;

then 1 <= len w1 by XREAL_1:6;

then ex WI being Element of I ex QI, QI1 being State of S st

( WI = w1 . 1 & QI = (GEN (w1, the InitS of S)) . 1 & QI1 = (GEN (w1, the InitS of S)) . (1 + 1) & WI -succ_of QI = QI1 ) by FSM_1:def 2;

hence (GEN (w1, the InitS of S)) . 2 <> the InitS of S by A2; :: thesis: verum

S

proof

for h being non trivial Nat holds S
let h be non trivial Nat; :: thesis: ( S_{1}[h] implies S_{1}[h + 1] )

assume for w1 being FinSequence of I st h <= (len w1) + 1 holds

(GEN (w1, the InitS of S)) . h <> the InitS of S ; :: thesis: S_{1}[h + 1]

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

assume A7: h + 1 <= (len w1) + 1 ; :: thesis: (GEN (w1, the InitS of S)) . (h + 1) <> the InitS of S

A8: 1 <= h by NAT_1:14;

h <= len w1 by A7, XREAL_1:6;

then ex WI being Element of I ex QI, QI1 being State of S st

( WI = w1 . h & QI = (GEN (w1, the InitS of S)) . h & QI1 = (GEN (w1, the InitS of S)) . (h + 1) & WI -succ_of QI = QI1 ) by A8, FSM_1:def 2;

hence (GEN (w1, the InitS of S)) . (h + 1) <> the InitS of S by A2; :: thesis: verum

end;assume for w1 being FinSequence of I st h <= (len w1) + 1 holds

(GEN (w1, the InitS of S)) . h <> the InitS of S ; :: thesis: S

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

assume A7: h + 1 <= (len w1) + 1 ; :: thesis: (GEN (w1, the InitS of S)) . (h + 1) <> the InitS of S

A8: 1 <= h by NAT_1:14;

h <= len w1 by A7, XREAL_1:6;

then ex WI being Element of I ex QI, QI1 being State of S st

( WI = w1 . h & QI = (GEN (w1, the InitS of S)) . h & QI1 = (GEN (w1, the InitS of S)) . (h + 1) & WI -succ_of QI = QI1 ) by A8, FSM_1:def 2;

hence (GEN (w1, the InitS of S)) . (h + 1) <> the InitS of S by A2; :: thesis: verum

hence for w1 being FinSequence of I st j <= (len w1) + 1 holds

(GEN (w1, the InitS of S)) . j <> the InitS of S by A4; :: thesis: verum

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

proof

hence
S is calculating_type
; :: thesis: verum
let j be non zero Element of NAT ; :: 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

A9: w1 . 1 = w2 . 1 and

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

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

defpred S_{1}[ Nat] means for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & $1 <= (len w1) + 1 & $1 <= (len w2) + 1 holds

(GEN (w1, the InitS of S)) . $1 = (GEN (w2, the InitS of S)) . $1;

A12: S_{1}[1]
_{1}[h] holds

S_{1}[h + 1]
_{1}[j]
from NAT_1:sch 10(A12, A13);

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

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

A9: w1 . 1 = w2 . 1 and

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

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

defpred S

(GEN (w1, the InitS of S)) . $1 = (GEN (w2, the InitS of S)) . $1;

A12: S

proof

A13:
for h being non zero Nat st S
let w1, w2 be FinSequence of I; :: thesis: ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 )

(GEN (w1, the InitS of S)) . 1 = the InitS of S by FSM_1:def 2;

hence ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 ) by FSM_1:def 2; :: thesis: verum

end;(GEN (w1, the InitS of S)) . 1 = the InitS of S by FSM_1:def 2;

hence ( w1 . 1 = w2 . 1 & 1 <= (len w1) + 1 & 1 <= (len w2) + 1 implies (GEN (w1, the InitS of S)) . 1 = (GEN (w2, the InitS of S)) . 1 ) by FSM_1:def 2; :: thesis: verum

S

proof

for j being non zero Nat holds S
let h be non zero Nat; :: thesis: ( S_{1}[h] implies S_{1}[h + 1] )

assume A14: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & h <= (len w1) + 1 & h <= (len w2) + 1 holds

(GEN (w1, the InitS of S)) . h = (GEN (w2, the InitS of S)) . h ; :: thesis: S_{1}[h + 1]

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

assume that

A15: w1 . 1 = w2 . 1 and

A16: h + 1 <= (len w1) + 1 and

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

A18: h <= len w1 by A16, XREAL_1:6;

A19: h <= (len w1) + 1 by A16, NAT_1:13;

A20: 1 <= h by NAT_1:14;

then consider WI being Element of I, QI, QI1 being State of S such that

A21: WI = w1 . h and

A22: QI = (GEN (w1, the InitS of S)) . h and

A23: QI1 = (GEN (w1, the InitS of S)) . (h + 1) and

A24: WI -succ_of QI = QI1 by A18, FSM_1:def 2;

A25: h <= len w2 by A17, XREAL_1:6;

A26: h <= (len w2) + 1 by A17, NAT_1:13;

1 <= h by NAT_1:14;

then consider WI2 being Element of I, QI2, QI12 being State of S such that

A27: WI2 = w2 . h and

A28: QI2 = (GEN (w2, the InitS of S)) . h and

A29: QI12 = (GEN (w2, the InitS of S)) . (h + 1) and

A30: WI2 -succ_of QI2 = QI12 by A25, FSM_1:def 2;

A31: QI = QI2 by A14, A15, A19, A22, A26, A28;

A32: h in NAT by ORDINAL1:def 12;

( h = 1 or h > 1 ) by A20, XXREAL_0:1;

then ( h = 1 or h >= 1 + 1 ) by NAT_1:13;

hence (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) by A1, A3, A15, A19, A21, A22, A23, A24, A27, A29, A30, A31, A32; :: thesis: verum

end;assume A14: for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & h <= (len w1) + 1 & h <= (len w2) + 1 holds

(GEN (w1, the InitS of S)) . h = (GEN (w2, the InitS of S)) . h ; :: thesis: S

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

assume that

A15: w1 . 1 = w2 . 1 and

A16: h + 1 <= (len w1) + 1 and

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

A18: h <= len w1 by A16, XREAL_1:6;

A19: h <= (len w1) + 1 by A16, NAT_1:13;

A20: 1 <= h by NAT_1:14;

then consider WI being Element of I, QI, QI1 being State of S such that

A21: WI = w1 . h and

A22: QI = (GEN (w1, the InitS of S)) . h and

A23: QI1 = (GEN (w1, the InitS of S)) . (h + 1) and

A24: WI -succ_of QI = QI1 by A18, FSM_1:def 2;

A25: h <= len w2 by A17, XREAL_1:6;

A26: h <= (len w2) + 1 by A17, NAT_1:13;

1 <= h by NAT_1:14;

then consider WI2 being Element of I, QI2, QI12 being State of S such that

A27: WI2 = w2 . h and

A28: QI2 = (GEN (w2, the InitS of S)) . h and

A29: QI12 = (GEN (w2, the InitS of S)) . (h + 1) and

A30: WI2 -succ_of QI2 = QI12 by A25, FSM_1:def 2;

A31: QI = QI2 by A14, A15, A19, A22, A26, A28;

A32: h in NAT by ORDINAL1:def 12;

( h = 1 or h > 1 ) by A20, XXREAL_0:1;

then ( h = 1 or h >= 1 + 1 ) by NAT_1:13;

hence (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) by A1, A3, A15, A19, A21, A22, A23, A24, A27, A29, A30, A31, A32; :: thesis: verum

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