let I be non empty set ; for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) holds
S is calculating_type
let S be non empty FSM over I; ( ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable ) implies S is calculating_type )
assume A1:
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable
; S is calculating_type
let j be non zero Element of NAT ; FSM_2:def 1 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; ( 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
A5: dom (GEN (w1, the InitS of S)) =
Seg (len (GEN (w1, the InitS of S)))
by FINSEQ_1:def 3
.=
Seg ((len w1) + 1)
by FSM_1:def 2
;
A6: dom (GEN (w2, the InitS of S)) =
Seg (len (GEN (w2, the InitS of S)))
by FINSEQ_1:def 3
.=
Seg ((len w2) + 1)
by FSM_1:def 2
;
A7:
1 <= j
by NAT_1:14;
then A8:
j in dom (GEN (w1, the InitS of S))
by A3, A5, FINSEQ_1:1;
j in dom (GEN (w2, the InitS of S))
by A4, A6, A7, FINSEQ_1:1;
then A9:
j in (dom (GEN (w1, the InitS of S))) /\ (dom (GEN (w2, the InitS of S)))
by A8, XBOOLE_0:def 4;
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable
by A1, A2;
then
( GEN (w1, the InitS of S) c= GEN (w2, the InitS of S) or GEN (w2, the InitS of S) c= GEN (w1, the InitS of S) )
;
then
GEN (w1, the InitS of S) tolerates GEN (w2, the InitS of S)
by PARTFUN1:54;
hence
(GEN (w1, the InitS of S)) . j = (GEN (w2, the InitS of S)) . j
by A9, PARTFUN1:def 4; verum