theorem Th22:
for
X being non
empty set for
f being
BinOp of
X for
M being non
empty Moore-SM_Final over
[:X,X:],
succ X st
M is
calculating_type & the
carrier of
M = succ X & the
FinalS of
M = X & the
InitS of
M = X & the
OFun of
M = id the
carrier of
M & ( for
x,
y being
Element of
X holds the
Tran of
M . [ the InitS of M,[x,y]] = f . (
x,
y) ) holds
(
M is
halting & ( for
x,
y being
Element of
X holds
f . (
x,
y)
is_result_of [x,y],
M ) )