let S be non empty set ; :: thesis: for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (CTLModel R,BASSIGN) holds
( s |= EG f iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) )
let R be total Relation of S,S; :: thesis: for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (CTLModel R,BASSIGN) holds
( s |= EG f iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for f being Assign of (CTLModel R,BASSIGN) holds
( s |= EG f iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for f being Assign of (CTLModel R,BASSIGN) holds
( s |= EG f iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) )
let f be Assign of (CTLModel R,BASSIGN); :: thesis: ( s |= EG f iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) )
A1: EG f = EGlobal_0 f,R by Def49;
A2: ( ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) implies s |= EG f )

proof

assume A3: ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) ; :: thesis: s |= EG f
ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds (Fid f,S) . (pai . n) = TRUE ) )

proof

consider pai being inf_path of R such that
A4: pai . 0 = s and
A5: for n being Element of NAT holds pai . n |= f by A3;
take pai ; :: thesis: ( pai . 0 = s & ( for n being Element of NAT holds (Fid f,S) . (pai . n) = TRUE ) )
for n being Element of NAT holds (Fid f,S) . (pai . n) = TRUE

proof

let n be Element of NAT ; :: thesis: (Fid f,S) . (pai . n) = TRUE
pai . n |= f by A5;
hence (Fid f,S) . (pai . n) = TRUE by Def59; :: thesis: verum

end;

hence ( pai . 0 = s & ( for n being Element of NAT holds (Fid f,S) . (pai . n) = TRUE ) ) by A4; :: thesis: verum

end;

then EGlobal_univ s,(Fid f,S),R = TRUE by Def47;
then (Fid (EG f),S) . s = TRUE by A1, Def48;
hence s |= EG f by Def59; :: thesis: verum

end;

( s |= EG f implies ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) )

proof

assume s |= EG f ; :: thesis: ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) )
then (Fid (EGlobal_0 f,R),S) . s = TRUE by A1, Def59;
then EGlobal_univ s,(Fid f,S),R = TRUE by Def48;
then consider pai being inf_path of R such that
A6: pai . 0 = s and
A7: for n being Element of NAT holds (Fid f,S) . (pai . n) = TRUE by Def47;
take pai ; :: thesis: ( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) )
for n being Element of NAT holds pai . n |= f

proof

let n be Element of NAT ; :: thesis: pai . n |= f
(Fid f,S) . (pai . n) = TRUE by A7;
hence pai . n |= f by Def59; :: thesis: verum

end;

hence ( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) by A6; :: thesis: verum

end;

hence ( s |= EG f iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= f ) ) ) by A2; :: thesis: verum