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 (CTLModel R,BASSIGN) holds
( s,kai |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,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 (CTLModel R,BASSIGN) holds
( s,kai |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,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 (CTLModel R,BASSIGN) holds
( s,kai |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,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 (CTLModel R,BASSIGN) holds
( s,kai |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for kai being Function of atomic_WFF ,the BasicAssign of (CTLModel R,BASSIGN) holds
( s,kai |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) )
let kai be Function of atomic_WFF ,the BasicAssign of (CTLModel R,BASSIGN); :: thesis: ( s,kai |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) )
( s,kai |= EX H iff s |= Evaluate (EX H),kai ) by Def60;
then A1: ( s,kai |= EX H iff s |= EX (Evaluate H,kai) ) by Th7;
A2: ( ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= Evaluate H,kai ) implies ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) )

proof

given pai being inf_path of R such that A3: ( pai . 0 = s & pai . 1 |= Evaluate H,kai ) ; :: thesis: ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H )
take pai ; :: thesis: ( pai . 0 = s & pai . 1,kai |= H )
thus ( pai . 0 = s & pai . 1,kai |= H ) by A3, Def60; :: thesis: verum

end;

( ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) implies ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= Evaluate H,kai ) )

proof

given pai being inf_path of R such that A4: ( pai . 0 = s & pai . 1,kai |= H ) ; :: thesis: ex pai being inf_path of R st
( pai . 0 = s & pai . 1 |= Evaluate H,kai )
take pai ; :: thesis: ( pai . 0 = s & pai . 1 |= Evaluate H,kai )
thus ( pai . 0 = s & pai . 1 |= Evaluate H,kai ) by A4, Def60; :: thesis: verum

end;

hence ( s,kai |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) ) by A1, A2, Th14; :: thesis: verum