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)) 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 (BASSModel (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 (BASSModel (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 (BASSModel (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 (BASSModel (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 (BASSModel (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 carrier of (BASSModel (R,BASSIGN)) st
( f is-Evaluation-for kai & Evaluate (H,kai) = f . H ) by Def34;
then A2: Evaluate (H,kai) = kai . H by A1;
H in atomic_WFF by A1;
then Evaluate (H,kai) in BASSIGN by A2, FUNCT_2:5;
hence ( s,kai |= H iff kai . H in (Label_ BASSIGN) . s ) by A2, Th11; :: thesis: verum