let v be LTL-formula; :: thesis: for w being Element of Inf_seq AtomicFamily
for f being Function of (LTLNodes v),(LTLNodes v) st f is_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
w |= * (CastNode (((f |** k) . x),v))
let w be Element of Inf_seq AtomicFamily; :: thesis: for f being Function of (LTLNodes v),(LTLNodes v) st f is_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
w |= * (CastNode (((f |** k) . x),v))
set LN = LTLNodes v;
let f be Function of (LTLNodes v),(LTLNodes v); :: thesis: ( f is_homomorphism v,w implies for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
w |= * (CastNode (((f |** k) . x),v)) )
assume f is_homomorphism v,w ; :: thesis: for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
w |= * (CastNode (((f |** k) . x),v))
then A1: for y being set st y in LTLNodes v & not CastNode (y,v) is elementary & w |= * (CastNode (y,v)) holds
w |= * (CastNode ((f . y),v)) ;
for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
w |= * (CastNode (((f |** k) . x),v))
proof
let x be set ; :: thesis: ( x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) implies for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
w |= * (CastNode (((f |** k) . x),v)) )
assume that
A2: x in LTLNodes v and
not CastNode (x,v) is elementary and
A3: w |= * (CastNode (x,v)) ; :: thesis: for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
w |= * (CastNode (((f |** k) . x),v))
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
w |= * (CastNode (((f |** k) . x),v))
proof
defpred S1[ Nat] means ( ( for i being Nat st i <= $1 holds
not CastNode (((f |** i) . x),v) is elementary ) implies w |= * (CastNode (((f |** $1) . x),v)) );
A4: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A5: S1[m] ; :: thesis: S1[m + 1]
S1[m + 1]
proof
set y = (f |** m) . x;
A6: m <= m + 1 by NAT_1:13;
A7: (f |** (m + 1)) . x = (f * (f |** m)) . x by FUNCT_7:71
.= f . ((f |** m) . x) by A2, FUNCT_2:15 ;
assume for i being Nat st i <= m + 1 holds
not CastNode (((f |** i) . x),v) is elementary ; :: thesis: w |= * (CastNode (((f |** (m + 1)) . x),v))
then ( not CastNode (((f |** m) . x),v) is elementary & w |= * (CastNode (((f |** m) . x),v)) ) by A5, A6, XXREAL_0:2;
hence w |= * (CastNode (((f |** (m + 1)) . x),v)) by A1, A2, A7, FUNCT_2:5; :: thesis: verum
end;
hence S1[m + 1] ; :: thesis: verum
end;
A8: S1[ 0 ]
proof
assume for i being Nat st i <= 0 holds
not CastNode (((f |** i) . x),v) is elementary ; :: thesis: w |= * (CastNode (((f |** 0) . x),v))
f |** 0 = id (LTLNodes v) by FUNCT_7:84;
hence w |= * (CastNode (((f |** 0) . x),v)) by A2, A3, FUNCT_1:18; :: thesis: verum
end;
A9: for m being Nat holds S1[m] from NAT_1:sch 2(A8, A4);
 let k be Nat; :: thesis: ( ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) implies w |= * (CastNode (((f |** k) . x),v)) )
assume for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ; :: thesis: w |= * (CastNode (((f |** k) . x),v))
hence w |= * (CastNode (((f |** k) . x),v)) by A9; :: thesis: verum
end;
hence for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
w |= * (CastNode (((f |** k) . x),v)) ; :: thesis: verum
end;
hence for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
for k being Nat st ( for i being Nat st i <= k holds
not CastNode (((f |** i) . x),v) is elementary ) holds
w |= * (CastNode (((f |** k) . x),v)) ; :: thesis: verum