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_succ_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) holds
ex n being Nat st
( ( for i being Nat st i < n holds
( not CastNode ((f |** i) . x),v is elementary & CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v ) ) & CastNode ((f |** n) . x),v is elementary & ( for i being Nat st i <= n holds
w |= * (CastNode ((f |** i) . x),v) ) )
let w be Element of Inf_seq AtomicFamily ; :: thesis: for f being Function of LTLNodes v, LTLNodes v st f is_succ_homomorphism v,w holds
for x being set st x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) holds
ex n being Nat st
( ( for i being Nat st i < n holds
( not CastNode ((f |** i) . x),v is elementary & CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v ) ) & CastNode ((f |** n) . x),v is elementary & ( for i being Nat st i <= n holds
w |= * (CastNode ((f |** i) . x),v) ) )
set LN = LTLNodes v;
let f be Function of LTLNodes v, LTLNodes v; :: thesis: ( f is_succ_homomorphism v,w implies for x being set st x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) holds
ex n being Nat st
( ( for i being Nat st i < n holds
( not CastNode ((f |** i) . x),v is elementary & CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v ) ) & CastNode ((f |** n) . x),v is elementary & ( for i being Nat st i <= n holds
w |= * (CastNode ((f |** i) . x),v) ) ) )
assume A1: f is_succ_homomorphism v,w ; :: thesis: for x being set st x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) holds
ex n being Nat st
( ( for i being Nat st i < n holds
( not CastNode ((f |** i) . x),v is elementary & CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v ) ) & CastNode ((f |** n) . x),v is elementary & ( for i being Nat st i <= n holds
w |= * (CastNode ((f |** i) . x),v) ) )
then 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) by Def32;
then A2: f is_homomorphism v,w by Def33;
for x being set st x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) holds
ex n being Nat st
( ( for i being Nat st i < n holds
( not CastNode ((f |** i) . x),v is elementary & CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v ) ) & CastNode ((f |** n) . x),v is elementary & ( for i being Nat st i <= n holds
w |= * (CastNode ((f |** i) . x),v) ) )

proof

let x be set ; :: thesis: ( x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) implies ex n being Nat st
( ( for i being Nat st i < n holds
( not CastNode ((f |** i) . x),v is elementary & CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v ) ) & CastNode ((f |** n) . x),v is elementary & ( for i being Nat st i <= n holds
w |= * (CastNode ((f |** i) . x),v) ) ) )
assume that
A3: x in LTLNodes v and
A4: not CastNode x,v is elementary and
A5: w |= * (CastNode x,v) ; :: thesis: ex n being Nat st
( ( for i being Nat st i < n holds
( not CastNode ((f |** i) . x),v is elementary & CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v ) ) & CastNode ((f |** n) . x),v is elementary & ( for i being Nat st i <= n holds
w |= * (CastNode ((f |** i) . x),v) ) )
consider n being Nat such that
A6: for i being Nat st i < n holds
not CastNode ((f |** i) . x),v is elementary and
A7: CastNode ((f |** n) . x),v is elementary by A1, A3, A4, A5, Th49;
for i being Nat st i < n holds
CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v

proof

let i be Nat; :: thesis: ( i < n implies CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v )
assume A8: i < n ; :: thesis: CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v
for j being Nat st j <= i holds
not CastNode ((f |** j) . x),v is elementary

proof

let j be Nat; :: thesis: ( j <= i implies not CastNode ((f |** j) . x),v is elementary )
assume j <= i ; :: thesis: not CastNode ((f |** j) . x),v is elementary
then j < n by A8, XXREAL_0:2;
hence not CastNode ((f |** j) . x),v is elementary by A6; :: thesis: verum

end;

hence CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v by A1, A3, A4, A5, Th48; :: thesis: verum

end;

then A9: for i being Nat st i < n holds
( not CastNode ((f |** i) . x),v is elementary & CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v ) by A6;
defpred S₁[ Nat] means ( $1 <= n implies for i being Nat st i <= $1 holds
w |= * (CastNode ((f |** i) . x),v) );
A10: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A11: S₁[m] ; :: thesis: S₁[m + 1]
S₁[m + 1]

proof

assume A12: m + 1 <= n ; :: thesis: for i being Nat st i <= m + 1 holds
w |= * (CastNode ((f |** i) . x),v)
then A13: m < n by NAT_1:13;
then A14: not CastNode ((f |** m) . x),v is elementary by A6;
for i being Nat st i <= m + 1 holds
w |= * (CastNode ((f |** i) . x),v)

proof

let i be Nat; :: thesis: ( i <= m + 1 implies w |= * (CastNode ((f |** i) . x),v) )
w |= * (CastNode ((f |** m) . x),v) by A11, A12, NAT_1:13;
then A15: w |= * (CastNode ((f |** (m + 1)) . x),v) by A2, A3, A4, A14, Th50;
assume i <= m + 1 ; :: thesis: w |= * (CastNode ((f |** i) . x),v)
hence w |= * (CastNode ((f |** i) . x),v) by A11, A13, A15, NAT_1:8; :: thesis: verum

end;

hence for i being Nat st i <= m + 1 holds
w |= * (CastNode ((f |** i) . x),v) ; :: thesis: verum

end;

hence S₁[m + 1] ; :: thesis: verum

end;

A16: S₁[ 0 ]

proof

assume 0 <= n ; :: thesis: for i being Nat st i <= 0 holds
w |= * (CastNode ((f |** i) . x),v)
for i being Nat st i <= 0 holds
w |= * (CastNode ((f |** i) . x),v)

proof

let i be Nat; :: thesis: ( i <= 0 implies w |= * (CastNode ((f |** i) . x),v) )
assume i <= 0 ; :: thesis: w |= * (CastNode ((f |** i) . x),v)
then i = 0 ;
then f |** i = id (LTLNodes v) by FUNCT_7:86;
hence w |= * (CastNode ((f |** i) . x),v) by A3, A5, FUNCT_1:35; :: thesis: verum

end;

hence for i being Nat st i <= 0 holds
w |= * (CastNode ((f |** i) . x),v) ; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A16, A10);
then for i being Nat st i <= n holds
w |= * (CastNode ((f |** i) . x),v) ;
hence ex n being Nat st
( ( for i being Nat st i < n holds
( not CastNode ((f |** i) . x),v is elementary & CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v ) ) & CastNode ((f |** n) . x),v is elementary & ( for i being Nat st i <= n holds
w |= * (CastNode ((f |** i) . x),v) ) ) by A7, A9; :: thesis: verum

end;

hence for x being set st x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) holds
ex n being Nat st
( ( for i being Nat st i < n holds
( not CastNode ((f |** i) . x),v is elementary & CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v ) ) & CastNode ((f |** n) . x),v is elementary & ( for i being Nat st i <= n holds
w |= * (CastNode ((f |** i) . x),v) ) ) ; :: thesis: verum