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)) st H is atomic holds
( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )
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)) st H is atomic holds
( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )
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)) st H is atomic holds
( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )
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)) st H is atomic holds
( s,kai |= H iff kai . H in (Label_ BASSIGN) . s )
let BASSIGN be 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 kai be Function of atomic_WFF, the BasicAssign of (BASSModel (R,BASSIGN)); ( H is atomic implies ( s,kai |= H iff kai . H in (Label_ BASSIGN) . s ) )
assume A1:
H is atomic
; ( 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; verum