let I be non empty set ; 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; ( ( 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]
; 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
let j be 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)) . jlet w1,
w2 be
FinSequence of
I;
( 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
;
(GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j
defpred S1[
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:
S1[1]
A6:
for
h being non
zero Nat st
S1[
h] holds
S1[
h + 1]
proof
let h be non
zero Nat;
( S1[h] implies S1[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
;
S1[h + 1]
let w1,
w2 be
FinSequence of
I;
( 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
;
(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;
verum
end;
for
j being non
zero Nat holds
S1[
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;
verum
end;
hence
S is calculating_type
; verum