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 holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) 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 holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) implies S is calculating_type )

assume A1: for s1, s2 being Element of I

for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ; :: thesis: S is calculating_type

for j being non zero Element of NAT

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 holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) 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 holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ) implies S is calculating_type )

assume A1: for s1, s2 being Element of I

for q being State of S holds the Tran of S . [q,s1] = the Tran of S . [q,s2] ; :: thesis: S is calculating_type

for j being non zero Element of NAT

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

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

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;

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

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

hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by A2, A3, A4; :: 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

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

defpred S

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

A5: S

proof

A6:
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 A7: 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

A8: w1 . 1 = w2 . 1 and

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

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

A11: h <= len w1 by A9, XREAL_1:6;

A12: h <= (len w1) + 1 by A9, NAT_1:13;

1 <= h by NAT_1:14;

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

WI = w1 . h and

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

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

A15: WI -succ_of QI = QI1 by A11, FSM_1:def 2;

A16: h <= len w2 by A10, XREAL_1:6;

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

1 <= h by NAT_1:14;

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

WI2 = w2 . h and

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

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

A20: WI2 -succ_of QI2 = QI12 by A16, FSM_1:def 2;

QI = QI2 by A7, A8, A12, A13, A17, A18;

hence (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) by A1, A14, A15, A19, A20; :: thesis: verum

end;assume A7: 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

A8: w1 . 1 = w2 . 1 and

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

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

A11: h <= len w1 by A9, XREAL_1:6;

A12: h <= (len w1) + 1 by A9, NAT_1:13;

1 <= h by NAT_1:14;

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

WI = w1 . h and

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

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

A15: WI -succ_of QI = QI1 by A11, FSM_1:def 2;

A16: h <= len w2 by A10, XREAL_1:6;

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

1 <= h by NAT_1:14;

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

WI2 = w2 . h and

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

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

A20: WI2 -succ_of QI2 = QI12 by A16, FSM_1:def 2;

QI = QI2 by A7, A8, A12, A13, A17, A18;

hence (GEN (w1, the InitS of S)) . (h + 1) = (GEN (w2, the InitS of S)) . (h + 1) by A1, A14, A15, A19, A20; :: thesis: verum

hence (GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j by A2, A3, A4; :: thesis: verum