deffunc H1( set ) -> set = [[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);
set N3 = the
LTLnext of
(CastNode x,v);
assume
x in LTLNodes v
;
H1(x) in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):]
then
ex
N being
strict LTLnode of
v st
x = N
by Def30;
then reconsider x =
x as
strict LTLnode of
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:106, ZFMISC_1:def 3;
hence
H1(
x)
in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):]
by ZFMISC_1:106;
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 2(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 set st x1 in LTLNodes v & x2 in LTLNodes v & f . x1 = f . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
( 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 of
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 of
v st
x1 = Nx1
by A3, Def30;
reconsider x2 =
x2 as
strict LTLnode of
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 of
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, ZFMISC_1:33;
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, ZFMISC_1:33;
then
the
LTLold of
(CastNode x1,v) = the
LTLold of
(CastNode x2,v)
by ZFMISC_1:33;
hence
x1 = x2
by A12, A11, A8, A13, A10, ZFMISC_1:33;
verum
end;
then A14:
f is one-to-one
by FUNCT_2:25;
rng f is finite
;
then
dom (f " ) is finite
by A14, FUNCT_1:55;
then
( dom f = LTLNodes v & rng (f " ) is finite )
by FINSET_1:26, FUNCT_2:def 1;
hence
LTLNodes v is finite
by A14, FUNCT_1:55; verum