defpred S1[ object ] means ex f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) st
( $1 = f & f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) );
consider Z being set such that
A1:
for c being object holds
( c in Z iff ( c in Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X)) & S1[c] ) )
from XBOOLE_0:sch 1();
Z c= Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))
by A1;
then reconsider Z = Z as Subset of (Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))) ;
take
Z
; for f being Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X) holds
( f in Z iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) )
let f be Function of [:(C -States the generators of X), the carrier of A:],(C -States the generators of X); ( f in Z iff ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) ) )
hereby ( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) implies f in Z )
assume
f in Z
;
( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) )then
S1[
f]
by A1;
hence
(
f is
ExecutionFunction of
A,
C -States the
generators of
X,
z -States ( the
generators of
X,
x) & ( for
s being
Element of
C -States the
generators of
X for
b being
SortSymbol of
B for
v being
Element of the
generators of
X . b for
v0 being
Element of
X,
b st
v0 = v holds
for
t being
Element of
T,
b holds
f . (
s,
(v := (t,A)))
= succ (
s,
v0,
(t value_at (C,s))) ) )
;
verum
end;
f in Funcs ([:(C -States the generators of X), the carrier of A:],(C -States the generators of X))
by FUNCT_2:8;
hence
( f is ExecutionFunction of A,C -States the generators of X,z -States ( the generators of X,x) & ( for s being Element of C -States the generators of X
for b being SortSymbol of B
for v being Element of the generators of X . b
for v0 being Element of X,b st v0 = v holds
for t being Element of T,b holds f . (s,(v := (t,A))) = succ (s,v0,(t value_at (C,s))) ) implies f in Z )
by A1; verum