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 )
consider f being Function of CTL_WFF ,the Assignations of (CTLModel R,BASSIGN) such that
A2: ( f is-Evaluation-for kai & Evaluate H,kai = f . H ) by Def32;
A3: Evaluate H,kai = kai . H by A1, A2, Def26;
H in atomic_WFF by A1;
then A4: Evaluate H,kai in BASSIGN by A3, FUNCT_2:7;
( s,kai |= H iff s |= Evaluate H,kai ) by Def60;
hence ( s,kai |= H iff kai . H in (Label_ BASSIGN) . s ) by A3, A4, Th11; :: thesis: verum