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 A0: 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 defSuccHom;
then A2: f is_homomorphism v,w by defHom;
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 B1: ( x in LTLNodes v & not CastNode x,v is elementary & 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
B2: ( ( for i being Nat st i < n holds
not CastNode ((f |** i) . x),v is elementary ) & CastNode ((f |** n) . x),v is elementary ) by A0, B1, ThLTLNodes04;
B302: 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 C1: 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 C1, XXREAL_0:2;
hence not CastNode ((f |** j) . x),v is elementary by B2; :: thesis: verum

end;

hence CastNode ((f |** (i + 1)) . x),v is_succ_of CastNode ((f |** i) . x),v by A0, B1, ThLTLNodes03; :: thesis: verum

end;

B303: 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 B2, B302;
defpred S₁[ Nat] means ( $1 <= n implies for i being Nat st i <= $1 holds
w |= * (CastNode ((f |** i) . x),v) );
B3: 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 B1, FUNCT_1:35; :: thesis: verum

end;

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

end;

B4: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

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

proof

assume D1: m + 1 <= n ; :: thesis: for i being Nat st i <= m + 1 holds
w |= * (CastNode ((f |** i) . x),v)
D2: m < n by D1, NAT_1:13;
then D3: not CastNode ((f |** m) . x),v is elementary by B2;
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) )
assume E1: i <= m + 1 ; :: thesis: w |= * (CastNode ((f |** i) . x),v)
w |= * (CastNode ((f |** m) . x),v) by D1, C1, NAT_1:13;
then w |= * (CastNode ((f |** (m + 1)) . x),v) by D3, A2, ThLTLNodes05, B1;
hence w |= * (CastNode ((f |** i) . x),v) by E1, D2, C1, 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;

for m being Nat holds S₁[m] from NAT_1:sch 2(B3, B4);
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 B2, B303; :: 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