let H be CTL-formula; :: thesis: for S being non empty set
for R being total Relation of S,S
for s being Element of S
for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= EG H iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) )
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 kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= EG H iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) )
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 kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= EG H iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) )
let s be Element of S; :: thesis: for BASSIGN being non empty Subset of (ModelSP S)
for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= EG H iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)) holds
( s,kai |= EG H iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) )
let kai be Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)); :: thesis: ( s,kai |= EG H iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) )
A1: ( ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= Evaluate (H,kai) ) ) implies ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) )

proof

given pai being inf_path of R such that A2: pai . 0 = s and
A3: for n being Element of NAT holds pai . n |= Evaluate (H,kai) ; :: thesis: ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) )
take pai ; :: thesis: ( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) )
for n being Element of NAT holds pai . n,kai |= H by A3;
hence ( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) by A2; :: thesis: verum

end;

A4: ( ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) implies ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= Evaluate (H,kai) ) ) )

proof

given pai being inf_path of R such that A5: pai . 0 = s and
A6: for n being Element of NAT holds pai . n,kai |= H ; :: thesis: ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n |= Evaluate (H,kai) ) )
take pai ; :: thesis: ( pai . 0 = s & ( for n being Element of NAT holds pai . n |= Evaluate (H,kai) ) )
for n being Element of NAT holds pai . n |= Evaluate (H,kai) by A6, Def60;
hence ( pai . 0 = s & ( for n being Element of NAT holds pai . n |= Evaluate (H,kai) ) ) by A5; :: thesis: verum

end;

( s,kai |= EG H iff s |= EG (Evaluate (H,kai)) ) by Th8;
hence ( s,kai |= EG H iff ex pai being inf_path of R st
( pai . 0 = s & ( for n being Element of NAT holds pai . n,kai |= H ) ) ) by A1, A4, Th15; :: thesis: verum