let H be CTL-formula; 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 |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) )
let S be 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 |= 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; 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 |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) )
let s be 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 |= 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); for kai being Function of atomic_WFF, the BasicAssign of (BASSModel (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 (BASSModel (R,BASSIGN)); ( s,kai |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) )
A1:
( 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 ) )
by Def60;
( s,kai |= EX H iff s |= EX (Evaluate (H,kai)) )
by Th7;
hence
( s,kai |= EX H iff ex pai being inf_path of R st
( pai . 0 = s & pai . 1,kai |= H ) )
by A1, Th14; verum