deffunc H1( set ) -> object = [[ the LTLold of (CastNode (v,v)), the LTLnew of (CastNode (v,v))], the LTLnext of (CastNode (v,v))];
set X = bool (Subformulae v);
set LN = LTLNodes v;
set Y = [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):];
A1:
for x being set st x in LTLNodes v holds
H1(x) in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):]
proof
let x be
set ;
( x in LTLNodes v implies H1(x) in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] )
set N1 = the
LTLold of
(CastNode (x,v));
set N2 = the
LTLnew of
(CastNode (x,v));
assume
x in LTLNodes v
;
H1(x) in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):]
set M1 =
[ the LTLold of (CastNode (x,v)), the LTLnew of (CastNode (x,v))];
set X1 =
[:(bool (Subformulae v)),(bool (Subformulae v)):];
(
[:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] = [:[:(bool (Subformulae v)),(bool (Subformulae v)):],(bool (Subformulae v)):] &
[ the LTLold of (CastNode (x,v)), the LTLnew of (CastNode (x,v))] in [:(bool (Subformulae v)),(bool (Subformulae v)):] )
by ZFMISC_1:87, ZFMISC_1:def 3;
hence
H1(
x)
in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):]
by ZFMISC_1:87;
verum
end;
ex f being Function of (LTLNodes v),[:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] st
for x being set st x in LTLNodes v holds
f . x = H1(x)
from FUNCT_2:sch 11(A1);
then consider f being Function of (LTLNodes v),[:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] such that
A2:
for x being set st x in LTLNodes v holds
f . x = H1(x)
;
for x1, x2 being object st x1 in LTLNodes v & x2 in LTLNodes v & f . x1 = f . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in LTLNodes v & x2 in LTLNodes v & f . x1 = f . x2 implies x1 = x2 )
assume that A3:
x1 in LTLNodes v
and A4:
x2 in LTLNodes v
and A5:
f . x1 = f . x2
;
x1 = x2
A6:
ex
Nx2 being
strict LTLnode over
v st
x2 = Nx2
by A4, Def30;
set Nx23 = the
LTLnext of
(CastNode (x2,v));
set Nx22 = the
LTLnew of
(CastNode (x2,v));
set Nx21 = the
LTLold of
(CastNode (x2,v));
A7:
ex
Nx1 being
strict LTLnode over
v st
x1 = Nx1
by A3, Def30;
reconsider x2 =
x2 as
strict LTLnode over
v by A6;
set Nx11 = the
LTLold of
(CastNode (x1,v));
set Nx12 = the
LTLnew of
(CastNode (x1,v));
set Nx13 = the
LTLnext of
(CastNode (x1,v));
set Mx1 =
[ the LTLold of (CastNode (x1,v)), the LTLnew of (CastNode (x1,v))];
set Mx2 =
[ the LTLold of (CastNode (x2,v)), the LTLnew of (CastNode (x2,v))];
A8:
( the
LTLnew of
(CastNode (x2,v)) = the
LTLnew of
x2 & the
LTLnext of
(CastNode (x2,v)) = the
LTLnext of
x2 )
by Def16;
reconsider x1 =
x1 as
strict LTLnode over
v by A7;
A9:
(
f . x1 = [[ the LTLold of (CastNode (x1,v)), the LTLnew of (CastNode (x1,v))], the LTLnext of (CastNode (x1,v))] &
f . x2 = [[ the LTLold of (CastNode (x2,v)), the LTLnew of (CastNode (x2,v))], the LTLnext of (CastNode (x2,v))] )
by A2, A3, A4;
then A10:
the
LTLnext of
(CastNode (x1,v)) = the
LTLnext of
(CastNode (x2,v))
by A5, XTUPLE_0:1;
A11:
( the
LTLnext of
(CastNode (x1,v)) = the
LTLnext of
x1 & the
LTLold of
(CastNode (x2,v)) = the
LTLold of
x2 )
by Def16;
A12:
( the
LTLold of
(CastNode (x1,v)) = the
LTLold of
x1 & the
LTLnew of
(CastNode (x1,v)) = the
LTLnew of
x1 )
by Def16;
A13:
[ the LTLold of (CastNode (x1,v)), the LTLnew of (CastNode (x1,v))] = [ the LTLold of (CastNode (x2,v)), the LTLnew of (CastNode (x2,v))]
by A5, A9, XTUPLE_0:1;
then
the
LTLold of
(CastNode (x1,v)) = the
LTLold of
(CastNode (x2,v))
by XTUPLE_0:1;
hence
x1 = x2
by A12, A11, A8, A13, A10, XTUPLE_0:1;
verum
end;
then A14:
f is one-to-one
by FUNCT_2:19;
rng f is finite
;
then
dom (f ") is finite
by A14, FUNCT_1:33;
then
( dom f = LTLNodes v & rng (f ") is finite )
by FINSET_1:8, FUNCT_2:def 1;
hence
LTLNodes v is finite
by A14, FUNCT_1:33; verum