set LN = LTLNodes v;
set X = bool (Subformulae v);
set Y = [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):];
deffunc H1( set ) -> set = [[the LTLold of (CastNode v,v),the LTLnew of (CastNode v,v)],the LTLnext of (CastNode v,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 ;
:: thesis: ( x in LTLNodes v implies H1(x) in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] )
assume
x in LTLNodes v
;
:: thesis: H1(x) in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):]
then consider N being
strict LTLnode of
v such that B1:
x = N
by defLTLNodes;
set N1 = the
LTLold of
(CastNode x,v);
set N2 = the
LTLnew of
(CastNode x,v);
set N3 = the
LTLnext of
(CastNode x,v);
set M1 =
[the LTLold of (CastNode x,v),the LTLnew of (CastNode x,v)];
set X1 =
[:(bool (Subformulae v)),(bool (Subformulae v)):];
B1p:
(
H1(
x)
= [[the LTLold of (CastNode x,v),the LTLnew of (CastNode x,v)],the LTLnext of (CastNode x,v)] &
[:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] = [:[:(bool (Subformulae v)),(bool (Subformulae v)):],(bool (Subformulae v)):] )
by ZFMISC_1:def 3;
reconsider x =
x as
strict LTLnode of
v by B1;
[the LTLold of (CastNode x,v),the LTLnew of (CastNode x,v)] in [:(bool (Subformulae v)),(bool (Subformulae v)):]
by ZFMISC_1:106;
hence
H1(
x)
in [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):]
by B1p, ZFMISC_1:106;
:: thesis: 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)
;
A3p:
( dom f = LTLNodes v & rng f c= [:(bool (Subformulae v)),(bool (Subformulae v)),(bool (Subformulae v)):] )
by FUNCT_2:def 1;
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 ;
:: thesis: ( x1 in LTLNodes v & x2 in LTLNodes v & f . x1 = f . x2 implies x1 = x2 )
assume B1:
(
x1 in LTLNodes v &
x2 in LTLNodes v &
f . x1 = f . x2 )
;
:: thesis: x1 = x2
consider Nx1 being
strict LTLnode of
v such that B2:
x1 = Nx1
by B1, defLTLNodes;
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)];
reconsider x1 =
x1 as
strict LTLnode of
v by B2;
B3:
( the
LTLold of
(CastNode x1,v) = the
LTLold of
x1 & the
LTLnew of
(CastNode x1,v) = the
LTLnew of
x1 & the
LTLnext of
(CastNode x1,v) = the
LTLnext of
x1 )
by defCastNode01;
B4:
f . x1 = [[the LTLold of (CastNode x1,v),the LTLnew of (CastNode x1,v)],the LTLnext of (CastNode x1,v)]
by A2, B1;
consider Nx2 being
strict LTLnode of
v such that B5:
x2 = Nx2
by B1, defLTLNodes;
set Nx21 = the
LTLold of
(CastNode x2,v);
set Nx22 = the
LTLnew of
(CastNode x2,v);
set Nx23 = the
LTLnext of
(CastNode x2,v);
set Mx2 =
[the LTLold of (CastNode x2,v),the LTLnew of (CastNode x2,v)];
reconsider x2 =
x2 as
strict LTLnode of
v by B5;
B6:
( the
LTLold of
(CastNode x2,v) = the
LTLold of
x2 & the
LTLnew of
(CastNode x2,v) = the
LTLnew of
x2 & the
LTLnext of
(CastNode x2,v) = the
LTLnext of
x2 )
by defCastNode01;
B7:
f . x2 = [[the LTLold of (CastNode x2,v),the LTLnew of (CastNode x2,v)],the LTLnext of (CastNode x2,v)]
by A2, B1;
(
[the LTLold of (CastNode x1,v),the LTLnew of (CastNode x1,v)] = [the LTLold of (CastNode x2,v),the LTLnew of (CastNode x2,v)] & the
LTLnext of
(CastNode x1,v) = the
LTLnext of
(CastNode x2,v) )
by B1, B4, B7, ZFMISC_1:33;
then
( the
LTLold of
(CastNode x1,v) = the
LTLold of
(CastNode x2,v) & the
LTLnew of
(CastNode x1,v) = the
LTLnew of
(CastNode x2,v) & the
LTLnext of
(CastNode x1,v) = the
LTLnext of
(CastNode x2,v) )
by ZFMISC_1:33;
hence
x1 = x2
by B3, B6;
:: thesis: verum
end;
then A4:
f is one-to-one
by FUNCT_2:25;
rng f is finite
;
then
dom (f " ) is finite
by A4, FUNCT_1:55;
then
rng (f " ) is finite
by FINSET_1:26;
hence
LTLNodes v is finite
by A4, A3p, FUNCT_1:55; :: thesis: verum