let I be non empty set ; for S being non empty FSM over I st S is calculating_type holds
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
let S be non empty FSM over I; ( S is calculating_type implies 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 )
assume A1:
S is calculating_type
; 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
let w1, w2 be FinSequence of I; ( w1 . 1 = w2 . 1 implies GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable )
assume A2:
w1 . 1 = w2 . 1
; GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable
set A = (Seg (1 + (len w1))) /\ (Seg (1 + (len w2)));
( 1 + (len w1) <= 1 + (len w2) or 1 + (len w2) <= 1 + (len w1) )
;
then A3:
( ( Seg (1 + (len w1)) c= Seg (1 + (len w2)) & (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) = Seg (1 + (len w1)) ) or ( Seg (1 + (len w2)) c= Seg (1 + (len w1)) & (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) = Seg (1 + (len w2)) ) )
by FINSEQ_1:5, FINSEQ_1:7;
A4:
len (GEN (w1, the InitS of S)) = 1 + (len w1)
by FSM_1:def 2;
A5:
len (GEN (w2, the InitS of S)) = 1 + (len w2)
by FSM_1:def 2;
A6:
dom (GEN (w1, the InitS of S)) = Seg (1 + (len w1))
by A4, FINSEQ_1:def 3;
A7:
dom (GEN (w2, the InitS of S)) = Seg (1 + (len w2))
by A5, FINSEQ_1:def 3;
now for x being object st x in (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) holds
(GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . xlet x be
object ;
( x in (Seg (1 + (len w1))) /\ (Seg (1 + (len w2))) implies (GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . x )assume A8:
x in (Seg (1 + (len w1))) /\ (Seg (1 + (len w2)))
;
(GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . xthen reconsider i =
x as
Element of
NAT ;
A9:
i >= 1
by A3, A8, FINSEQ_1:1;
A10:
i <= 1
+ (len w1)
by A3, A8, FINSEQ_1:1;
i <= 1
+ (len w2)
by A3, A8, FINSEQ_1:1;
hence
(GEN (w1, the InitS of S)) . x = (GEN (w2, the InitS of S)) . x
by A1, A2, A9, A10;
verum end;
hence
( 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) )
by A3, A6, A7, GRFUNC_1:2; XBOOLE_0:def 9 verum