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 );
( (len (<*s*> ^ w)) + 1 >= 1 & q = (GEN (<*s*> ^ w),the InitS of S) . ((len (<*s*> ^ w)) + 1) ) by A2, FSM_1:def 3, NAT_1:11;
then A3: ex m being Nat st S₁[m] ;
consider m being Nat such that
A4: S₁[m] and
A5: for k being Nat st S₁[k] holds
m <= k from NAT_1:sch 5(A3);
reconsider m = m as non empty Element of NAT by A4, 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 A6: ( (len w1) + 1 >= m & 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, A6, Th4;
then A7: ( 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;
A8: 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 ;
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 ;
then ( m in dom (GEN (<*s*> ^ w),the InitS of S) & m in dom (GEN w1,the InitS of S) ) by A4, A6, A8, FINSEQ_1:3;
hence q = (GEN w1,the InitS of S) . m by A4, A7, 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 A9: i < m ; :: thesis: (GEN w1,the InitS of S) . i <> q
then A10: ( 1 <= i & i <= (len (<*s*> ^ w)) + 1 & i <= (len w1) + 1 ) by A4, A6, NAT_1:14, XXREAL_0: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 ;
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 A12: ( i in dom (GEN (<*s*> ^ w),the InitS of S) & i in dom (GEN w1,the InitS of S) ) by A10, A11, 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 A7, A12, GRFUNC_1:8;
hence contradiction by A5, A9, A10; :: thesis: verum