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)) ;
then A2: f is_homomorphism v,w ;
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:84;
hence w |= * (CastNode (((f |** i) . x),v)) by A3, A5, FUNCT_1:18; :: 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