let I be non empty set ; :: thesis: for S being non empty FSM of 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 of 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 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] ) & ( 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
A2: for j being non empty 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

let j be non empty 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 <> 0 & j <> 1 ) ;
then A3: not j is trivial by NAT_2:def 1;
defpred S₁[ 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;
A4: S₁[2]

proof

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:8;
then consider WI being Element of I, QI, QI1 being State of S such that
A5: ( 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;
thus (GEN w1,the InitS of S) . 2 <> the InitS of S by A1, A5; :: thesis: verum

end;

A6: for h being non trivial Nat st S₁[h] holds
S₁[h + 1]

proof

let h be non trivial Nat; :: thesis: ( S₁[h] implies S₁[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₁[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:8;
then consider WI being Element of I, QI, QI1 being State of S such that
A9: ( 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;
thus (GEN w1,the InitS of S) . (h + 1) <> the InitS of S by A1, A9; :: thesis: verum

end;

for h being non trivial Nat holds S₁[h] from NAT_2:sch 2(A4, 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 A3; :: thesis: verum

end;

for j being non empty 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

let j be non empty 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 A10: ( w1 . 1 = w2 . 1 & j <= (len w1) + 1 & j <= (len w2) + 1 ) ; :: thesis: (GEN w1,the InitS of S) . j = (GEN w2,the InitS of S) . j
defpred S₁[ 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;
A11: S₁[1]

proof

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;

A12: for h being non empty Nat st S₁[h] holds
S₁[h + 1]

proof

let h be non empty Nat; :: thesis: ( S₁[h] implies S₁[h + 1] )
assume A13: 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₁[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 A14: ( w1 . 1 = w2 . 1 & h + 1 <= (len w1) + 1 & h + 1 <= (len w2) + 1 ) ; :: thesis: (GEN w1,the InitS of S) . (h + 1) = (GEN w2,the InitS of S) . (h + 1)
then A15: h <= len w1 by XREAL_1:8;
A16: h <= (len w1) + 1 by A14, NAT_1:13;
A17: 1 <= h by NAT_1:14;
then consider WI being Element of I, QI, QI1 being State of S such that
A18: ( 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 A15, FSM_1:def 2;
A19: h <= len w2 by A14, XREAL_1:8;
A20: h <= (len w2) + 1 by A14, NAT_1:13;
1 <= h by NAT_1:14;
then consider WI2 being Element of I, QI2, QI12 being State of S such that
A21: ( WI2 = w2 . h & QI2 = (GEN w2,the InitS of S) . h & QI12 = (GEN w2,the InitS of S) . (h + 1) & WI2 -succ_of QI2 = QI12 ) by A19, FSM_1:def 2;
A22: QI = QI2 by A13, A14, A16, A18, A20, A21;
X: h in NAT by ORDINAL1:def 13;
( h = 1 or h > 1 ) by A17, XXREAL_0:1;
then ( h = 1 or h >= 1 + 1 ) by NAT_1:13;
then ( WI = WI2 or QI <> the InitS of S ) by A2, A14, A16, A18, A21, X;
hence (GEN w1,the InitS of S) . (h + 1) = (GEN w2,the InitS of S) . (h + 1) by A1, A18, A21, A22; :: thesis: verum

end;

for j being non empty Nat holds S₁[j] from NAT_1:sch 10(A11, A12);
hence (GEN w1,the InitS of S) . j = (GEN w2,the InitS of S) . j by A10; :: thesis: verum

end;

hence S is calculating_type by Def1; :: thesis: verum