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) st H is atomic holds
( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )
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) st H is atomic holds
( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )
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) st H is atomic holds
( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )
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) st H is atomic holds
( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )
let BASSIGN be non empty Subset of (ModelSP S); :: thesis: for kai being Function of atomic_WFF ,the BasicAssign of (CTLModel R,BASSIGN) st H is atomic holds
( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )
let kai be Function of atomic_WFF ,the BasicAssign of (CTLModel R,BASSIGN); :: thesis: ( H is atomic implies ( s,kai |= H iff kai . H in (Label_ BASSIGN) . s ) )
assume A1: H is atomic ; :: thesis: ( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )
ex f being Function of CTL_WFF ,the Assignations of (CTLModel R,BASSIGN) st
( f is-Evaluation-for kai & Evaluate H,kai = f . H ) by Def32;
then A2: Evaluate H,kai = kai . H by A1, Def26;
A3: ( s,kai |= H iff s |= Evaluate H,kai ) by Def60;
H in atomic_WFF by A1;
then Evaluate H,kai in BASSIGN by A2, FUNCT_2:7;
hence ( s,kai |= H iff kai . H in (Label_ BASSIGN) . s ) by A2, A3, Th11; :: thesis: verum