let I be non empty set ; :: thesis: for s being Element of I
for S being non empty FSM of I
for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN w,the InitS of S) . m & ( for i being non empty Element of NAT st i < m holds
(GEN w,the InitS of S) . i <> q ) )
let s be Element of I; :: thesis: for S being non empty FSM of I
for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN w,the InitS of S) . m & ( for i being non empty Element of NAT st i < m holds
(GEN w,the InitS of S) . i <> q ) )
let S be non empty FSM of I; :: thesis: for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN w,the InitS of S) . m & ( for i being non empty Element of NAT st i < m holds
(GEN w,the InitS of S) . i <> q ) )
let q be State of S; :: thesis: ( S is calculating_type & q is_accessible_via s implies ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN w,the InitS of S) . m & ( for i being non empty Element of NAT st i < m holds
(GEN w,the InitS of S) . i <> q ) ) )
assume A1: S is calculating_type ; :: thesis: ( not q is_accessible_via s or ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN w,the InitS of S) . m & ( for i being non empty Element of NAT st i < m holds
(GEN w,the InitS of S) . i <> q ) ) )
given w being FinSequence of I such that A2: the InitS of S,<*s*> ^ w -leads_to q ; :: according to FSM_2:def 2 :: thesis: ex m being non empty Element of NAT st
for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN w,the InitS of S) . m & ( for i being non empty Element of NAT st i < m holds
(GEN w,the InitS of S) . i <> q ) )
defpred S₁[ Nat] means ( q = (GEN (<*s*> ^ w),the InitS of S) . $1 & $1 >= 1 & $1 <= (len (<*s*> ^ w)) + 1 );
A3: (len (<*s*> ^ w)) + 1 >= 1 by NAT_1:11;
q = (GEN (<*s*> ^ w),the InitS of S) . ((len (<*s*> ^ w)) + 1) by A2, FSM_1:def 3;
then A4: ex m being Nat st S₁[m] by A3;
consider m being Nat such that
A5: S₁[m] and
A6: for k being Nat st S₁[k] holds
m <= k from NAT_1:sch 5(A4);
reconsider m = m as non empty Element of NAT by A5, ORDINAL1:def 13;
take m ; :: thesis: for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
( q = (GEN w,the InitS of S) . m & ( for i being non empty Element of NAT st i < m holds
(GEN w,the InitS of S) . i <> q ) )
let w1 be FinSequence of I; :: thesis: ( (len w1) + 1 >= m & w1 . 1 = s implies ( q = (GEN w1,the InitS of S) . m & ( for i being non empty Element of NAT st i < m holds
(GEN w1,the InitS of S) . i <> q ) ) )
assume that
A7: (len w1) + 1 >= m and
A8: w1 . 1 = s ; :: thesis: ( q = (GEN w1,the InitS of S) . m & ( for i being non empty Element of NAT st i < m holds
(GEN w1,the InitS of S) . i <> q ) )
(<*s*> ^ w) . 1 = s by FINSEQ_1:58;
then GEN w1,the InitS of S, GEN (<*s*> ^ w),the InitS of S are_c=-comparable by A1, A8, Th4;
then A9: ( GEN w1,the InitS of S c= GEN (<*s*> ^ w),the InitS of S or GEN (<*s*> ^ w),the InitS of S c= GEN w1,the InitS of S ) by XBOOLE_0:def 9;
A10: dom (GEN (<*s*> ^ w),the InitS of S) = Seg (len (GEN (<*s*> ^ w),the InitS of S)) by FINSEQ_1:def 3
.= Seg ((len (<*s*> ^ w)) + 1) by FSM_1:def 2 ;
A11: 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 ;
A12: m in dom (GEN (<*s*> ^ w),the InitS of S) by A5, A10, FINSEQ_1:3;
m in dom (GEN w1,the InitS of S) by A5, A7, A11, FINSEQ_1:3;
hence q = (GEN w1,the InitS of S) . m by A5, A9, A12, GRFUNC_1:8; :: thesis: for i being non empty Element of NAT st i < m holds
(GEN w1,the InitS of S) . i <> q
let i be non empty Element of NAT ; :: thesis: ( i < m implies (GEN w1,the InitS of S) . i <> q )
assume A13: i < m ; :: thesis: (GEN w1,the InitS of S) . i <> q
A14: 1 <= i by NAT_1:14;
A15: i <= (len (<*s*> ^ w)) + 1 by A5, A13, XXREAL_0:2;
A16: i <= (len w1) + 1 by A7, A13, XXREAL_0:2;
A17: 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 ;
dom (GEN (<*s*> ^ w),the InitS of S) = Seg (len (GEN (<*s*> ^ w),the InitS of S)) by FINSEQ_1:def 3
.= Seg ((len (<*s*> ^ w)) + 1) by FSM_1:def 2 ;
then A18: i in dom (GEN (<*s*> ^ w),the InitS of S) by A14, A15, FINSEQ_1:3;
A19: i in dom (GEN w1,the InitS of S) by A14, A16, A17, FINSEQ_1:3;
assume (GEN w1,the InitS of S) . i = q ; :: thesis: contradiction
then q = (GEN (<*s*> ^ w),the InitS of S) . i by A9, A18, A19, GRFUNC_1:8;
hence contradiction by A6, A13, A14, A15; :: thesis: verum