let I be non empty set ; :: thesis: for s being Element of I
for S being non empty FSM over I
for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non zero 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 zero 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 over I
for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non zero 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 zero Element of NAT st i < m holds
(GEN (w, the InitS of S)) . i <> q ) )
let S be non empty FSM over I; :: thesis: for q being State of S st S is calculating_type & q is_accessible_via s holds
ex m being non zero 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 zero 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 zero 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 zero 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 zero 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 zero 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 zero 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 zero 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;
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 zero Element of NAT by A5, ORDINAL1:def 12;
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 zero 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 zero 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 zero Element of NAT st i < m holds
(GEN (w1, the InitS of S)) . i <> q ) )
(<*s*> ^ w) . 1 = s by FINSEQ_1:41;
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) ) ;
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:1;
m in dom (GEN (w1, the InitS of S)) by A5, A7, A11, FINSEQ_1:1;
hence q = (GEN (w1, the InitS of S)) . m by A5, A9, A12, GRFUNC_1:2; :: thesis: for i being non zero Element of NAT st i < m holds
(GEN (w1, the InitS of S)) . i <> q
let i be non zero 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:1;
A19: i in dom (GEN (w1, the InitS of S)) by A14, A16, A17, FINSEQ_1:1;
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:2;
hence contradiction by A6, A13, A14, A15; :: thesis: verum