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

proof

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₁[ 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₁[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: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;

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: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;

for h being non trivial Nat holds S₁[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;

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

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₁[ 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]

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;

A13: for h being non zero Nat st S₁[h] holds
S₁[h + 1]

proof

let h be non zero Nat; :: thesis: ( S₁[h] implies S₁[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₁[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;

for j being non zero Nat holds S₁[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;

hence S is calculating_type ; :: thesis: verum