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_{1}[ 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_{1}[m]
by A3;

consider m being Nat such that

A5: S_{1}[m]
and

A6: for k being Nat st S_{1}[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

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

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

consider m being Nat such that

A5: S

A6: for k being Nat st S

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