let S be non empty set ; :: thesis: for R being total Relation of S,S
for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ) holds
for s being Element of S st s |= f EU g holds
s |= h
let R be total Relation of S,S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f, g, h being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ) holds
for s being Element of S st s |= f EU g holds
s |= h
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f, g, h being Assign of (CTLModel R,BASSIGN) st ( for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ) holds
for s being Element of S st s |= f EU g holds
s |= h
let f, g, h be Assign of (CTLModel R,BASSIGN); :: thesis: ( ( for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ) implies for s being Element of S st s |= f EU g holds
s |= h )
assume A1: for s being Element of S holds
( s |= h iff s |= Foax g,f,h ) ; :: thesis: for s being Element of S st s |= f EU g holds
s |= h
let s0 be Element of S; :: thesis: ( s0 |= f EU g implies s0 |= h )
assume s0 |= f EU g ; :: thesis: s0 |= h
then consider pai being inf_path of R such that
A2: pai . 0 = s0 and
A3: ex m being Element of NAT st
( ( for j being Element of NAT st j < m holds
pai . j |= f ) & pai . m |= g ) by Th16;
consider m being Element of NAT such that
A4: for j being Element of NAT st j < m holds
pai . j |= f and
A5: pai . m |= g by A3;
for j being Element of NAT st j <= m holds
pai . (k_nat (m - j)) |= h

proof

defpred S₁[ Element of NAT ] means ( $1 <= m implies pai . (k_nat (m - $1)) |= h );
A6: S₁[ 0 ]

proof

assume 0 <= m ; :: thesis: pai . (k_nat (m - 0 )) |= h
A7: k_nat (m - 0 ) = m by Def2;
pai . m |= Foax g,f,h by A5, Th17;
hence pai . (k_nat (m - 0 )) |= h by A1, A7; :: thesis: verum

end;

A8: for j being Element of NAT st S₁[j] holds
S₁[j + 1]

proof

let j be Element of NAT ; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A9: S₁[j] ; :: thesis: S₁[j + 1]
set j1 = j + 1;
( j + 1 <= m implies pai . (k_nat (m - (j + 1))) |= h )

proof

assume A10: j + 1 <= m ; :: thesis: pai . (k_nat (m - (j + 1))) |= h
set k = m - (j + 1);
reconsider k = m - (j + 1) as Element of NAT by A10, NAT_1:21;
A11: k_nat k = k by Def2;
A12: pai . (k + 1) |= h by A9, A10, Def2, NAT_1:13;
set pai1 = PathShift pai,k;
A13: (PathShift pai,k) . 0 = pai . (k + 0 ) by Def67
.= pai . k ;
(PathShift pai,k) . 1 = pai . (k + 1) by Def67;
then A14: pai . k |= EX h by A12, A13, Th14;
k < m

proof

k <= k + j by NAT_1:12;
then k < (k + j) + 1 by NAT_1:13;
hence k < m ; :: thesis: verum

end;

then pai . k |= f by A4;
then pai . k |= Fax f,h by A14, Th13;
then pai . k |= Foax g,f,h by Th17;
hence pai . (k_nat (m - (j + 1))) |= h by A1, A11; :: thesis: verum

end;

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

end;

for j being Element of NAT holds S₁[j] from NAT_1:sch 1(A6, A8);
hence for j being Element of NAT st j <= m holds
pai . (k_nat (m - j)) |= h ; :: thesis: verum

end;

then pai . (k_nat (m - m)) |= h ;
hence s0 |= h by A2, Def2; :: thesis: verum