let IAlph, OAlph be non empty set ; for tfsm being non empty Mealy-FSM over IAlph,OAlph
for k being Nat st Class (k -eq_states_EqR tfsm) = Class ((k + 1) -eq_states_EqR tfsm) holds
for m being Nat holds Class ((k + m) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm)
let tfsm be non empty Mealy-FSM over IAlph,OAlph; for k being Nat st Class (k -eq_states_EqR tfsm) = Class ((k + 1) -eq_states_EqR tfsm) holds
for m being Nat holds Class ((k + m) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm)
let k be Nat; ( Class (k -eq_states_EqR tfsm) = Class ((k + 1) -eq_states_EqR tfsm) implies for m being Nat holds Class ((k + m) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm) )
set S = the carrier of tfsm;
set CEk = Class (k -eq_states_EqR tfsm);
set Ek = k -eq_states_EqR tfsm;
set CEk1 = Class ((k + 1) -eq_states_EqR tfsm);
set Ek1 = (k + 1) -eq_states_EqR tfsm;
defpred S1[ Nat] means Class ((k + $1) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm);
assume
Class (k -eq_states_EqR tfsm) = Class ((k + 1) -eq_states_EqR tfsm)
; for m being Nat holds Class ((k + m) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm)
then A1:
k -eq_states_EqR tfsm = (k + 1) -eq_states_EqR tfsm
by FINSEQ_4:86;
A2:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
set CEkm =
Class ((k + m) -eq_states_EqR tfsm);
set Ekm =
(k + m) -eq_states_EqR tfsm;
set CEkm1 =
Class ((k + (m + 1)) -eq_states_EqR tfsm);
set Ekm1 =
(k + (m + 1)) -eq_states_EqR tfsm;
assume
Class ((k + m) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm)
;
S1[m + 1]
then A3:
(k + m) -eq_states_EqR tfsm = k -eq_states_EqR tfsm
by FINSEQ_4:86;
now for x being object holds
( ( x in Class ((k + (m + 1)) -eq_states_EqR tfsm) implies x in Class (k -eq_states_EqR tfsm) ) & ( x in Class (k -eq_states_EqR tfsm) implies x in Class ((k + (m + 1)) -eq_states_EqR tfsm) ) )let x be
object ;
( ( x in Class ((k + (m + 1)) -eq_states_EqR tfsm) implies x in Class (k -eq_states_EqR tfsm) ) & ( x in Class (k -eq_states_EqR tfsm) implies x in Class ((k + (m + 1)) -eq_states_EqR tfsm) ) )reconsider xx =
x as
set by TARSKI:1;
hereby ( x in Class (k -eq_states_EqR tfsm) implies x in Class ((k + (m + 1)) -eq_states_EqR tfsm) )
assume A4:
x in Class ((k + (m + 1)) -eq_states_EqR tfsm)
;
x in Class (k -eq_states_EqR tfsm)then reconsider x9 =
x as
Subset of the
carrier of
tfsm ;
consider qa being
object such that A5:
qa in the
carrier of
tfsm
and A6:
x9 = Class (
((k + (m + 1)) -eq_states_EqR tfsm),
qa)
by A4, EQREL_1:def 3;
reconsider qa =
qa as
Element of the
carrier of
tfsm by A5;
A7:
x9 c= the
carrier of
tfsm
;
now for y being object holds
( ( y in xx implies y in Class ((k -eq_states_EqR tfsm),qa) ) & ( y in Class ((k -eq_states_EqR tfsm),qa) implies y in xx ) )let y be
object ;
( ( y in xx implies y in Class ((k -eq_states_EqR tfsm),qa) ) & ( y in Class ((k -eq_states_EqR tfsm),qa) implies y in xx ) )assume A9:
y in Class (
(k -eq_states_EqR tfsm),
qa)
;
y in xxthen reconsider y9 =
y as
Element of the
carrier of
tfsm ;
[y9,qa] in k -eq_states_EqR tfsm
by A9, EQREL_1:19;
then A10:
k + 1
-equivalent y9,
qa
by A1, Def12;
A11:
1
<= k + 1
by NAT_1:11;
A12:
now for s being Element of IAlph
for k1 being Nat st k1 = ((k + m) + 1) - 1 holds
k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]let s be
Element of
IAlph;
for k1 being Nat st k1 = ((k + m) + 1) - 1 holds
k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]let k1 be
Nat;
( k1 = ((k + m) + 1) - 1 implies k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s] )set Sy9 = the
Tran of
tfsm . [y9,s];
set Sqa = the
Tran of
tfsm . [qa,s];
(
k in NAT &
k = (k + 1) - 1 )
by ORDINAL1:def 12;
then
k -equivalent the
Tran of
tfsm . [y9,s], the
Tran of
tfsm . [qa,s]
by A10, A11, Th27;
then A13:
[( the Tran of tfsm . [y9,s]),( the Tran of tfsm . [qa,s])] in k -eq_states_EqR tfsm
by Def12;
assume
k1 = ((k + m) + 1) - 1
;
k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]hence
k1 -equivalent the
Tran of
tfsm . [y9,s], the
Tran of
tfsm . [qa,s]
by A3, A13, Def12;
verum end;
( 1
<= (k + m) + 1 & 1
-equivalent y9,
qa )
by A10, A11, Th27, NAT_1:11;
then
(k + m) + 1
-equivalent y9,
qa
by A12, Th27;
then
[y9,qa] in (k + (m + 1)) -eq_states_EqR tfsm
by Def12;
hence
y in xx
by A6, EQREL_1:19;
verum end; then
x = Class (
(k -eq_states_EqR tfsm),
qa)
by TARSKI:2;
hence
x in Class (k -eq_states_EqR tfsm)
by EQREL_1:def 3;
verum
end; assume A14:
x in Class (k -eq_states_EqR tfsm)
;
x in Class ((k + (m + 1)) -eq_states_EqR tfsm)then reconsider x9 =
x as
Subset of the
carrier of
tfsm ;
consider qa being
object such that A15:
qa in the
carrier of
tfsm
and A16:
x9 = Class (
(k -eq_states_EqR tfsm),
qa)
by A14, EQREL_1:def 3;
reconsider qa =
qa as
Element of the
carrier of
tfsm by A15;
now for y being object holds
( ( y in xx implies y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) ) & ( y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) implies y in xx ) )let y be
object ;
( ( y in xx implies y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) ) & ( y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) implies y in xx ) )hereby ( y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa) implies y in xx )
assume A17:
y in xx
;
y in Class (((k + (m + 1)) -eq_states_EqR tfsm),qa)then reconsider y9 =
y as
Element of the
carrier of
tfsm by A16;
[y9,qa] in k -eq_states_EqR tfsm
by A16, A17, EQREL_1:19;
then A18:
k + 1
-equivalent y9,
qa
by A1, Def12;
A19:
1
<= k + 1
by NAT_1:11;
A20:
now for s being Element of IAlph
for k1 being Nat st k1 = ((k + m) + 1) - 1 holds
k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]let s be
Element of
IAlph;
for k1 being Nat st k1 = ((k + m) + 1) - 1 holds
k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]let k1 be
Nat;
( k1 = ((k + m) + 1) - 1 implies k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s] )set Sy9 = the
Tran of
tfsm . [y9,s];
set Sqa = the
Tran of
tfsm . [qa,s];
(
k in NAT &
k = (k + 1) - 1 )
by ORDINAL1:def 12;
then
k -equivalent the
Tran of
tfsm . [y9,s], the
Tran of
tfsm . [qa,s]
by A18, A19, Th27;
then A21:
[( the Tran of tfsm . [y9,s]),( the Tran of tfsm . [qa,s])] in k -eq_states_EqR tfsm
by Def12;
assume
k1 = ((k + m) + 1) - 1
;
k1 -equivalent the Tran of tfsm . [y9,s], the Tran of tfsm . [qa,s]hence
k1 -equivalent the
Tran of
tfsm . [y9,s], the
Tran of
tfsm . [qa,s]
by A3, A21, Def12;
verum end;
( 1
<= (k + m) + 1 & 1
-equivalent y9,
qa )
by A18, A19, Th27, NAT_1:11;
then
(k + m) + 1
-equivalent y9,
qa
by A20, Th27;
then
[y9,qa] in (k + (m + 1)) -eq_states_EqR tfsm
by Def12;
hence
y in Class (
((k + (m + 1)) -eq_states_EqR tfsm),
qa)
by EQREL_1:19;
verum
end; assume A22:
y in Class (
((k + (m + 1)) -eq_states_EqR tfsm),
qa)
;
y in xxthen reconsider y9 =
y as
Element of the
carrier of
tfsm ;
[y,qa] in (k + (m + 1)) -eq_states_EqR tfsm
by A22, EQREL_1:19;
then
k + (m + 1) -equivalent y9,
qa
by Def12;
then
k -equivalent y9,
qa
by Th26;
then
[y9,qa] in k -eq_states_EqR tfsm
by Def12;
hence
y in xx
by A16, EQREL_1:19;
verum end; then
x = Class (
((k + (m + 1)) -eq_states_EqR tfsm),
qa)
by TARSKI:2;
hence
x in Class ((k + (m + 1)) -eq_states_EqR tfsm)
by EQREL_1:def 3;
verum end;
hence
Class ((k + (m + 1)) -eq_states_EqR tfsm) = Class (k -eq_states_EqR tfsm)
by TARSKI:2;
verum
end;
A23:
S1[ 0 ]
;
thus
for m being Nat holds S1[m]
from NAT_1:sch 2(A23, A2); verum